Theorems · Theorem · algebraic topology

SSet.PtSimplex.MulStruct.mk.inj

∀ {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g fg : X.PtSimplex n x} {i : Fin n}
  {map : SSet.stdSimplex.obj { len := n + 1 } ⟶ X}
  {δ_castSucc_castSucc_map :
    autoParam (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i.castSucc.castSucc) map = g.map)
      SSet.PtSimplex.MulStruct.δ_castSucc_castSucc_map._autoParam}
  {δ_succ_castSucc_map :
    autoParam (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i.castSucc.succ) map = fg.map)
      SSet.PtSimplex.MulStruct.δ_succ_castSucc_map._autoParam}
  {δ_succ_succ_map :
    autoParam (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i.succ.succ) map = f.map)
      SSet.PtSimplex.MulStruct.δ_succ_succ_map._autoParam}
  {δ_map_of_lt :
    autoParam (∀ j < i.castSucc.castSucc, CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ j) map = SSet.const x)
      SSet.PtSimplex.MulStruct.δ_map_of_lt._autoParam}
  {δ_map_of_gt :
    autoParam
      (∀ (j : Fin (n + 2)),
        i.succ.succ < j → CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ j) map = SSet.const x)
      SSet.PtSimplex.MulStruct.δ_map_of_gt._autoParam}
  {map_1 : SSet.stdSimplex.obj { len := n + 1 } ⟶ X}
  {δ_castSucc_castSucc_map_1 :
    autoParam (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i.castSucc.castSucc) map_1 = g.map)
      SSet.PtSimplex.MulStruct.δ_castSucc_castSucc_map._autoParam}
  {δ_succ_castSucc_map_1 :
    autoParam (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i.castSucc.succ) map_1 = fg.map)
      SSet.PtSimplex.MulStruct.δ_succ_castSucc_map._autoParam}
  {δ_succ_succ_map_1 :
    autoParam (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i.succ.succ) map_1 = f.map)
      SSet.PtSimplex.MulStruct.δ_succ_succ_map._autoParam}
  {δ_map_of_lt_1 :
    autoParam (∀ j < i.castSucc.castSucc, CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ j) map_1 = SSet.const x)
      SSet.PtSimplex.MulStruct.δ_map_of_lt._autoParam}
  {δ_map_of_gt_1 :
    autoParam
      (∀ (j : Fin (n + 2)),
        i.succ.succ < j → CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ j) map_1 = SSet.const x)
      SSet.PtSimplex.MulStruct.δ_map_of_gt._autoParam},
  { map := map, δ_castSucc_castSucc_map := δ_castSucc_castSucc_map, δ_succ_castSucc_map := δ_succ_castSucc_map,
        δ_succ_succ_map := δ_succ_succ_map, δ_map_of_lt := δ_map_of_lt, δ_map_of_gt := δ_map_of_gt } =
      { map := map_1, δ_castSucc_castSucc_map := δ_castSucc_castSucc_map_1,
        δ_succ_castSucc_map := δ_succ_castSucc_map_1, δ_succ_succ_map := δ_succ_succ_map_1,
        δ_map_of_lt := δ_map_of_lt_1, δ_map_of_gt := δ_map_of_gt_1 } →
    map = map_1

Defined in

Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Cited by

1 results in Mathlib

Foundations

Depth 44 from the axioms · uses propext, Classical.choice, Quot.sound