Theorems · Definition · algebraic topology

TopPair.HomologyPretheory.Hom.mk.noConfusion

{C : Type u_1} →
  {inst : CategoryTheory.Category.{v_1, u_1} C} →
    {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C} →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          {HP HP' : TopPair.HomologyPretheory C c} →
            {P : Sort u_3} →
              {homₚ : (i : ι) → HP.Hₚ i ⟶ HP'.Hₚ i} →
                {hom : (i : ι) → HP.H i ⟶ HP'.H i} →
                  {iso_comm :
                      autoParam
                        (∀ (i : ι),
                          CategoryTheory.CategoryStruct.comp (HP.iso i).hom (TopPair.incl.whiskerLeft (homₚ i)) =
                            CategoryTheory.CategoryStruct.comp (hom i) (HP'.iso i).hom)
                        TopPair.HomologyPretheory.Hom.iso_comm._autoParam} →
                    {w :
                        autoParam
                          (∀ (i j : ι),
                            CategoryTheory.CategoryStruct.comp (HP.δ i j) (TopPair.proj₂.whiskerLeft (hom j)) =
                              CategoryTheory.CategoryStruct.comp (homₚ i) (HP'.δ i j))
                          TopPair.HomologyPretheory.Hom.w._autoParam} →
                      {homₚ' : (i : ι) → HP.Hₚ i ⟶ HP'.Hₚ i} →
                        {hom' : (i : ι) → HP.H i ⟶ HP'.H i} →
                          {iso_comm' :
                              autoParam
                                (∀ (i : ι),
                                  CategoryTheory.CategoryStruct.comp (HP.iso i).hom
                                      (TopPair.incl.whiskerLeft (homₚ' i)) =
                                    CategoryTheory.CategoryStruct.comp (hom' i) (HP'.iso i).hom)
                                TopPair.HomologyPretheory.Hom.iso_comm._autoParam} →
                            {w' :
                                autoParam
                                  (∀ (i j : ι),
                                    CategoryTheory.CategoryStruct.comp (HP.δ i j) (TopPair.proj₂.whiskerLeft (hom' j)) =
                                      CategoryTheory.CategoryStruct.comp (homₚ' i) (HP'.δ i j))
                                  TopPair.HomologyPretheory.Hom.w._autoParam} →
                              { homₚ := homₚ, hom := hom, iso_comm := iso_comm, w := w } =
                                  { homₚ := homₚ', hom := hom', iso_comm := iso_comm', w := w' } →
                                (homₚ ≍ homₚ' → hom ≍ hom' → P) → P

Defined in

Mathlib.AlgebraicTopology.EilenbergSteenrod

Cited by

1 results in Mathlib

Foundations

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