Pointed simplices

Given a simplicial set X, n : ℕ and x : X _⦋0⦌, we introduce the type X.PtSimplex n x of morphisms Δ[n] ⟶ X which send ∂Δ[n] to x. We introduce structures PtSimplex.RelStruct and PtSimplex.MulStruct which will be used in the definition of homotopy groups of Kan complexes.

@[reducible, inline]

abbrev SSet.PtSimplex (X : SSet) (n : ℕ) (x : X.obj (Opposite.op { len := 0 })) : Type u

Given a simplicial set X, n : ℕ and x : X _⦋0⦌, this is the type of morphisms Δ[n] ⟶ X which are constant with value x on the boundary.

Equations

• X.PtSimplex n x = SSet.RelativeMorphism (SSet.boundary n) (SSet.Subcomplex.ofSimplex x) (SSet.const ⟨x, ⋯⟩)

@[implicit_reducible]

def SSet.PtSimplex.equiv₀ {X : SSet} (x : X.obj (Opposite.op { len := 0 })) : X.PtSimplex 0 x ≃ X.obj (Opposite.op { len := 0 })

The bijection X.PtSimplex 0 x ≃ X _⦋0⦌.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SSet.PtSimplex.equiv₀_apply {X : SSet} (x : X.obj (Opposite.op { len := 0 })) (f : X.PtSimplex 0 x) : (equiv₀ x) f = yonedaEquiv f.map

@[simp]

theorem SSet.PtSimplex.equiv₀_symm_apply_map {X : SSet} (x y : X.obj (Opposite.op { len := 0 })) : ((equiv₀ x).symm y).map = yonedaEquiv.symm y

theorem SSet.PtSimplex.map_eq_const_equiv₀ {X : SSet} {x : X.obj (Opposite.op { len := 0 })} (s : X.PtSimplex 0 x) : s.map = const ((equiv₀ x) s)

theorem SSet.PtSimplex.comp_map_eq_const {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} (s : X.PtSimplex n x) {Y : SSet} (φ : Y ⟶ stdSimplex.obj { len := n }) [Y.HasDimensionLT n] : CategoryTheory.CategoryStruct.comp φ s.map = const x

theorem SSet.PtSimplex.comp_map_eq_const_assoc {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} (s : X.PtSimplex n x) {Y : SSet} (φ : Y ⟶ stdSimplex.obj { len := n }) [Y.HasDimensionLT n] {Z : SSet} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp φ (CategoryTheory.CategoryStruct.comp s.map h) = CategoryTheory.CategoryStruct.comp (const x) h

@[simp]

theorem SSet.PtSimplex.δ_map {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} (f : X.PtSimplex (n + 1) x) (i : Fin (n + 2)) : CategoryTheory.CategoryStruct.comp (stdSimplex.δ i) f.map = const x

@[simp]

theorem SSet.PtSimplex.δ_map_assoc {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} (f : X.PtSimplex (n + 1) x) (i : Fin (n + 2)) {Z : SSet} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (stdSimplex.δ i) (CategoryTheory.CategoryStruct.comp f.map h) = CategoryTheory.CategoryStruct.comp (const x) h

def SSet.PtSimplex.opEquiv {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} : X.op.PtSimplex n (opObjEquiv.symm x) ≃ X.PtSimplex n x

The bijection between n-simplices of X.op and of X that are constant on the boundary.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SSet.PtSimplex.opEquiv_apply_map {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} (f : X.op.PtSimplex n (opObjEquiv.symm x)) : (opEquiv f).map = yonedaEquiv.symm (opObjEquiv (yonedaEquiv f.map))

@[simp]

theorem SSet.PtSimplex.opEquiv_symm_apply_map {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} (g : X.PtSimplex n x) : (opEquiv.symm g).map = yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv g.map))

@[reducible, inline]

abbrev SSet.PtSimplex.op {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} (f : X.PtSimplex n x) : X.op.PtSimplex n (opObjEquiv.symm x)

Given a n-simplex of X that is constant on the boundary, this is the corresponding n-simplex of X.op.

Equations

• f.op = SSet.PtSimplex.opEquiv.symm f

@[reducible, inline]

abbrev SSet.PtSimplex.unop {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} (f : X.op.PtSimplex n (opObjEquiv.symm x)) : X.PtSimplex n x

Given a n-simplex of X.op that is constant on the boundary, this is the corresponding n-simplex of X.

Equations

• f.unop = SSet.PtSimplex.opEquiv f

structure SSet.PtSimplex.RelStruct {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} (f g : X.PtSimplex n x) (i : Fin (n + 1)) : Type u

For each i : Fin (n + 1), this is a variant of the homotopy relation on n-simplices that are constant on the boundary. Simplices f and g are related if they appear respectively as the i.castSucc and i.succ faces of a n + 1-simplex such that all the other faces are constant.

• map : stdSimplex.obj { len := n + 1 } ⟶ X

  A n + 1-simplex

• δ_castSucc_map : CategoryTheory.CategoryStruct.comp (stdSimplex.δ i.castSucc) self.map = f.map
• δ_succ_map : CategoryTheory.CategoryStruct.comp (stdSimplex.δ i.succ) self.map = g.map
• δ_map_of_lt (j : Fin (n + 2)) (hj : j < i.castSucc) : CategoryTheory.CategoryStruct.comp (stdSimplex.δ j) self.map = const x
• δ_map_of_gt (j : Fin (n + 2)) (hj : i.succ < j) : CategoryTheory.CategoryStruct.comp (stdSimplex.δ j) self.map = const x

@[simp]

theorem SSet.PtSimplex.RelStruct.δ_map_of_lt_assoc {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g : X.PtSimplex n x} {i : Fin (n + 1)} (self : f.RelStruct g i) (j : Fin (n + 2)) (hj : j < i.castSucc) {Z : SSet} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (stdSimplex.δ j) (CategoryTheory.CategoryStruct.comp self.map h) = CategoryTheory.CategoryStruct.comp (const x) h

@[simp]

theorem SSet.PtSimplex.RelStruct.δ_map_of_gt_assoc {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g : X.PtSimplex n x} {i : Fin (n + 1)} (self : f.RelStruct g i) (j : Fin (n + 2)) (hj : i.succ < j) {Z : SSet} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (stdSimplex.δ j) (CategoryTheory.CategoryStruct.comp self.map h) = CategoryTheory.CategoryStruct.comp (const x) h

@[simp]

theorem SSet.PtSimplex.RelStruct.δ_succ_map_assoc {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g : X.PtSimplex n x} {i : Fin (n + 1)} (self : f.RelStruct g i) {Z : SSet} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (stdSimplex.δ i.succ) (CategoryTheory.CategoryStruct.comp self.map h) = CategoryTheory.CategoryStruct.comp g.map h

@[simp]

theorem SSet.PtSimplex.RelStruct.δ_castSucc_map_assoc {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g : X.PtSimplex n x} {i : Fin (n + 1)} (self : f.RelStruct g i) {Z : SSet} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (stdSimplex.δ i.castSucc) (CategoryTheory.CategoryStruct.comp self.map h) = CategoryTheory.CategoryStruct.comp f.map h

def SSet.PtSimplex.RelStruct.refl {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} (f : X.PtSimplex n x) (i : Fin (n + 1)) : f.RelStruct f i

RelStruct is reflexive.

Equations

• SSet.PtSimplex.RelStruct.refl f i = { map := CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.σ i) f.map, δ_castSucc_map := ⋯, δ_succ_map := ⋯, δ_map_of_lt := ⋯, δ_map_of_gt := ⋯ }

@[simp]

theorem SSet.PtSimplex.RelStruct.refl_map {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} (f : X.PtSimplex n x) (i : Fin (n + 1)) : (refl f i).map = CategoryTheory.CategoryStruct.comp (stdSimplex.σ i) f.map

def SSet.PtSimplex.RelStruct.copy {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g : X.PtSimplex n x} {i : Fin (n + 1)} (r : f.RelStruct g i) {f' g' : X.PtSimplex n x} (hf : f = f') (hg : g = g') : f'.RelStruct g' i

The RelStruct f' g' i deduced from r : RelStruct f g i when f = f' and g = g'.

Equations

• r.copy hf hg = { map := r.map, δ_castSucc_map := ⋯, δ_succ_map := ⋯, δ_map_of_lt := ⋯, δ_map_of_gt := ⋯ }

@[simp]

theorem SSet.PtSimplex.RelStruct.copy_map {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g : X.PtSimplex n x} {i : Fin (n + 1)} (r : f.RelStruct g i) {f' g' : X.PtSimplex n x} (hf : f = f') (hg : g = g') : (r.copy hf hg).map = r.map

def SSet.PtSimplex.RelStruct.ofEq {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g : X.PtSimplex n x} (h : f = g) (i : Fin (n + 1)) : f.RelStruct g i

The RelStruct f g i deduced from an equality f = g.

Equations

• SSet.PtSimplex.RelStruct.ofEq h i = (SSet.PtSimplex.RelStruct.refl f i).copy ⋯ h

@[simp]

theorem SSet.PtSimplex.RelStruct.ofEq_map {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g : X.PtSimplex n x} (h : f = g) (i : Fin (n + 1)) : (ofEq h i).map = CategoryTheory.CategoryStruct.comp (stdSimplex.σ i) f.map

@[reducible, inline]

abbrev SSet.PtSimplex.RelStruct₀ {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} (f g : X.PtSimplex n x) : Type u

One of the variants of the homotopy relation on n-simplices that are constant on the boundary. Simplices f and g are related if they appear respectively as the zeroth and first faces of a n + 1-simplex such that all the other faces are constant.

Equations

• f.RelStruct₀ g = f.RelStruct g 0

@[implicit_reducible]

def SSet.PtSimplex.RelStruct₀.equiv₀ {X : SSet} {x : X.obj (Opposite.op { len := 0 })} {f g : X.PtSimplex 0 x} : f.RelStruct₀ g ≃ Edge ((PtSimplex.equiv₀ x) g) ((PtSimplex.equiv₀ x) f)

In dimension 0, the type RelStruct₀ identify to a type of edges between 0-simplices.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SSet.PtSimplex.RelStruct₀.equiv₀_apply {X : SSet} {x : X.obj (Opposite.op { len := 0 })} {f g : X.PtSimplex 0 x} (h : f.RelStruct₀ g) : equiv₀ h = Edge.mk (yonedaEquiv h.map) ⋯ ⋯

@[simp]

theorem SSet.PtSimplex.RelStruct₀.equiv₀_symm_apply_map {X : SSet} {x : X.obj (Opposite.op { len := 0 })} {f g : X.PtSimplex 0 x} (e : Edge ((PtSimplex.equiv₀ x) g) ((PtSimplex.equiv₀ x) f)) : (equiv₀.symm e).map = yonedaEquiv.symm e.edge

structure SSet.PtSimplex.MulStruct {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} (f g fg : X.PtSimplex n x) (i : Fin n) : Type u

For each i : Fin n, this structure is a candidate for the relation saying that fg is the product of f and g in the homotopy group (of a Kan complex). It is so if g, fg and f are respectively the i.castSucc.castSucc, i.castSucc.succ and i.succ.succ faces of a n + 1-simplex such that all the other faces are constant. (The multiplication on homotopy groups will be defined using i := Fin.last _, but in general, this structure is useful in order to obtain properties of RelStruct.)

• map : stdSimplex.obj { len := n + 1 } ⟶ X

  A n + 1-simplex

• δ_castSucc_castSucc_map : CategoryTheory.CategoryStruct.comp (stdSimplex.δ i.castSucc.castSucc) self.map = g.map
• δ_succ_castSucc_map : CategoryTheory.CategoryStruct.comp (stdSimplex.δ i.castSucc.succ) self.map = fg.map
• δ_succ_succ_map : CategoryTheory.CategoryStruct.comp (stdSimplex.δ i.succ.succ) self.map = f.map
• δ_map_of_lt (j : Fin (n + 2)) (hj : j < i.castSucc.castSucc) : CategoryTheory.CategoryStruct.comp (stdSimplex.δ j) self.map = const x
• δ_map_of_gt (j : Fin (n + 2)) (hj : i.succ.succ < j) : CategoryTheory.CategoryStruct.comp (stdSimplex.δ j) self.map = const x

@[simp]

theorem SSet.PtSimplex.MulStruct.δ_castSucc_castSucc_map_assoc {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g fg : X.PtSimplex n x} {i : Fin n} (self : f.MulStruct g fg i) {Z : SSet} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (stdSimplex.δ i.castSucc.castSucc) (CategoryTheory.CategoryStruct.comp self.map h) = CategoryTheory.CategoryStruct.comp g.map h

@[simp]

theorem SSet.PtSimplex.MulStruct.δ_succ_succ_map_assoc {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g fg : X.PtSimplex n x} {i : Fin n} (self : f.MulStruct g fg i) {Z : SSet} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (stdSimplex.δ i.succ.succ) (CategoryTheory.CategoryStruct.comp self.map h) = CategoryTheory.CategoryStruct.comp f.map h

@[simp]

theorem SSet.PtSimplex.MulStruct.δ_map_of_gt_assoc {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g fg : X.PtSimplex n x} {i : Fin n} (self : f.MulStruct g fg i) (j : Fin (n + 2)) (hj : i.succ.succ < j) {Z : SSet} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (stdSimplex.δ j) (CategoryTheory.CategoryStruct.comp self.map h) = CategoryTheory.CategoryStruct.comp (const x) h

@[simp]

theorem SSet.PtSimplex.MulStruct.δ_succ_castSucc_map_assoc {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g fg : X.PtSimplex n x} {i : Fin n} (self : f.MulStruct g fg i) {Z : SSet} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (stdSimplex.δ i.castSucc.succ) (CategoryTheory.CategoryStruct.comp self.map h) = CategoryTheory.CategoryStruct.comp fg.map h

@[simp]

theorem SSet.PtSimplex.MulStruct.δ_map_of_lt_assoc {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g fg : X.PtSimplex n x} {i : Fin n} (self : f.MulStruct g fg i) (j : Fin (n + 2)) (hj : j < i.castSucc.castSucc) {Z : SSet} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (stdSimplex.δ j) (CategoryTheory.CategoryStruct.comp self.map h) = CategoryTheory.CategoryStruct.comp (const x) h

def SSet.PtSimplex.MulStruct.op {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g fg : X.PtSimplex n x} {i : Fin n} (h : f.MulStruct g fg i) {j : Fin n} (hij : i.rev = j := by grind) : g.op.MulStruct f.op fg.op j

The MulStruct for X.op that is deduced from a MulStruct for the simplicial set X.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SSet.PtSimplex.MulStruct.op_map {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g fg : X.PtSimplex n x} {i : Fin n} (h : f.MulStruct g fg i) {j : Fin n} (hij : i.rev = j := by grind) : (h.op hij).map = yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv h.map))

def SSet.PtSimplex.MulStruct.unop {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g fg : X.PtSimplex n x} {i : Fin n} (h : g.op.MulStruct f.op fg.op i) {j : Fin n} (hij : i.rev = j := by grind) : f.MulStruct g fg j

The Mulstruct for a simplicial set X that is deduced from a Mulstruct for X.op.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SSet.PtSimplex.MulStruct.unop_map {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g fg : X.PtSimplex n x} {i : Fin n} (h : g.op.MulStruct f.op fg.op i) {j : Fin n} (hij : i.rev = j := by grind) : (h.unop hij).map = yonedaEquiv.symm (opObjEquiv (yonedaEquiv h.map))

def SSet.PtSimplex.relStructCastSuccEquivMulStruct {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g : X.PtSimplex n x} {i : Fin n} : f.RelStruct g i.castSucc ≃ MulStruct RelativeMorphism.const f g i

If f and g are in X.PtSimplex n x, then RelStruct f g i.castSucc identifies to MulStruct .const f g i.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SSet.PtSimplex.relStructCastSuccEquivMulStruct_apply_map {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g : X.PtSimplex n x} {i : Fin n} (h : f.RelStruct g i.castSucc) : (relStructCastSuccEquivMulStruct h).map = h.map

@[simp]

theorem SSet.PtSimplex.relStructCastSuccEquivMulStruct_symm_apply_map {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g : X.PtSimplex n x} {i : Fin n} (h : MulStruct RelativeMorphism.const f g i) : (relStructCastSuccEquivMulStruct.symm h).map = h.map

def SSet.PtSimplex.relStructSuccEquivMulStruct {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g : X.PtSimplex n x} {i : Fin n} : f.RelStruct g i.succ ≃ g.MulStruct RelativeMorphism.const f i

If f and g are in X.PtSimplex n x, then RelStruct f g i.succ identifies to MulStruct g .const f i.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SSet.PtSimplex.relStructSuccEquivMulStruct_apply_map {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g : X.PtSimplex n x} {i : Fin n} (h : f.RelStruct g i.succ) : (relStructSuccEquivMulStruct h).map = h.map

@[simp]

theorem SSet.PtSimplex.relStructSuccEquivMulStruct_symm_apply_map {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g : X.PtSimplex n x} {i : Fin n} (h : g.MulStruct RelativeMorphism.const f i) : (relStructSuccEquivMulStruct.symm h).map = h.map

def SSet.PtSimplex.MulStruct.oneMul {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} (f : X.PtSimplex n x) (i : Fin n) : MulStruct RelativeMorphism.const f f i

Given f : X.PtSimplex n x and i : Fin n (note that this implies n ≠ 0), this is the term in MulStruct .const f f i corresponding to stdSimplex.σ i.castSucc ≫ f.map.

Equations

• SSet.PtSimplex.MulStruct.oneMul f i = SSet.PtSimplex.relStructCastSuccEquivMulStruct (SSet.PtSimplex.RelStruct.refl f i.castSucc)

@[simp]

theorem SSet.PtSimplex.MulStruct.oneMul_map {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} (f : X.PtSimplex n x) (i : Fin n) : (oneMul f i).map = CategoryTheory.CategoryStruct.comp (stdSimplex.σ i.castSucc) f.map

def SSet.PtSimplex.MulStruct.mulOne {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} (f : X.PtSimplex n x) (i : Fin n) : f.MulStruct RelativeMorphism.const f i

Given f : X.PtSimplex n x and i : Fin n (note that this implies n ≠ 0), this is the term in MulStruct f .const f i corresponding to stdSimplex.σ i.succ ≫ f.map.

Equations

• SSet.PtSimplex.MulStruct.mulOne f i = SSet.PtSimplex.relStructSuccEquivMulStruct (SSet.PtSimplex.RelStruct.refl f i.succ)

@[simp]

theorem SSet.PtSimplex.MulStruct.mulOne_map {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} (f : X.PtSimplex n x) (i : Fin n) : (mulOne f i).map = CategoryTheory.CategoryStruct.comp (stdSimplex.σ i.succ) f.map

noncomputable def SSet.PtSimplex.MulStruct.assoc {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} [X.KanComplex] {f₀₁ f₁₂ f₂₃ f₀₂ f₁₃ f₀₃ : X.PtSimplex n x} {i : Fin n} (h₀₂ : f₀₁.MulStruct f₁₂ f₀₂ i) (h₁₃ : f₁₂.MulStruct f₂₃ f₁₃ i) (h : f₀₁.MulStruct f₁₃ f₀₃ i) : f₀₂.MulStruct f₂₃ f₀₃ i

Given f₀₁, f₁₂, f₂₃, f₀₂, f₁₃ and f₀₃ in X.PtSimplex n x, if "the" multiplication of f₀₁ and f₁₂ is f₀₂, the multiplication of f₁₂ and f₂₃ is f₁₃, and the multiplication of f₀₁ and f₁₃ is f₀₃, then the multiplication of f₀₂ and f₂₃ is f₀₃.

Equations

• h₀₂.assoc h₁₃ h = SSet.PtSimplex.MulStruct.assocAux✝ h₀₂ h₁₃ h ⋯.liftOfKanComplex ⋯

noncomputable def SSet.PtSimplex.MulStruct.assoc' {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} [X.KanComplex] {f₀₁ f₁₂ f₂₃ f₀₂ f₁₃ f₀₃ : X.PtSimplex n x} {i : Fin n} (h₀₂ : f₀₁.MulStruct f₁₂ f₀₂ i) (h₁₃ : f₁₂.MulStruct f₂₃ f₁₃ i) (h : f₀₂.MulStruct f₂₃ f₀₃ i) : f₀₁.MulStruct f₁₃ f₀₃ i

Given f₀₁, f₁₂, f₂₃, f₀₂, f₁₃ and f₀₃ in X.PtSimplex n x, if "the" multiplication of f₀₁ and f₁₂ is f₀₂, the multiplication of f₁₂ and f₂₃ is f₁₃, and the multiplication of f₀₂ and f₂₃ is f₀₃, then the multiplication of f₀₁ and f₁₃ is f₀₃.

Equations

• h₀₂.assoc' h₁₃ h = ((h₁₃.op ⋯).assoc (h₀₂.op ⋯) (h.op ⋯)).unop ⋯

noncomputable def SSet.PtSimplex.MulStruct.mulOneEqSymm {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} [X.KanComplex] {p q : X.PtSimplex (n + 1) x} {i : Fin (n + 1)} (h : p.MulStruct RelativeMorphism.const q i) : q.MulStruct RelativeMorphism.const p i

A MulStruct q .const p i structure deduced from a MulStruct p .const q i structure.

Equations

• h.mulOneEqSymm = h.assoc (SSet.PtSimplex.MulStruct.mulOne SSet.RelativeMorphism.const i) (SSet.PtSimplex.MulStruct.mulOne p i)

noncomputable def SSet.PtSimplex.MulStruct.oneMulEqSymm {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} [X.KanComplex] {p q : X.PtSimplex (n + 1) x} {i : Fin (n + 1)} (h : MulStruct RelativeMorphism.const p q i) : MulStruct RelativeMorphism.const q p i

A MulStruct .const q p i structure deduced from a MulStruct .const p q i structure.

Equations

• h.oneMulEqSymm = (SSet.PtSimplex.MulStruct.oneMul SSet.RelativeMorphism.const i).assoc' h (SSet.PtSimplex.MulStruct.oneMul p i)

noncomputable def SSet.PtSimplex.MulStruct.oneMulEqOfMulOneEq {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} [X.KanComplex] {p q : X.PtSimplex (n + 1) x} {i : Fin (n + 1)} (h : p.MulStruct RelativeMorphism.const q i) : MulStruct RelativeMorphism.const p q i

A MulStruct .const p q i structure deduced from a MulStruct p .const q i structure.

Equations

• h.oneMulEqOfMulOneEq = ((SSet.PtSimplex.MulStruct.oneMul p i).assoc' h (SSet.PtSimplex.MulStruct.mulOne p i)).oneMulEqSymm

noncomputable def SSet.PtSimplex.MulStruct.mulOneEqOfOneMulEq {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} [X.KanComplex] {p q : X.PtSimplex (n + 1) x} {i : Fin (n + 1)} (h : MulStruct RelativeMorphism.const p q i) : p.MulStruct RelativeMorphism.const q i

A MulStruct p .const q i structure deduced from a MulStruct .const p q i structure.

Equations

• h.mulOneEqOfOneMulEq = (h.assoc (SSet.PtSimplex.MulStruct.mulOne p i) (SSet.PtSimplex.MulStruct.oneMul p i)).mulOneEqSymm

noncomputable def SSet.PtSimplex.MulStruct.mulOneEqTrans {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} [X.KanComplex] {p q r : X.PtSimplex (n + 1) x} {i : Fin (n + 1)} (h : p.MulStruct RelativeMorphism.const q i) (h' : q.MulStruct RelativeMorphism.const r i) : p.MulStruct RelativeMorphism.const r i

A MulStruct p .const r i structure deduced from MulStruct p .const q i and MulStruct q .const r i structures.

Equations

• h.mulOneEqTrans h' = (SSet.PtSimplex.MulStruct.oneMul p i).assoc h h'.oneMulEqOfMulOneEq

noncomputable def SSet.PtSimplex.MulStruct.oneMulEqTrans {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} [X.KanComplex] {p q r : X.PtSimplex (n + 1) x} {i : Fin (n + 1)} (h : MulStruct RelativeMorphism.const p q i) (h' : MulStruct RelativeMorphism.const q r i) : MulStruct RelativeMorphism.const p r i

A MulStruct .const p r i structure deduced from MulStruct .const p q i and MulStruct .const q r i structures.

Equations

• h.oneMulEqTrans h' = h.assoc' (SSet.PtSimplex.MulStruct.mulOne p i) h'.mulOneEqOfOneMulEq

theorem SSet.PtSimplex.MulStruct.nonempty {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} [X.KanComplex] (p q : X.PtSimplex (n + 1) x) (i : Fin (n + 1)) : ∃ (r : X.PtSimplex (n + 1) x), Nonempty (p.MulStruct q r i)

theorem SSet.PtSimplex.MulStruct.exists_left_inverse {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} [X.KanComplex] (p : X.PtSimplex (n + 1) x) (i : Fin (n + 1)) : ∃ (q : X.PtSimplex (n + 1) x), Nonempty (q.MulStruct p RelativeMorphism.const i)