Other results

Results named in the rest of Tau Ceti's TauCeti.AlgebraicTopology modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

DefinitionThe Eilenberg–Zilber theorem#

the Alexander–Whitney map C(K × L; R ⊗ S) ⟶ C(K; R) ⊗ C(L; S) is a chain homotopy equivalence, with homotopy inverse the shuffle map.

SSet.eilenbergZilberHomotopyEquiv.{w, v, u} {C : Type u} [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C]
  [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C]
  [∀ (X : C) (J : Type w),
      CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J)
        (CategoryTheory.MonoidalCategory.tensorLeft X)]
  [∀ (X : C) (J : Type w),
      CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J)
        (CategoryTheory.MonoidalCategory.tensorRight X)]
  (K L : _root_.SSet) (R S : C) :
  HomotopyEquiv
    ((CategoryTheory.MonoidalCategoryStruct.tensorObj K L).chainComplex
      (CategoryTheory.MonoidalCategoryStruct.tensorObj R S))
    (CategoryTheory.MonoidalCategoryStruct.tensorObj (K.chainComplex R) (L.chainComplex S))

Lean

Formalized in Tau Ceti as SSet.eilenbergZilberHomotopyEquiv.

Sources

• Tau Ceti documentation: SSet.eilenbergZilberHomotopyEquiv
• Source of SSet.eilenbergZilberHomotopyEquiv in TauCeti/AlgebraicTopology/SimplicialSet/EilenbergZilber.lean

LeanSSet.eilenbergZilberHomotopyEquiv

TheoremJoyal's theorem on special outer horns (HTT Proposition 1.2.4.3)#

in a quasicategory, a horn Λ[n + 2, 0] whose initial edge, from 0 to 1, is an equivalence can be filled.

SSet.Quasicategory.hornFilling_zero.{u} {C : _root_.SSet} [C.Quasicategory] {n : ℕ}
  (σ₀ : (SSet.horn (n + 2) 0).toSSet ⟶ C)
  (h :
    (SSet.Edge.mk'
        ((CategoryTheory.ConcreteCategory.hom (σ₀.app (Opposite.op { len := 1 })))
          (SSet.horn.edge (n + 2) 0 0 1 ⋯ ⋯))).IsEquivalence) :
  ∃ σ, σ₀ = CategoryTheory.CategoryStruct.comp (SSet.horn (n + 2) 0).ι σ

Lean

Formalized in Tau Ceti as SSet.Quasicategory.hornFilling_zero.

Sources

• Tau Ceti documentation: SSet.Quasicategory.hornFilling_zero
• Source of SSet.Quasicategory.hornFilling_zero in TauCeti/AlgebraicTopology/Quasicategory/OuterHorn.lean

LeanSSet.Quasicategory.hornFilling_zero

TheoremMoore's theorem#

a simplicial set whose sets of simplices are groups, with simplicial operators group homomorphisms, is a Kan complex.

SSet.kanComplex_of_group.{u} {X : _root_.SSet} [(n : SimplexCategoryᵒᵖ) → Group (X.obj n)]
  (hX :
    ∀ ⦃m n : SimplexCategoryᵒᵖ⦄ (f : m ⟶ n) (x y : X.obj m),
      (CategoryTheory.ConcreteCategory.hom (X.map f)) (x * y) =
        (CategoryTheory.ConcreteCategory.hom (X.map f)) x *
          (CategoryTheory.ConcreteCategory.hom (X.map f)) y) :
  X.KanComplex

Lean

Formalized in Tau Ceti as SSet.kanComplex_of_group.

Other forms

Moore's theorem for additive groups. Formalized in Tau Ceti as SSet.kanComplex_of_addGroup.

SSet.kanComplex_of_addGroup.{u} {X : _root_.SSet} [(n : SimplexCategoryᵒᵖ) → AddGroup (X.obj n)]
  (hX :
    ∀ ⦃m n : SimplexCategoryᵒᵖ⦄ (f : m ⟶ n) (x y : X.obj m),
      (CategoryTheory.ConcreteCategory.hom (X.map f)) (x + y) =
        (CategoryTheory.ConcreteCategory.hom (X.map f)) x +
          (CategoryTheory.ConcreteCategory.hom (X.map f)) y) :
  X.KanComplex

Sources

• Tau Ceti documentation: SSet.kanComplex_of_group
• Source of SSet.kanComplex_of_group in TauCeti/AlgebraicTopology/SimplicialSet/KanComplex/SimplicialGroup.lean

LeanSSet.kanComplex_of_group · SSet.kanComplex_of_addGroup

TheoremThe two-set van Kampen theorem for fundamental groupoids#

If the interiors of A and B cover X, the square of fundamental groupoids induced by the inclusions of A ∩ B into A and B and of A and B into X is a pushout in the category of groupoids.

TauCeti.isPushout_fundamentalGroupoid.{u} {X : Type u} [TopologicalSpace X] {A B : Set X}
  (hCover : interior A ∪ interior B = Set.univ) :
  CategoryTheory.IsPushout (FundamentalGroupoid.map (ContinuousMap.inclusion ⋯))
    (FundamentalGroupoid.map (ContinuousMap.inclusion ⋯))
    (FundamentalGroupoid.map (ContinuousMap.subtypeVal A))
    (FundamentalGroupoid.map (ContinuousMap.subtypeVal B))

Lean

Formalized in Tau Ceti as TauCeti.isPushout_fundamentalGroupoid.

Other forms

The two-set van Kampen theorem for fundamental groupoids on a set of basepoints. Formalized in Tau Ceti as TauCeti.isPushout_fundamentalGroupoidOn.

TauCeti.isPushout_fundamentalGroupoidOn.{u} {X : Type u} [TopologicalSpace X] {A B S : Set X}
  (hSA : ∀ x ∈ A, ∃ y ∈ S, JoinedIn A x y) (hSB : ∀ x ∈ B, ∃ y ∈ S, JoinedIn B x y)
  (hSAB : ∀ x ∈ A ∩ B, ∃ y ∈ S, JoinedIn (A ∩ B) x y)
  (hCover : interior A ∪ interior B = Set.univ) :
  CategoryTheory.IsPushout (TauCeti.FundamentalGroupoidOn.map (ContinuousMap.inclusion ⋯) ⋯)
    (TauCeti.FundamentalGroupoidOn.map (ContinuousMap.inclusion ⋯) ⋯)
    (TauCeti.FundamentalGroupoidOn.map (ContinuousMap.subtypeVal A) ⋯)
    (TauCeti.FundamentalGroupoidOn.map (ContinuousMap.subtypeVal B) ⋯)

Sources

• Tau Ceti documentation: TauCeti.isPushout_fundamentalGroupoid
• Source of TauCeti.isPushout_fundamentalGroupoid in TauCeti/AlgebraicTopology/FundamentalGroupoid/Pushout.lean

LeanTauCeti.isPushout_fundamentalGroupoid · TauCeti.isPushout_fundamentalGroupoidOn

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.