Theorems · Definition · category theory

HomotopicalAlgebra.AttachCells.reindexCellTypes

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {α : Type t} →
      {A B : α → C} →
        {g : (a : α) → A a ⟶ B a} →
          {X₁ X₂ : C} →
            {f : X₁ ⟶ X₂} →
              HomotopicalAlgebra.AttachCells g f →
                {α' : Type t'} →
                  {A' B' : α' → C} →
                    (g' : (i' : α') → A' i' ⟶ B' i') →
                      (a : α → α') →
                        ((i : α) → CategoryTheory.Arrow.mk (g i) ≅ CategoryTheory.Arrow.mk (g' (a i))) →
                          HomotopicalAlgebra.AttachCells g' f

If a family of maps g is contained in another family g' (up to isomorphisms), if f : X₁ ⟶ X₂ is a morphism, and X₂ is obtained from X₁ by attaching cells of the form g, then it is also obtained by attaching cells of the form g'.

Defined in

Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category