Attaching cells #
Given a family of morphisms g a : A a ⟶ B a and a morphism f : X₁ ⟶ X₂,
we introduce a structure AttachCells g f which expresses that X₂
is obtained from X₁ by attaching cells of the form g a. It means that
there is a pushout diagram of the form
⨿ i, A (π i) -----> X₁
| |f
v v
⨿ i, B (π i) -----> X₂
In other words, the morphism f is a pushout of coproducts of morphisms
of the form g a : A a ⟶ B a, see nonempty_attachCells_iff.
See the file Mathlib.AlgebraicTopology.RelativeCellComplex.Basic for transfinite compositions
of morphisms f with AttachCells g f structures.
structure
HomotopicalAlgebra.AttachCells
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{α : Type t}
{A B : α → C}
(g : (a : α) → A a ⟶ B a)
{X₁ X₂ : C}
(f : X₁ ⟶ X₂)
:
Type (max (max (max t u) v) (w + 1))
Given a family of morphisms g a : A a ⟶ B a and a morphism f : X₁ ⟶ X₂,
this structure contains the data and properties which expresses that X₂
is obtained from X₁ by attaching cells of the form g a.
- ι : Type w
the index type of the cells
- π : self.ι → α
for each
i : ι, we shall attach a cell given by the morphismg (π i). - cofan₁ : CategoryTheory.Limits.Cofan fun (i : self.ι) => A (self.π i)
a colimit cofan which gives the coproduct of the object
A (π i) - cofan₂ : CategoryTheory.Limits.Cofan fun (i : self.ι) => B (self.π i)
a colimit cofan which gives the coproduct of the object
B (π i) - isColimit₁ : CategoryTheory.Limits.IsColimit self.cofan₁
cofan₁is colimit - isColimit₂ : CategoryTheory.Limits.IsColimit self.cofan₂
cofan₂is colimit the coproduct of the maps
g (π i) : A (π i) ⟶ B (π i)for alli : ι.- hm (i : self.ι) : CategoryTheory.CategoryStruct.comp (self.cofan₁.inj i) self.m = CategoryTheory.CategoryStruct.comp (g (self.π i)) (self.cofan₂.inj i)
the top morphism of the pushout square
the bottom morphism of the pushout square
- isPushout : CategoryTheory.IsPushout self.g₁ self.m f self.g₂
Instances For
@[simp]
theorem
HomotopicalAlgebra.AttachCells.hm_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{α : Type t}
{A B : α → C}
{g : (a : α) → A a ⟶ B a}
{X₁ X₂ : C}
{f : X₁ ⟶ X₂}
(self : AttachCells g f)
(i : self.ι)
{Z : C}
(h : self.cofan₂.pt ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (self.cofan₁.inj i) (CategoryTheory.CategoryStruct.comp self.m h) = CategoryTheory.CategoryStruct.comp (g (self.π i)) (CategoryTheory.CategoryStruct.comp (self.cofan₂.inj i) h)
theorem
HomotopicalAlgebra.AttachCells.pushouts_coproducts
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{α : Type t}
{A B : α → C}
{g : (a : α) → A a ⟶ B a}
{X₁ X₂ : C}
{f : X₁ ⟶ X₂}
(c : AttachCells g f)
:
def
HomotopicalAlgebra.AttachCells.cell
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{α : Type t}
{A B : α → C}
{g : (a : α) → A a ⟶ B a}
{X₁ X₂ : C}
{f : X₁ ⟶ X₂}
(c : AttachCells g f)
(i : c.ι)
:
The inclusion of a cell.
Instances For
theorem
HomotopicalAlgebra.AttachCells.cell_def
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{α : Type t}
{A B : α → C}
{g : (a : α) → A a ⟶ B a}
{X₁ X₂ : C}
{f : X₁ ⟶ X₂}
(c : AttachCells g f)
(i : c.ι)
:
theorem
HomotopicalAlgebra.AttachCells.cell_def_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{α : Type t}
{A B : α → C}
{g : (a : α) → A a ⟶ B a}
{X₁ X₂ : C}
{f : X₁ ⟶ X₂}
(c : AttachCells g f)
(i : c.ι)
{Z : C}
(h : X₂ ⟶ Z)
:
theorem
HomotopicalAlgebra.AttachCells.hom_ext
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{α : Type t}
{A B : α → C}
{g : (a : α) → A a ⟶ B a}
{X₁ X₂ : C}
{f : X₁ ⟶ X₂}
(c : AttachCells g f)
{Z : C}
{φ φ' : X₂ ⟶ Z}
(h₀ : CategoryTheory.CategoryStruct.comp f φ = CategoryTheory.CategoryStruct.comp f φ')
(h : ∀ (i : c.ι), CategoryTheory.CategoryStruct.comp (c.cell i) φ = CategoryTheory.CategoryStruct.comp (c.cell i) φ')
:
def
HomotopicalAlgebra.AttachCells.ofArrowIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{α : Type t}
{A B : α → C}
{g : (a : α) → A a ⟶ B a}
{X₁ X₂ : C}
{f : X₁ ⟶ X₂}
(c : AttachCells g f)
{Y₁ Y₂ : C}
{f' : Y₁ ⟶ Y₂}
(e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk f')
:
AttachCells g f'
If f and f' are isomorphic morphisms and the target of f
is obtained by attaching cells to the source of f,
then the same holds for f'.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
HomotopicalAlgebra.AttachCells.ofArrowIso_m
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{α : Type t}
{A B : α → C}
{g : (a : α) → A a ⟶ B a}
{X₁ X₂ : C}
{f : X₁ ⟶ X₂}
(c : AttachCells g f)
{Y₁ Y₂ : C}
{f' : Y₁ ⟶ Y₂}
(e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk f')
:
@[simp]
theorem
HomotopicalAlgebra.AttachCells.ofArrowIso_cofan₁
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{α : Type t}
{A B : α → C}
{g : (a : α) → A a ⟶ B a}
{X₁ X₂ : C}
{f : X₁ ⟶ X₂}
(c : AttachCells g f)
{Y₁ Y₂ : C}
{f' : Y₁ ⟶ Y₂}
(e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk f')
:
@[simp]
theorem
HomotopicalAlgebra.AttachCells.ofArrowIso_ι
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{α : Type t}
{A B : α → C}
{g : (a : α) → A a ⟶ B a}
{X₁ X₂ : C}
{f : X₁ ⟶ X₂}
(c : AttachCells g f)
{Y₁ Y₂ : C}
{f' : Y₁ ⟶ Y₂}
(e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk f')
:
@[simp]
theorem
HomotopicalAlgebra.AttachCells.ofArrowIso_isColimit₂
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{α : Type t}
{A B : α → C}
{g : (a : α) → A a ⟶ B a}
{X₁ X₂ : C}
{f : X₁ ⟶ X₂}
(c : AttachCells g f)
{Y₁ Y₂ : C}
{f' : Y₁ ⟶ Y₂}
(e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk f')
:
@[simp]
theorem
HomotopicalAlgebra.AttachCells.ofArrowIso_isColimit₁
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{α : Type t}
{A B : α → C}
{g : (a : α) → A a ⟶ B a}
{X₁ X₂ : C}
{f : X₁ ⟶ X₂}
(c : AttachCells g f)
{Y₁ Y₂ : C}
{f' : Y₁ ⟶ Y₂}
(e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk f')
:
@[simp]
theorem
HomotopicalAlgebra.AttachCells.ofArrowIso_g₂
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{α : Type t}
{A B : α → C}
{g : (a : α) → A a ⟶ B a}
{X₁ X₂ : C}
{f : X₁ ⟶ X₂}
(c : AttachCells g f)
{Y₁ Y₂ : C}
{f' : Y₁ ⟶ Y₂}
(e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk f')
:
@[simp]
theorem
HomotopicalAlgebra.AttachCells.ofArrowIso_cofan₂
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{α : Type t}
{A B : α → C}
{g : (a : α) → A a ⟶ B a}
{X₁ X₂ : C}
{f : X₁ ⟶ X₂}
(c : AttachCells g f)
{Y₁ Y₂ : C}
{f' : Y₁ ⟶ Y₂}
(e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk f')
:
@[simp]
theorem
HomotopicalAlgebra.AttachCells.ofArrowIso_g₁
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{α : Type t}
{A B : α → C}
{g : (a : α) → A a ⟶ B a}
{X₁ X₂ : C}
{f : X₁ ⟶ X₂}
(c : AttachCells g f)
{Y₁ Y₂ : C}
{f' : Y₁ ⟶ Y₂}
(e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk f')
:
@[simp]
theorem
HomotopicalAlgebra.AttachCells.ofArrowIso_π
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{α : Type t}
{A B : α → C}
{g : (a : α) → A a ⟶ B a}
{X₁ X₂ : C}
{f : X₁ ⟶ X₂}
(c : AttachCells g f)
{Y₁ Y₂ : C}
{f' : Y₁ ⟶ Y₂}
(e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk f')
(a✝ : c.ι)
:
def
HomotopicalAlgebra.AttachCells.reindex
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{α : Type t}
{A B : α → C}
{g : (a : α) → A a ⟶ B a}
{X₁ X₂ : C}
{f : X₁ ⟶ X₂}
(c : AttachCells g f)
{ι' : Type w'}
(e : ι' ≃ c.ι)
:
AttachCells g f
This definition allows the replacement of the ι field of
a AttachCells g f structure by an equivalent type.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
HomotopicalAlgebra.AttachCells.reindex_ι
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{α : Type t}
{A B : α → C}
{g : (a : α) → A a ⟶ B a}
{X₁ X₂ : C}
{f : X₁ ⟶ X₂}
(c : AttachCells g f)
{ι' : Type w'}
(e : ι' ≃ c.ι)
:
@[simp]
theorem
HomotopicalAlgebra.AttachCells.reindex_isColimit₁
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{α : Type t}
{A B : α → C}
{g : (a : α) → A a ⟶ B a}
{X₁ X₂ : C}
{f : X₁ ⟶ X₂}
(c : AttachCells g f)
{ι' : Type w'}
(e : ι' ≃ c.ι)
:
@[simp]
theorem
HomotopicalAlgebra.AttachCells.reindex_cofan₁
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{α : Type t}
{A B : α → C}
{g : (a : α) → A a ⟶ B a}
{X₁ X₂ : C}
{f : X₁ ⟶ X₂}
(c : AttachCells g f)
{ι' : Type w'}
(e : ι' ≃ c.ι)
:
@[simp]
theorem
HomotopicalAlgebra.AttachCells.reindex_g₂
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{α : Type t}
{A B : α → C}
{g : (a : α) → A a ⟶ B a}
{X₁ X₂ : C}
{f : X₁ ⟶ X₂}
(c : AttachCells g f)
{ι' : Type w'}
(e : ι' ≃ c.ι)
:
@[simp]
theorem
HomotopicalAlgebra.AttachCells.reindex_isColimit₂
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{α : Type t}
{A B : α → C}
{g : (a : α) → A a ⟶ B a}
{X₁ X₂ : C}
{f : X₁ ⟶ X₂}
(c : AttachCells g f)
{ι' : Type w'}
(e : ι' ≃ c.ι)
:
@[simp]
theorem
HomotopicalAlgebra.AttachCells.reindex_m
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{α : Type t}
{A B : α → C}
{g : (a : α) → A a ⟶ B a}
{X₁ X₂ : C}
{f : X₁ ⟶ X₂}
(c : AttachCells g f)
{ι' : Type w'}
(e : ι' ≃ c.ι)
:
@[simp]
theorem
HomotopicalAlgebra.AttachCells.reindex_g₁
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{α : Type t}
{A B : α → C}
{g : (a : α) → A a ⟶ B a}
{X₁ X₂ : C}
{f : X₁ ⟶ X₂}
(c : AttachCells g f)
{ι' : Type w'}
(e : ι' ≃ c.ι)
:
@[simp]
theorem
HomotopicalAlgebra.AttachCells.reindex_cofan₂
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{α : Type t}
{A B : α → C}
{g : (a : α) → A a ⟶ B a}
{X₁ X₂ : C}
{f : X₁ ⟶ X₂}
(c : AttachCells g f)
{ι' : Type w'}
(e : ι' ≃ c.ι)
:
@[simp]
theorem
HomotopicalAlgebra.AttachCells.reindex_π
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{α : Type t}
{A B : α → C}
{g : (a : α) → A a ⟶ B a}
{X₁ X₂ : C}
{f : X₁ ⟶ X₂}
(c : AttachCells g f)
{ι' : Type w'}
(e : ι' ≃ c.ι)
(i' : ι')
:
def
HomotopicalAlgebra.AttachCells.reindexCellTypes
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{α : Type t}
{A B : α → C}
{g : (a : α) → A a ⟶ B a}
{X₁ X₂ : C}
{f : X₁ ⟶ X₂}
(c : AttachCells g f)
{α' : Type t'}
{A' B' : α' → C}
(g' : (i' : α') → A' i' ⟶ B' i')
(a : α → α')
(ha : (i : α) → CategoryTheory.Arrow.mk (g i) ≅ CategoryTheory.Arrow.mk (g' (a i)))
:
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'.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
HomotopicalAlgebra.nonempty_attachCells_iff
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{α : Type t}
{A B : α → C}
(g : (a : α) → A a ⟶ B a)
{X₁ X₂ : C}
(f : X₁ ⟶ X₂)
: