Theorems · Theorem · algebraic topology

CategoryTheory.SimplicialObject.Split.Hom.mk.inj

∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {S₁ S₂ : CategoryTheory.SimplicialObject.Split C}
  {F : S₁.X ⟶ S₂.X} {f : (n : ℕ) → S₁.s.N n ⟶ S₂.s.N n}
  {comm :
    autoParam
      (∀ (n : ℕ),
        CategoryTheory.CategoryStruct.comp (S₁.s.ι n) (F.app (Opposite.op { len := n })) =
          CategoryTheory.CategoryStruct.comp (f n) (S₂.s.ι n))
      CategoryTheory.SimplicialObject.Split.Hom.comm._autoParam}
  {F_1 : S₁.X ⟶ S₂.X} {f_1 : (n : ℕ) → S₁.s.N n ⟶ S₂.s.N n}
  {comm_1 :
    autoParam
      (∀ (n : ℕ),
        CategoryTheory.CategoryStruct.comp (S₁.s.ι n) (F_1.app (Opposite.op { len := n })) =
          CategoryTheory.CategoryStruct.comp (f_1 n) (S₂.s.ι n))
      CategoryTheory.SimplicialObject.Split.Hom.comm._autoParam},
  { F := F, f := f, comm := comm } = { F := F_1, f := f_1, comm := comm_1 } → F = F_1 ∧ f = f_1

Defined in

Mathlib.AlgebraicTopology.SimplicialObject.Split

Cited by

1 results in Mathlib

Foundations

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