14.23 Simplicial objects and… to 14.34 Standard resolutions

Section14.23 Simplicial objects and chain complexes #

Section 14.23 of the Stacks Project, Tag 0194. 9 tags here are carried by 8 declarations of the repository (all in StacksFrontier) and 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0195, a lemma

Tag 0195 in the Stacks Project.

AlgebraicTopology.alternatingFaceMapComplex_preservesHomology, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/MooreComplex.lean, line 370.

Stacks 0195. The Moore complex functor s : Simp(C) ⥤ Ch_{≥0}(C), sending a simplicial object U of a preadditive category C to the chain complex U₀ ← U₁ ← U₂ ← … with differentials the alternating sums of the face maps, is exact: it preserves kernels and cokernels.

public instance alternatingFaceMapComplex_preservesHomology :
    (alternatingFaceMapComplex C).PreservesHomology

Tag 0196, a lemma

Tag 0196 in the Stacks Project.

AlgebraicTopology.DoldKan.acyclic_alternatingFaceMapComplex_Γ₀_double, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/MooreComplex.lean, line 468.

Stacks 0196. The Moore complex of the simplicial object E of [Stacks, Tag 0192], the termwise split extension of K(A, k + 1) by K(A, k), that is Γ₀ of the two-term complex A --𝟙--> A in degrees k + 1 and k, is acyclic.

public theorem acyclic_alternatingFaceMapComplex_Γ₀_double (A : C) (k : ℕ) :
    K[Γ₀.obj (HomologicalComplex.double (𝟙 A)
      (show (ComplexShape.down ℕ).Rel (k + 1) k by simp))].Acyclic

Tag 0197, a lemma

Tag 0197 in the Stacks Project.

AlgebraicTopology.DoldKan.homology_alternatingFaceMapComplex_Γ₀_single, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/MooreComplex.lean, line 478.

Stacks 0197. The Moore complex of the Eilenberg-MacLane object K(A, k) of an object A of an additive category with homology has homology A in degree k and zero homology in every other degree. Here K(A, k) is Γ₀.obj L for L the chain complex A concentrated in degree k.

public theorem homology_alternatingFaceMapComplex_Γ₀_single (A : C) (k : ℕ) :
    IsIsomorphic
        (K[Γ₀.obj ((HomologicalComplex.single C (ComplexShape.down ℕ) k).obj A)].homology k) A ∧
      ∀ i ≠ k, IsZero
        (K[Γ₀.obj ((HomologicalComplex.single C (ComplexShape.down ℕ) k).obj A)].homology i)

Tag 0198, a lemma

Tag 0198 in the Stacks Project.

Declarations registered for the tag:

AlgebraicTopology.inclusionOfMooreComplexMap registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch14.lean, line 76 (StacksFrontier): “the morphism of complexes N(U) -> s(U)”.
AlgebraicTopology.inclusionOfMooreComplexMap_f registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch14.lean, line 78 (StacksFrontier): “its components are the inclusions N(U_n) -> U_n”.

Tag 0199, a lemma

Tag 0199 in the Stacks Project.

AlgebraicTopology.isIsomorphic_normalizedMooreComplex_eilenbergMacLane_single, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/MooreComplex.lean, line 561.

Stacks 0199. The normalized complex N(K(A, k)) of the Eilenberg-MacLane object K(A, k) = i_{k!}U of an object A of an abelian category is isomorphic to the chain complex A concentrated in degree k; in particular N(K(A, k))ᵢ is A for i = k and 0 otherwise.

public theorem isIsomorphic_normalizedMooreComplex_eilenbergMacLane_single (A : C) (k : ℕ) :
    IsIsomorphic ((normalizedMooreComplex C).obj (SimplicialObject.eilenbergMacLane A k))
      ((HomologicalComplex.single C (ComplexShape.down ℕ) k).obj A)

Tag 019A, a lemma

Tag 019A in the Stacks Project.

AlgebraicTopology.exists_degenerateComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/MooreComplex.lean, line 611.

Stacks 019A. Let A be an abelian category. The canonical morphism of chain complexes N(U) ⟶ s(U) from the normalized complex of a simplicial object U of A to its Moore complex is split, functorially in U: there are a functor D from simplicial objects of A to chain complexes, the degenerate part, and a natural isomorphism N ⊞ D ≅ s which on the first summand is the canonical inclusion. In other words s(U) = N(U) ⊕ D(U), naturally in U.

public theorem exists_degenerateComplex :
    ∃ (D : SimplicialObject A ⥤ ChainComplex A ℕ)
      (e : normalizedMooreComplex A ⊞ D ≅ alternatingFaceMapComplex A),
      biprod.inl ≫ e.hom = inclusionOfMooreComplex A

Tag 0FKI, a remark

Tag 0FKI in the Stacks Project.

AlgebraicTopology.exists_degenerateComplex_eq_sup_imageSubobject_σ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/MooreComplex.lean, line 252.

Stacks 0FKI. Let A be an abelian category. The functorial splitting s(U) = N(U) ⊕ D(U) of the Moore complex of a simplicial object U of A along its normalized subcomplex ([Stacks, Tag 019A]) can be chosen so that the degenerate part is described degreewise as the subobject of U_n generated by the degenerate simplices: D(U)_0 = 0 and D(U)_{n + 1} is the supremum of the images of the degeneracy operators σ_i : U_n ⟶ U_{n + 1}, i = 0, …, n. For a simplicial abelian group this says that the elements of D(U)_n are exactly the sums of degenerate n-simplices.

public theorem exists_degenerateComplex_eq_sup_imageSubobject_σ :
    ∃ (D : SimplicialObject A ⥤ ChainComplex A ℕ)
      (e : normalizedMooreComplex A ⊞ D ≅ alternatingFaceMapComplex A),
      biprod.inl ≫ e.hom = inclusionOfMooreComplex A ∧
        ∀ U : SimplicialObject A,
          IsZero ((D.obj U).X 0) ∧
            ∀ n : ℕ, imageSubobject (((biprod.inr ≫ e.hom).app U).f (n + 1)) =
              Finset.univ.sup fun i : Fin (n + 1) => imageSubobject (U.σ i)

Tag 019B, a lemma

Tag 019B in the Stacks Project.

AlgebraicTopology.exactFunctor_normalizedMooreComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/MooreComplex.lean, line 696.

Stacks 019B. The normalized complex functor N : Simp(C) ⥤ Ch_{≥0}(C) of an abelian category C is exact, i.e. it preserves finite limits and finite colimits.

public theorem exactFunctor_normalizedMooreComplex :
    exactFunctor (SimplicialObject C) (ChainComplex C ℕ) (normalizedMooreComplex C)

Tag 019C, a lemma

Tag 019C in the Stacks Project.

AlgebraicTopology.quasiIso_inclusionOfMooreComplexMap_and_acyclic_degenerateComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/MooreComplexQuasiIso.lean, line 70.

Let A be an abelian category and let V be a simplicial object of A. The canonical morphism of chain complexes N(V) ⟶ s(V) is a quasi-isomorphism, and for every functorial splitting e : N ⊞ D ≅ s which on the first summand is the canonical inclusion, the complex D(V) is acyclic.

public theorem quasiIso_inclusionOfMooreComplexMap_and_acyclic_degenerateComplex
    (V : SimplicialObject A) :
    QuasiIso (inclusionOfMooreComplexMap V) ∧
      ∀ (D : SimplicialObject A ⥤ ChainComplex A ℕ)
        (e : normalizedMooreComplex A ⊞ D ≅ alternatingFaceMapComplex A),
        biprod.inl ≫ e.hom = inclusionOfMooreComplex A → (D.obj V).Acyclic

Sources

LeanAlgebraicTopology.alternatingFaceMapComplex_preservesHomology · AlgebraicTopology.DoldKan.acyclic_alternatingFaceMapComplex_Γ₀_double · AlgebraicTopology.DoldKan.homology_alternatingFaceMapComplex_Γ₀_single · AlgebraicTopology.inclusionOfMooreComplexMap · AlgebraicTopology.inclusionOfMooreComplexMap_f · AlgebraicTopology.isIsomorphic_normalizedMooreComplex_eilenbergMacLane_single · AlgebraicTopology.exists_degenerateComplex · AlgebraicTopology.exists_degenerateComplex_eq_sup_imageSubobject_σ

Section14.24 Dold-Kan #

Section 14.24 of the Stacks Project, Tag 019D. 3 tags here are carried by 2 declarations of the repository (all in StacksFrontier) and 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 019E, a lemma

Tag 019E in the Stacks Project.

AlgebraicTopology.normalizedMooreComplex_faithful, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/DoldKan/Equivalence.lean, line 50.

Stacks 019E. The normalized complex functor N : Simp(A) ⥤ Ch_{≥0}(A) of an abelian category A, sending a simplicial object U to the complex of normalized chains N(U)_m = ⋂_i Ker(d^m_i), is faithful. Consequently it reflects monomorphisms, epimorphisms and isomorphisms.

public instance normalizedMooreComplex_faithful :
    (normalizedMooreComplex A).Faithful

Tag 019F, a lemma

Tag 019F in the Stacks Project.

CategoryTheory.Equivalence.exists_of_faithful_of_essSurj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/DoldKan/Equivalence.lean, line 134.

Stacks 019F. For abelian categories A and B and exact functors N : A ⥤ B, S : B ⥤ A with a natural isomorphism g : S ⋙ N ≅ 𝟭 B, N faithful and S essentially surjective, N and S are quasi-inverse equivalences of categories: there is an equivalence A ≌ B whose functor is N and whose inverse functor is S.

theorem Equivalence.exists_of_faithful_of_essSurj
    {A B : Type*} [Category A] [Category B] [Abelian A] [Abelian B]
    (N : A ⥤ B) (S : B ⥤ A)
    (g : S ⋙ N ≅ 𝟭 B)
    (hN_faithful : N.Faithful)
    (hS_essSurj : S.EssSurj) :
    ∃ e : A ≌ B, e.functor = N ∧ e.inverse = S

Tag 019G, a theorem

Tag 019G in the Stacks Project.

Declarations registered for the tag:

CategoryTheory.Abelian.DoldKan.equivalence registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch14.lean, line 80 (StacksFrontier): “the equivalence Simp(A) ≌ Ch_{≥0}(A)”.
CategoryTheory.Abelian.DoldKan.equivalence_functor registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch14.lean, line 82 (StacksFrontier): “the functor of the equivalence is N”.

Sources

LeanAlgebraicTopology.normalizedMooreComplex_faithful · CategoryTheory.Equivalence.exists_of_faithful_of_essSurj · CategoryTheory.Abelian.DoldKan.equivalence · CategoryTheory.Abelian.DoldKan.equivalence_functor

Section14.25 Dold-Kan for cosimplicial objects #

Section 14.25 of the Stacks Project, Tag 019H. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 019I, a lemma

Tag 019I in the Stacks Project.

AlgebraicTopology.exists_normalizedCochainComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/DoldKan/Cosimplicial.lean, line 450. References: SGA 4 XVII (5.5.3), “Dold–Puppe equivalence”; SGA 4½ Fonctions L (1.4), “N is an equivalence”.

Stacks 019I. Let A be an abelian category. (1) The Moore cochain complex functor s : CoSimp(A) ⥤ CoCh_{≥0}(A) is exact. (2) There is a functor Q, the normalized cochain complex, together with a natural transformation π : s ⟶ Q which is an isomorphism in degree 0 and, in degree n + 1, a cokernel of the cofaces δ i : Uₙ ⟶ Uₙ₊₁, i ≤ n. (3) π is a split epimorphism in the functor category, which is the functorial direct sum decomposition s(U) = D(U) ⊕ Q(U) with D = ker π. (4) Q is exact. (5) Each π.app U is a quasi-isomorphism. (6) Q is an equivalence of categories.

public theorem exists_normalizedCochainComplex :
    (PreservesFiniteLimits (alternatingCofaceMapComplex A) ∧
      PreservesFiniteColimits (alternatingCofaceMapComplex A)) ∧
    ∃ (Q : CosimplicialObject A ⥤ CochainComplex A ℕ)
      (π : alternatingCofaceMapComplex A ⟶ Q),
      (∀ U : CosimplicialObject A, IsIso ((π.app U).f 0)) ∧
      (∀ (U : CosimplicialObject A) (n : ℕ),
        ∃ e : cokernel (Sigma.desc (f := fun _ : Fin (n + 1) => U.obj ⦋n⦌)
            fun i => U.δ i.castSucc) ≅ (Q.obj U).X (n + 1),
          cokernel.π _ ≫ e.hom = (π.app U).f (n + 1)) ∧
      IsSplitEpi π ∧
      (PreservesFiniteLimits Q ∧ PreservesFiniteColimits Q) ∧
      (∀ U : CosimplicialObject A, QuasiIso (π.app U)) ∧
      Q.IsEquivalence

Sources

LeanAlgebraicTopology.exists_normalizedCochainComplex

Section14.26 Homotopies #

Section 14.26 of the Stacks Project, Tag 019J. 9 tags here are carried by 10 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 019K, a definition

Tag 019K in the Stacks Project.

CategoryTheory.SimplicialObject.IsHomotopy, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/SimplicialObject/Homotopy/Basic.lean, line 78. The attribute's comment: “part (1); part (2), being homotopic, is the equivalence relation Relation.EqvGen (fun a b ↦ ∃ h, IsHomotopy h a b) generated by it, see the module docstring”. References: SGA 4 Vbis (3.0.2).

Stacks 019K (part 1). Given simplicial objects U, V of a category C for which the product U × Δ[1] = U.copower Δ[1] of [Stacks, Tag 017C] exists, a morphism h : U × Δ[1] ⟶ V is a homotopy from a to b for a, b : U ⟶ V when a = e₀ ≫ h and b = e₁ ≫ h, where e₀, e₁ : U ⟶ U × Δ[1] come from the two vertices Δ[0] ⟶ Δ[1] and the identification U × Δ[0] = U. In degree m these two vertex inclusions are the inclusions of the summands of ∐_{α ∈ Δ[1]_m} U_m indexed by the constant m-simplices SSet.stdSimplex.const 1 0 m and SSet.stdSimplex.const 1 1 m of Δ[1], which is how the two conditions are spelled here; equivalently, h_{m, m + 1} = a_m and h_{m, 0} = b_m in the notation of [Stacks, Tag 019L].

public def IsHomotopy (h : U.copower Δ[1] ⟶ V) (a b : U ⟶ V) : Prop

Tag 019L, a lemma

Tag 019L in the Stacks Project.

CategoryTheory.SimplicialObject.htpy_forward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/SimplicialObject/Homotopy/Basic.lean, line 242.

Stacks 019L. The components h_{n, i} of a homotopy h : U × Δ[1] ⟶ V from a to b satisfy the relations HtpyRel a b.

theorem htpy_forward {U V : SimplicialObject C}
    [∀ m, HasCoproduct fun _ : (Δ[1] : SSet.{w}).obj m => U.obj m] (a b : U ⟶ V)
    (h : U.copower Δ[1] ⟶ V) (hh : IsHomotopy h a b) :
    HtpyRel a b (homotopyComponent h)

CategoryTheory.SimplicialObject.htpy_converse, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/SimplicialObject/Homotopy/Basic.lean, line 431.

Stacks 019L. Given a family of morphisms hc n i : U_n ⟶ V_n satisfying the relations HtpyRel a b, there is a unique morphism of simplicial objects h : U × Δ[1] ⟶ V whose components are the given hc, and it is a homotopy from a to b.

theorem htpy_converse {U V : SimplicialObject C}
    [∀ m, HasCoproduct fun _ : (Δ[1] : SSet.{w}).obj m => U.obj m] (a b : U ⟶ V)
    (hc : ∀ (n : ℕ), Fin (n + 2) →
      (U.obj (op (SimplexCategory.mk n)) ⟶ V.obj (op (SimplexCategory.mk n))))
    (hrel : HtpyRel a b hc) :
    ∃! h : U.copower Δ[1] ⟶ V,
      IsHomotopy h a b ∧ (∀ (n : ℕ) (i : Fin (n+2)), homotopyComponent h n i = hc n i)

Tag 019M, a remark

Tag 019M in the Stacks Project.

CategoryTheory.SimplicialObject.IsHomotopy.exists_whiskerRight, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/SimplicialObject/Homotopy/Basic.lean, line 585. The attribute's comment: “the remark's concluding deduction: a functor preserves the notion of homotopy of 019K whenever the two products with Δ[1] exist, with the transported homotopy pinned to the family {F(h_{n, i})} rather than merely asserted to exist. The remark's other content is already in Mathlib or is a composite of existing declarations, see the module docstring: the notion of homotopy for an arbitrary category is SimplicialObject.Homotopy, its preservation by a functor is SimplicialObject.Homotopy.whiskerRight, and being homotopic is Relation.EqvGen fun a b => ∃ h, IsHomotopy h a b as in 019K”.

Stacks 019M. Functors preserve homotopies of simplicial objects. Let F : C ⥤ D be any functor between any two categories, let U, V be simplicial objects of C, and let a, b : U ⟶ V. If k : U × Δ[1] ⟶ V is a homotopy from a to b in the sense of [Stacks, Tag 019K], then there is a homotopy l : F(U) × Δ[1] ⟶ F(V) from F(a) to F(b) whose component at each simplex α ∈ Δ[1]_m is F applied to the component of k at α; in the notation of [Stacks, Tag 019L], l is the family {F(h_{m, i})}. No compatibility of F with the coproducts making up the two products with Δ[1] is required.

public theorem IsHomotopy.exists_whiskerRight {U V : SimplicialObject C}
    [∀ m, HasCoproduct fun _ : (Δ[1] : SSet.{w}).obj m => U.obj m] (F : C ⥤ D)
    [∀ m, HasCoproduct fun _ : (Δ[1] : SSet.{w}).obj m => (U ⋙ F).obj m]
    {a b : U ⟶ V} {k : U.copower Δ[1] ⟶ V} (hk : IsHomotopy k a b) :
    ∃ l : (U ⋙ F).copower Δ[1] ⟶ V ⋙ F,
      (∀ (m : SimplexCategoryᵒᵖ) (α : (Δ[1] : SSet.{w}).obj m),
          Sigma.ι (fun _ : (Δ[1] : SSet.{w}).obj m => (U ⋙ F).obj m) α ≫ l.app m =
            F.map (Sigma.ι (fun _ : (Δ[1] : SSet.{w}).obj m => U.obj m) α ≫ k.app m)) ∧
        IsHomotopy l (Functor.whiskerRight a F) (Functor.whiskerRight b F)

Tag 08RJ, a remark

Tag 08RJ in the Stacks Project.

CategoryTheory.SimplicialObject.congruence_homotopic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/SimplicialObject/Homotopy/Basic.lean, line 731.

Stacks 08RJ. Let C be any category. Being homotopic — the equivalence relation on morphisms of simplicial objects of C generated by the existence of a simplicial homotopy — is a congruence: if a and a' are homotopic then so are b ∘ a and b ∘ a' for any b : V ⟶ W, and so are a ∘ c and a' ∘ c for any c : X ⟶ U. Hence CategoryTheory.Quotient of this relation is the source's hSimp(C), the category whose objects are the simplicial objects of C and whose morphisms are the homotopy classes of morphisms of simplicial objects, and CategoryTheory.Quotient.functor is the canonical functor Simp(C) ⟶ hSimp(C), essentially surjective and surjective on sets of morphisms.

public theorem congruence_homotopic :
    Congruence fun (U V : SimplicialObject C) (a a' : U ⟶ V) ↦
      Relation.EqvGen (fun a a' : U ⟶ V ↦ Nonempty (Homotopy a a')) a a'

Tag 019N, a definition

Tag 019N in the Stacks Project.

CategoryTheory.SimplicialObject.homotopyEquivalences, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/SimplicialObject/Homotopy/Basic.lean, line 652. The attribute's comment: “the first sentence; being homotopy equivalent, the second sentence, is the composite ∃ a : U ⟶ V, homotopyEquivalences C a and gets no name, as in Mathlib for complexes, where it is Nonempty (HomotopyEquiv K L). Stated as a MorphismProperty, the shape of the sibling HomologicalComplex.homotopyEquivalences; being homotopic is Relation.EqvGen fun f g => Nonempty (Homotopy f g) as in 019S”.

Stacks 019N (the first sentence). Let C be any category. A morphism a : U ⟶ V of simplicial objects of C is a homotopy equivalence if there is a morphism b : V ⟶ U such that a ≫ b is homotopic to 𝟙 U and b ≫ a is homotopic to 𝟙 V, where two morphisms are homotopic when they are related by the equivalence relation generated by the existence of a simplicial homotopy ([Stacks, Tag 019M]). The simplicial objects U and V are homotopy equivalent when some a : U ⟶ V is a homotopy equivalence, that is, when ∃ a : U ⟶ V, homotopyEquivalences C a.

public def homotopyEquivalences : MorphismProperty (SimplicialObject C)

Tag 08Q3, an example

Tag 08Q3 in the Stacks Project.

SSet.stdSimplex.homotopyEquivalences_hom_obj₀, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/SimplicialObject/Homotopy/Equivalence.lean, line 793. The attribute's comment: “the homotopy equivalence, with the homotopy 𝟙 ⟹ f ≫ g for g the last vertex; g ≫ f = 𝟙 is SSet.stdSimplex.ext₀, as Δ[0] is terminal”.

The standard simplex Δ[m] is homotopy equivalent to Δ[0]. The unique morphism f : Δ[m] ⟶ Δ[0] is a homotopy equivalence of simplicial objects ([Stacks, Tag 019N]): a homotopy inverse is the inclusion g : Δ[0] ⟶ Δ[m] of the last 0-simplex of Δ[m], for which g ≫ f = 𝟙 Δ[0] and, as the second conjunct records, 𝟙 Δ[m] is homotopic to f ≫ g = SSet.const (obj₀Equiv.symm (Fin.last m)) by a homotopy in that direction, namely (φ, α) ↦ (k ↦ if α k = 0 then φ k else m).

public theorem homotopyEquivalences_hom_obj₀ (m : ℕ) :
    (∀ f : (Δ[m] : SSet.{u}) ⟶ Δ[0],
        SimplicialObject.homotopyEquivalences (Type u) f) ∧
      Nonempty (SSet.Homotopy (𝟙 (Δ[m] : SSet.{u}))
        (SSet.const (obj₀Equiv.symm (Fin.last m))))

Tag 019O, a lemma

Tag 019O in the Stacks Project.

CategoryTheory.SimplicialObject.homotopyEquivalence_proj_cylinder, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/SimplicialObject/Homotopy/Equivalence.lean, line 478. The attribute's comment: “the cylinder is any object with the universal property of U × Δ[1], in place of a chosen construction, so that the source's finite coproducts on C are weakened to the coproducts making it up; the maps of [Stacks, Tag 017E] are pinned by their characterizing equations instead of being reconstructed; and the two homotopies are directed, as the source's proof produces them, which is stronger than the source's symmetric are homotopic”.

The projection from the cylinder U × Δ[1] is a homotopy equivalence, with either vertex inclusion as a homotopy inverse. Let U be a simplicial object of a category C, and let X be a cylinder on U: a simplicial object together with morphisms ι m α : U_m ⟶ X_m, one for each m-simplex α of Δ[1], which exhibit X_m as the coproduct ∐_{α ∈ Δ[1]_m} U_m and satisfy ι m α ≫ X(φ) = U(φ) ≫ ι m' (Δ[1](φ) α); this is the product U × Δ[1] of [Stacks, Tag 017C]. Let π : X ⟶ U be the projection, the identity on each summand, and let e₀, e₁ : U ⟶ X be the two vertex inclusions, in degree m the inclusions of the summands indexed by the constant m-simplices SSet.stdSimplex.const 1 0 m and SSet.stdSimplex.const 1 1 m of Δ[1]. Then π ∘ e₀ = π ∘ e₁ = id_U, the composite e₀ ∘ π admits a homotopy to id_X, and id_X admits a homotopy to e₁ ∘ π. In particular π is a homotopy equivalence ([Stacks, Tag 019N]), so U × Δ[1] is homotopy equivalent to U.

public theorem homotopyEquivalence_proj_cylinder
    (ι : ∀ m : SimplexCategoryᵒᵖ, (Δ[1] : SSet.{w}).obj m → (U.obj m ⟶ X.obj m))
    (hX : ∀ m : SimplexCategoryᵒᵖ,
      IsColimit (Cofan.mk (f := fun _ : (Δ[1] : SSet.{w}).obj m => U.obj m) (X.obj m) (ι m)))
    (hι : ∀ {m m' : SimplexCategoryᵒᵖ} (φ : m ⟶ m') (α : (Δ[1] : SSet.{w}).obj m),
      ι m α ≫ X.map φ = U.map φ ≫ ι m' ((Δ[1] : SSet.{w}).map φ α))
    (π : X ⟶ U) (e₀ e₁ : U ⟶ X)
    (hπ : ∀ (m : SimplexCategoryᵒᵖ) (α : (Δ[1] : SSet.{w}).obj m),
      ι m α ≫ π.app m = 𝟙 (U.obj m))
    (he₀ : ∀ m : SimplexCategoryᵒᵖ, e₀.app m = ι m (stdSimplex.const 1 0 m))
    (he₁ : ∀ m : SimplexCategoryᵒᵖ, e₁.app m = ι m (stdSimplex.const 1 1 m)) :
    (e₀ ≫ π = 𝟙 U ∧ e₁ ≫ π = 𝟙 U) ∧
      Nonempty (Homotopy (π ≫ e₀) (𝟙 X)) ∧ Nonempty (Homotopy (𝟙 X) (π ≫ e₁))

Tag 019P, a lemma

Tag 019P in the Stacks Project.

CategoryTheory.Arrow.nonempty_homotopy_mapCechNerve_id, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/SimplicialObject/Homotopy/Equivalence.lean, line 718. The attribute's comment: “the first sentence, stated for an arbitrary endomorphism F of the arrow f with f.hom ≫ F.right = f.hom, of which the source's self map is the case F = (f.hom ≫ s, 𝟙 X) for a section s of f; the self map is pinned as Arrow.mapCechNerve F, and the conclusion is the existence of a homotopy, which is stronger than the source's homotopic of 019M. The second sentence, that U is homotopy equivalent to the constant simplicial object X, uses the section and is a formal consequence, to be tagged jointly on a second declaration; see the module docstring”.

A self map of a Čech nerve which is the identity on the base is homotopic to the identity. Let f : Y ⟶ X be an arrow of a category C whose iterated fibre products Y ×_X ⋯ ×_X Y exist, let U = f.cechNerve be the simplicial object of [Stacks, Tag 016E] built from f, and let F be an endomorphism of the arrow f with f ≫ F.right = f, so that the induced self map Arrow.mapCechNerve F of U, given by F.left on each factor Y, is the identity on the base X. Then there is a simplicial homotopy from that self map to 𝟙 U in the sense of [Stacks, Tag 019M]; in particular the two are homotopic.

public theorem nonempty_homotopy_mapCechNerve_id {f : Arrow C}
    [∀ n : ℕ, HasWidePullback f.right (fun _ : Fin (n + 1) => f.left) fun _ => f.hom]
    (F : f ⟶ f) (hF : f.hom ≫ F.right = f.hom) :
    Nonempty (SimplicialObject.Homotopy (mapCechNerve F) (𝟙 f.cechNerve))

Tag 08Q4, a lemma

Tag 08Q4 in the Stacks Project.

CategoryTheory.SimplicialObject.nonempty_homotopy_and_homotopyEquivalences_of_isLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/SimplicialObject/Homotopy/Equivalence.lean, line 1000. The attribute's comment: “the three conjuncts are parts (2), (3), (1), in that order. The products are pinned degreewise by limit fans, as in [Stacks, Tag 016Q], instead of by HasProduct in SimplicialObject C, and f = ∏ a_t, g = ∏ b_t by their characterizing equations. Part (1) is stated in the stronger form that the product of homotopy equivalences is one, the source's homotopy equivalent following by choice; part (3) is stated with the weaker hypothesis that only finitely many coordinates differ. See the module docstring”.

Products of homotopies and of homotopy equivalences of simplicial objects. Let X t, Y t (t : T) be families of simplicial objects of a category C, and let p t : P ⟶ X t and q t : Q ⟶ Y t exhibit P and Q as the products ∏_t X t and ∏_t Y t, that is, degreewise products in the sense of [Stacks, Tag 016Q]. Let a t, b t : X t ⟶ Y t be morphisms and let f, g : P ⟶ Q be their products, pinned by f ≫ q t = p t ≫ a t and g ≫ q t = p t ≫ b t. Then: * if there is a homotopy from a t to b t for every t, there is a homotopy from f to g (part (2), no finiteness needed); * if a t and b t are homotopic for every t and a t = b t for all but finitely many t, then f and g are homotopic (part (3)); * if T is finite and every a t is a homotopy equivalence, then f is a homotopy equivalence, so ∏_t X t and ∏_t Y t are homotopy equivalent (part (1)).

public theorem nonempty_homotopy_and_homotopyEquivalences_of_isLimit
    {T : Type w} {X Y : T → SimplicialObject C} {P Q : SimplicialObject C}
    (p : ∀ t, P ⟶ X t) (q : ∀ t, Q ⟶ Y t)
    (hP : ∀ n : SimplexCategoryᵒᵖ, IsLimit (Fan.mk (P.obj n) fun t => (p t).app n))
    (hQ : ∀ n : SimplexCategoryᵒᵖ, IsLimit (Fan.mk (Q.obj n) fun t => (q t).app n))
    {a b : ∀ t, X t ⟶ Y t} {f g : P ⟶ Q}
    (hf : ∀ t, f ≫ q t = p t ≫ a t) (hg : ∀ t, g ≫ q t = p t ≫ b t) :
    ((∀ t, Nonempty (Homotopy (a t) (b t))) → Nonempty (Homotopy f g)) ∧
      ({t | a t ≠ b t}.Finite →
        (∀ t, Relation.EqvGen (fun u v : X t ⟶ Y t => Nonempty (Homotopy u v)) (a t) (b t)) →
          Relation.EqvGen (fun u v : P ⟶ Q => Nonempty (Homotopy u v)) f g) ∧
      (Finite T → (∀ t, homotopyEquivalences C (a t)) → homotopyEquivalences C f)

Sources

LeanCategoryTheory.SimplicialObject.IsHomotopy · CategoryTheory.SimplicialObject.htpy_forward · CategoryTheory.SimplicialObject.htpy_converse · CategoryTheory.SimplicialObject.IsHomotopy.exists_whiskerRight · CategoryTheory.SimplicialObject.congruence_homotopic · CategoryTheory.SimplicialObject.homotopyEquivalences · SSet.stdSimplex.homotopyEquivalences_hom_obj₀ · CategoryTheory.SimplicialObject.homotopyEquivalence_proj_cylinder

Section14.27 Homotopies in abelian categories #

Section 14.27 of the Stacks Project, Tag 019Q. 3 tags here are carried by 3 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 019R, an equation

Tag 019R in the Stacks Project.

Declarations registered for the tag:

CategoryTheory.SimplicialObject.Homotopy.ToChainHomotopy.hom_eq registered with add_to_stacks in StacksFrontier/AlgebraicTopology/SimplicialObject/ChainHomotopy.lean, line 58 (StacksFrontier): “the components of the chain homotopy s(h) = toChainHomotopy induced by a simplicial homotopy h, with the sign (-1)^{i+1} pulled out of the sum and h.h i denoting the composite h_{n+1,i+1} ∘ sⁿᵢ”.

Tag 019S, a lemma

Tag 019S in the Stacks Project.

AlgebraicTopology.homotopic_normalizedMooreComplex_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/SimplicialObject/ChainHomotopy.lean, line 196. The attribute's comment: “the half about the Moore complex s is Mathlib's, so it gets no public name here: a homotopy gives SimplicialObject.Homotopy.toChainHomotopy, and homotopy_congruence propagates it along the source's chain; stated here is the half about N. homotopic is Mathlib's chain homotopy relation, and being homotopic is spelled Relation.EqvGen fun a b => Nonempty (Homotopy a b) as in 019W”. References: SGA 4½ Fonctions L (1.4), “N preserves homotopy”.

Homotopic morphisms have chain homotopic normalized Moore complexes. If a, b : U ⟶ V are homotopic morphisms of simplicial objects of an abelian category A — related by a chain of morphisms consecutive members of which admit a simplicial homotopy in one direction or the other — then the induced maps N(a), N(b) : N(U) ⟶ N(V) of normalized Moore complexes are chain homotopic.

public theorem homotopic_normalizedMooreComplex_map
    (h : Relation.EqvGen (fun a b : U ⟶ V => Nonempty (Homotopy a b)) a b) :
    homotopic A (ComplexShape.down ℕ)
      ((normalizedMooreComplex A).map a) ((normalizedMooreComplex A).map b)

Tag 019T, a lemma

Tag 019T in the Stacks Project.

AlgebraicTopology.homotopyEquivalences_alternatingFaceMapComplex_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/SimplicialObject/ChainHomotopy.lean, line 218. The attribute's comment: “the first sentence, for the Moore complex s, with the source's additive weakened to Preadditive, Mathlib's hypothesis for alternatingFaceMapComplex; the second sentence is homotopyEquivalences_normalizedMooreComplex_map below. Being a homotopy equivalence of chain complexes is HomologicalComplex.homotopyEquivalences, which pins the map, and the hypothesis is 019N's SimplicialObject.homotopyEquivalences”.

The Moore complex of a homotopy equivalence of simplicial objects is a homotopy equivalence of chain complexes. Let a : U ⟶ V be a homotopy equivalence of simplicial objects of a preadditive category A: there is b : V ⟶ U with a ≫ b homotopic to 𝟙 U and b ≫ a homotopic to 𝟙 V, homotopic meaning related by the equivalence relation generated by the existence of a simplicial homotopy ([Stacks, Tag 019N]). Then s(a) : s(U) ⟶ s(V) is a homotopy equivalence of chain complexes.

public theorem homotopyEquivalences_alternatingFaceMapComplex_map [Preadditive A]
    (ha : SimplicialObject.homotopyEquivalences A a) :
    HomologicalComplex.homotopyEquivalences A (ComplexShape.down ℕ)
      ((alternatingFaceMapComplex A).map a)

AlgebraicTopology.homotopyEquivalences_normalizedMooreComplex_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/SimplicialObject/ChainHomotopy.lean, line 239. The attribute's comment: “the second sentence, for the normalized Moore complex N; the first is homotopyEquivalences_alternatingFaceMapComplex_map above, from which this one is deduced by conjugating with the natural homotopy equivalence inclusionOfMooreComplexMap. Only Abelian A is assumed, which provides the preadditivity the source's additive asks for. Being a homotopy equivalence of chain complexes is HomologicalComplex.homotopyEquivalences, which pins the map, and the hypothesis is 019N's SimplicialObject.homotopyEquivalences”.

The normalized Moore complex of a homotopy equivalence of simplicial objects is a homotopy equivalence of chain complexes. Let a : U ⟶ V be a homotopy equivalence of simplicial objects of an abelian category A ([Stacks, Tag 019N]). Then N(a) : N(U) ⟶ N(V) is a homotopy equivalence of chain complexes.

public theorem homotopyEquivalences_normalizedMooreComplex_map [Abelian A]
    (ha : SimplicialObject.homotopyEquivalences A a) :
    HomologicalComplex.homotopyEquivalences A (ComplexShape.down ℕ)
      ((normalizedMooreComplex A).map a)

Sources

LeanCategoryTheory.SimplicialObject.Homotopy.ToChainHomotopy.hom_eq · AlgebraicTopology.homotopic_normalizedMooreComplex_map · AlgebraicTopology.homotopyEquivalences_alternatingFaceMapComplex_map · AlgebraicTopology.homotopyEquivalences_normalizedMooreComplex_map

Section14.28 Homotopies and cosimplicial objects #

Section 14.28 of the Stacks Project, Tag 019U. 8 tags here are carried by 8 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 019W, a definition

Tag 019W in the Stacks Project.

CategoryTheory.CosimplicialObject.Homotopy, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/SimplicialObject/Homotopy/Cosimplicial.lean, line 956. The attribute's comment: “the finite products of the source are replaced by the products that name Hom(Δ[1], V); the two conditions a = e₀ ∘ h, b = e₁ ∘ h are recorded degreewise, e₀ and e₁ being pinned there to the two projections; part (2), homotopic, is Relation.EqvGen fun a b => Nonempty (Homotopy a b)”. References: SGA 4 Vbis (3.0.2.2), “Dual form, special case”.

Stacks 019W. A homotopy from a to b, for a b : U ⟶ V two morphisms of cosimplicial objects of C: a morphism h : U ⟶ Hom(Δ[1], V) into the cosimplicial object Hom(Δ[1], V) = V.power Δ[1] of [Stacks, Tag 019V] such that a = e₀ ∘ h and b = e₁ ∘ h, where e₀, e₁ : Hom(Δ[1], V) ⟶ V are induced by the two vertices of Δ[1]. The two conditions are recorded in each degree n, where e₀ and e₁ are the projections of Hom(Δ[1], V)_n = ∏_{α ∈ Δ[1]_n} V_n onto the factors indexed by the constant maps [n] → [1] with value 0, resp. 1; so the components h_{n, α} : U_n ⟶ V_n of h satisfy a_n = h_{n, 0} and b_n = h_{n, 1}, and the naturality of h is the compatibility of the h_{n, α} with the structure maps.

public structure Homotopy (a b : U ⟶ V) : Type v

Tag 07KB, an equation

Tag 07KB in the Stacks Project.

CategoryTheory.CosimplicialObject.exists_hom_power_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/SimplicialObject/Homotopy/Cosimplicial.lean, line 1064. The attribute's comment: “stated for an arbitrary simplicial set K in place of Δ[1], and as the criterion characterising the families of morphisms that assemble into a morphism U ⟶ Hom(K, V), which is what the source's paragraph asserts in both directions”.

Stacks 07KB. A family of morphisms h_{n, α} : U_n ⟶ V_n of C, indexed by the simplices α ∈ K_n of a simplicial set K, is the family of components of a morphism H : U ⟶ Hom(K, V) of cosimplicial objects, with H_n = ∏_{α ∈ K_n} h_{n, α}, if and only if h_{m, α} ∘ U(f) = V(f) ∘ h_{n, α ∘ f} for every morphism f : [n] → [m] of Δ and every α ∈ K_m, where α ∘ f = K(f)(α).

public theorem exists_hom_power_iff
    (h : ∀ n : SimplexCategory, K.obj (op n) → (U.obj n ⟶ V.obj n)) :
    (∃ H : U ⟶ V.power K, ∀ n, H.app n = Pi.lift (h n)) ↔
      ∀ ⦃n m : SimplexCategory⦄ (f : n ⟶ m) (α : K.obj (op m)),
        U.map f ≫ h m α = h n (K.map f.op α) ≫ V.map f

Tag 0FKJ, a remark

Tag 0FKJ in the Stacks Project.

CategoryTheory.CosimplicialObject.exists_homotopy_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/SimplicialObject/Homotopy/Cosimplicial.lean, line 1157. The attribute's comment: “the remark's comparison of its notion with the one of 019W, this new notion is the same as the old one in case finite products exist, stated for a given family and with the correspondence pinned degreewise to h_n = ∏_α h_{n, α}; the finite products of 019W are weakened to the products naming Hom(Δ[1], V), and the right hand side, which needs no products, is the remark's definition, in the form its dependents use. Part (2), homotopic, is Relation.EqvGen of the existence of such a family, as in 019W and 019S; the remark's functoriality assertions are 019Y (2)”.

Stacks 0FKJ. A homotopy from a to b, for a b : U ⟶ V morphisms of cosimplicial objects of a category C with no assumptions whatsoever, is a family of morphisms h_{n, α} : U_n ⟶ V_n indexed by the objects ⦋n⦌ of Δ and the simplices α ∈ Δ[1]_n, satisfying h_{m, α} ∘ U(f) = V(f) ∘ h_{n, α ∘ f} for every morphism f : ⦋n⦌ ⟶ ⦋m⦌ of Δ ([Stacks, Tag 07KB]) and having a_n and b_n as its components at the two constant maps ⦋n⦌ ⟶ ⦋1⦌, with value 0 resp. 1. This notion agrees with the one of [Stacks, Tag 019W], which needs the products ∏_{α ∈ Δ[1]_n} V_n naming Hom(Δ[1], V): whenever those exist, a family is a homotopy in the above sense if and only if it is the family of components of a homotopy h : U ⟶ Hom(Δ[1], V) from a to b, with h_n = ∏_{α ∈ Δ[1]_n} h_{n, α}.

public theorem exists_homotopy_iff (a b : U ⟶ V)
    (h : ∀ n : SimplexCategory, (Δ[1] : SSet.{0}).obj (op n) → (U.obj n ⟶ V.obj n)) :
    (∃ H : Homotopy a b, ∀ n, H.h.app n = Pi.lift (h n)) ↔
      (∀ ⦃n m : SimplexCategory⦄ (f : n ⟶ m) (α : (Δ[1] : SSet.{0}).obj (op m)),
          U.map f ≫ h m α = h n ((Δ[1] : SSet.{0}).map f.op α) ≫ V.map f) ∧
        (∀ n : SimplexCategory, h n (stdSimplex.const 1 0 (op n)) = a.app n) ∧
        (∀ n : SimplexCategory, h n (stdSimplex.const 1 1 (op n)) = b.app n)

Tag 019X, a lemma

Tag 019X in the Stacks Project.

CategoryTheory.CosimplicialObject.exists_homotopy_iff_nonempty_homotopy_op, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/SimplicialObject/Homotopy/Cosimplicial.lean, line 414. The attribute's comment: “the equivalence of (1) and (2); the primed objects are spelled U.op and NatTrans.op a rather than through cosimplicialSimplicialEquiv, a homotopy as in 0FKJ by its family of components as in 07KB, and a homotopy as in 019M by Mathlib's SimplicialObject.Homotopy, so that neither side needs (co)products and the statement holds over an arbitrary category. The final assertion, homotopic if and only if homotopic, is the equivalence of the Relation.EqvGen of the two sides and is formal from this one, by transport along the bijection NatTrans.op : (U ⟶ V) ≃ (V.op ⟶ U.op); it is what 019Y (2) and (4) apply”.

Stacks 019X. A homotopy of morphisms of cosimplicial objects is a simplicial homotopy in the opposite category. Let C be a category with no assumptions whatsoever, let U, V be cosimplicial objects of C and let a, b : U ⟶ V, so that U, V correspond to simplicial objects U.op, V.op of Cᵒᵖ and a, b to morphisms aᵒᵖ, bᵒᵖ : V.op ⟶ U.op. Then there exists a homotopy {h_{n, α}} from a to b in the sense of [Stacks, Tag 0FKJ] — a family of morphisms h_{n, α} : U_n ⟶ V_n, indexed by the simplices α ∈ Δ[1]_n, satisfying h_{m, α} ∘ U(f) = V(f) ∘ h_{n, α ∘ f} for every morphism f : ⦋n⦌ ⟶ ⦋m⦌ of Δ and having a_n, b_n as its components at the two constant maps ⦋n⦌ ⟶ ⦋1⦌ — if and only if there exists a homotopy {h_{n, i}} from aᵒᵖ to bᵒᵖ in the sense of [Stacks, Tag 019M]. Hence a and b are homotopic if and only if aᵒᵖ and bᵒᵖ are, the two relations being the equivalence relations generated by these two existence statements.

public theorem exists_homotopy_iff_nonempty_homotopy_op {U V : CosimplicialObject C}
    (a b : U ⟶ V) :
    (∃ h : ∀ n : SimplexCategory, (Δ[1] : SSet.{0}).obj (op n) → (U.obj n ⟶ V.obj n),
        (∀ ⦃n m : SimplexCategory⦄ (f : n ⟶ m) (α : (Δ[1] : SSet.{0}).obj (op m)),
            U.map f ≫ h m α = h n ((Δ[1] : SSet.{0}).map f.op α) ≫ V.map f) ∧
          (∀ n : SimplexCategory, h n (stdSimplex.const 1 0 (op n)) = a.app n) ∧
          (∀ n : SimplexCategory, h n (stdSimplex.const 1 1 (op n)) = b.app n)) ↔
      Nonempty (SimplicialObject.Homotopy (NatTrans.op a) (NatTrans.op b))

Tag 019Y, a lemma

Tag 019Y in the Stacks Project.

CategoryTheory.homotopic_whiskerRight, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/SimplicialObject/Homotopy/Cosimplicial.lean, line 462. The attribute's comment: “all four parts, at the chain level: homotopic is Relation.EqvGen of the existence of a homotopy, as in 019K, 019W and 0FKJ. Homotopy of simplicial objects over an arbitrary category is SimplicialObject.Homotopy (Mathlib), the notion of 019M through the composites of the source's footnote; homotopy of cosimplicial objects is the family of 0FKJ, repeated verbatim. The source's four categories occur as they do there, each part binding the two it names, so that each part applies on its own; the four are one conjunction because they are one assertion read in four dualities. The passage between variances is Functor.rightOp/Functor.op and NatTrans.rightOp/NatTrans.op, the anti-equivalences simplicialCosimplicialEquiv and cosimplicialSimplicialEquiv”.

Stacks 019Y. Functors preserve homotopic morphisms of (co)simplicial objects. Let C, C', D, D' be categories, with no assumptions whatsoever. (1) If a, b : U ⟶ V are homotopic morphisms of simplicial objects of D in the sense of [Stacks, Tag 019M] and F : D ⥤ D' is a functor, then F(a), F(b) are homotopic morphisms F(U) ⟶ F(V) of simplicial objects of D'. (2) If a, b : U ⟶ V are homotopic morphisms of cosimplicial objects of C in the sense of [Stacks, Tag 0FKJ] — a family h_{n, α} : Uₙ ⟶ Vₙ, indexed by the simplices α ∈ Δ[1]_n, satisfying h_{m, α} ∘ U(f) = V(f) ∘ h_{n, α ∘ f} and having aₙ, bₙ as its components at the two constant maps ⦋n⦌ ⟶ ⦋1⦌, and chains of such — and F : C ⥤ C' is a functor, then F(a), F(b) are homotopic morphisms F(U) ⟶ F(V) of cosimplicial objects of C'. (3) For a contravariant functor, i.e. a functor F : Dᵒᵖ ⥤ C, homotopic morphisms a, b : U ⟶ V of simplicial objects of D have homotopic images F(a), F(b) : F(V) ⟶ F(U), morphisms of cosimplicial objects of C. (4) Likewise a functor F : Cᵒᵖ ⥤ D takes homotopic morphisms a, b : U ⟶ V of cosimplicial objects of C to homotopic morphisms F(a), F(b) : F(V) ⟶ F(U) of simplicial objects of D. No (co)limit in any of the four categories is assumed to exist, and the functor is not asked to preserve anything.

public theorem homotopic_whiskerRight :
    (∀ {D : Type u₁} [Category.{v₁} D] {D' : Type u₂} [Category.{v₂} D']
        {U V : SimplicialObject D} {a b : U ⟶ V} (F : D ⥤ D'),
        Relation.EqvGen (fun x y : U ⟶ V => Nonempty (SimplicialObject.Homotopy x y)) a b →
          Relation.EqvGen
            (fun x y : U ⋙ F ⟶ V ⋙ F => Nonempty (SimplicialObject.Homotopy x y))
            (Functor.whiskerRight a F) (Functor.whiskerRight b F)) ∧
      (∀ {C : Type u₁} [Category.{v₁} C] {C' : Type u₂} [Category.{v₂} C']
          {U V : CosimplicialObject C} {a b : U ⟶ V} (F : C ⥤ C'),
          Relation.EqvGen (fun x y : U ⟶ V => ∃ h : ∀ n : SimplexCategory,
              (Δ[1] : SSet.{0}).obj (op n) → (U.obj n ⟶ V.obj n),
              (∀ ⦃n m : SimplexCategory⦄ (f : n ⟶ m) (α : (Δ[1] : SSet.{0}).obj (op m)),
                  U.map f ≫ h m α = h n ((Δ[1] : SSet.{0}).map f.op α) ≫ V.map f) ∧
                (∀ n : SimplexCategory, h n (stdSimplex.const 1 0 (op n)) = x.app n) ∧
                (∀ n : SimplexCategory, h n (stdSimplex.const 1 1 (op n)) = y.app n)) a b →
            Relation.EqvGen (fun x y : U ⋙ F ⟶ V ⋙ F => ∃ h : ∀ n : SimplexCategory,
                (Δ[1] : SSet.{0}).obj (op n) → ((U ⋙ F).obj n ⟶ (V ⋙ F).obj n),
                (∀ ⦃n m : SimplexCategory⦄ (f : n ⟶ m) (α : (Δ[1] : SSet.{0}).obj (op m)),
                    (U ⋙ F).map f ≫ h m α =
                      h n ((Δ[1] : SSet.{0}).map f.op α) ≫ (V ⋙ F).map f) ∧
                  (∀ n : SimplexCategory, h n (stdSimplex.const 1 0 (op n)) = x.app n) ∧
                  (∀ n : SimplexCategory, h n (stdSimplex.const 1 1 (op n)) = y.app n))
              (Functor.whiskerRight a F) (Functor.whiskerRight b F)) ∧
        (∀ {D : Type u₁} [Category.{v₁} D] {C : Type u₂} [Category.{v₂} C]
            {U V : SimplicialObject D} {a b : U ⟶ V} (F : Dᵒᵖ ⥤ C),
            Relation.EqvGen (fun x y : U ⟶ V => Nonempty (SimplicialObject.Homotopy x y)) a b →
              Relation.EqvGen (fun x y : V.rightOp ⋙ F ⟶ U.rightOp ⋙ F =>
                  ∃ h : ∀ n : SimplexCategory, (Δ[1] : SSet.{0}).obj (op n) →
                    ((V.rightOp ⋙ F).obj n ⟶ (U.rightOp ⋙ F).obj n),
                  (∀ ⦃n m : SimplexCategory⦄ (f : n ⟶ m) (α : (Δ[1] : SSet.{0}).obj (op m)),
                      (V.rightOp ⋙ F).map f ≫ h m α =
                        h n ((Δ[1] : SSet.{0}).map f.op α) ≫ (U.rightOp ⋙ F).map f) ∧
                    (∀ n : SimplexCategory, h n (stdSimplex.const 1 0 (op n)) = x.app n) ∧
                    (∀ n : SimplexCategory, h n (stdSimplex.const 1 1 (op n)) = y.app n))
                (Functor.whiskerRight (NatTrans.rightOp a) F)
                (Functor.whiskerRight (NatTrans.rightOp b) F)) ∧
          (∀ {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D]
              {U V : CosimplicialObject C} {a b : U ⟶ V} (F : Cᵒᵖ ⥤ D),
              Relation.EqvGen (fun x y : U ⟶ V => ∃ h : ∀ n : SimplexCategory,
                  (Δ[1] : SSet.{0}).obj (op n) → (U.obj n ⟶ V.obj n),
                  (∀ ⦃n m : SimplexCategory⦄ (f : n ⟶ m) (α : (Δ[1] : SSet.{0}).obj (op m)),
                      U.map f ≫ h m α = h n ((Δ[1] : SSet.{0}).map f.op α) ≫ V.map f) ∧
                    (∀ n : SimplexCategory, h n (stdSimplex.const 1 0 (op n)) = x.app n) ∧
                    (∀ n : SimplexCategory, h n (stdSimplex.const 1 1 (op n)) = y.app n)) a b →
                Relation.EqvGen (fun x y : V.op ⋙ F ⟶ U.op ⋙ F =>
                    Nonempty (SimplicialObject.Homotopy x y))
                  (Functor.whiskerRight (NatTrans.op a) F)
                  (Functor.whiskerRight (NatTrans.op b) F))

Tag 019Z, a lemma

Tag 019Z in the Stacks Project.

CategoryTheory.Arrow.exists_homotopy_mapCechConerve_id, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/SimplicialObject/Homotopy/Cosimplicial.lean, line 678. The attribute's comment: “stated for an arbitrary endomorphism F of the arrow f with F.left ≫ f.hom = f.hom, of which the source's self map is the case F = (𝟙 X, f ∘ s) for a retraction s of f; the self map is pinned as Arrow.mapCechConerve F, and the homotopy is given by its family of components as in 0FKJ and 07KB, which needs no products in C, the source's concluding homotopy equivalence with the constant cosimplicial object X being a formal consequence”.

Stacks 019Z. A self map of a Čech conerve which is the identity on the base is homotopic to the identity. Let f : X ⟶ Y be an arrow of a category C whose iterated pushouts Y ⨿_X ⋯ ⨿_X Y exist, let U = f.cechConerve be the cosimplicial object of [Stacks, Tag 016N] built from f, and let F be an endomorphism of the arrow f with F.left ≫ f = f, so that the induced self map Arrow.mapCechConerve F of U, given by F.right on each factor Y, is the identity on the base X. Then there is a homotopy from that self map to 𝟙 U in the sense of [Stacks, Tag 0FKJ]: a family of morphisms h_{n, α} : U_n ⟶ U_n, indexed by the simplices α ∈ Δ[1]_n, satisfying h_{m, α} ∘ U(g) = U(g) ∘ h_{n, α ∘ g} for every morphism g : ⦋n⦌ ⟶ ⦋m⦌ of Δ, whose component at the constant map ⦋n⦌ ⟶ ⦋1⦌ with value 0 is the self map and whose component at the constant map with value 1 is the identity. In particular the two are homotopic.

public theorem exists_homotopy_mapCechConerve_id {f : Arrow C}
    [∀ n : ℕ, HasWidePushout f.left (fun _ : Fin (n + 1) => f.right) fun _ => f.hom]
    (F : f ⟶ f) (hF : F.left ≫ f.hom = f.hom) :
    ∃ h : ∀ n : SimplexCategory, (Δ[1] : SSet.{0}).obj (op n) →
        (f.cechConerve.obj n ⟶ f.cechConerve.obj n),
      (∀ ⦃n m : SimplexCategory⦄ (g : n ⟶ m) (α : (Δ[1] : SSet.{0}).obj (op m)),
          f.cechConerve.map g ≫ h m α =
            h n ((Δ[1] : SSet.{0}).map g.op α) ≫ f.cechConerve.map g) ∧
        (∀ n : SimplexCategory, h n (stdSimplex.const 1 0 (op n)) = (mapCechConerve F).app n) ∧
        (∀ n : SimplexCategory, h n (stdSimplex.const 1 1 (op n)) = 𝟙 (f.cechConerve.obj n))

Tag 01A0, a lemma

Tag 01A0 in the Stacks Project.

AlgebraicTopology.homotopic_alternatingCofaceMapComplex_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/SimplicialObject/Homotopy/Cosimplicial.lean, line 797. The attribute's comment: “the source's additive A is weakened to preadditive, which is all s uses; a homotopy is given by its family of components as in 0FKJ and 07KB, which needs no products in A, and being homotopic is spelled Relation.EqvGen of the existence of such a family, as in 019S; the source's second assertion, for the normalized cochain complex Q of 019I, is the formal consequence of this one obtained from the split epimorphism π : s ⟶ Q of 019I via Homotopy.compLeft and Homotopy.compRight”. References: SGA 4 XVII (5.5.3), “homotopy preservation”.

Stacks 01A0. The Moore cochain complex functor carries homotopic morphisms to homotopic maps of cochain complexes. Let a, b : U ⟶ V be homotopic morphisms of cosimplicial objects of a preadditive category A: related by a chain of morphisms consecutive members of which admit a homotopy in one direction or the other, a homotopy from a to b being a family of morphisms h_{n, α} : Uₙ ⟶ Vₙ indexed by the simplices α ∈ Δ[1]ₙ with h_{m, α} ∘ U(g) = V(g) ∘ h_{n, α ∘ g} for every morphism g : ⦋n⦌ ⟶ ⦋m⦌ of Δ, whose components at the constant maps ⦋n⦌ ⟶ ⦋1⦌ with values 0 and 1 are a_n and b_n ([Stacks, Tag 0FKJ]). Then the induced maps s(a), s(b) : s(U) ⟶ s(V) of Moore cochain complexes are chain homotopic.

public theorem homotopic_alternatingCofaceMapComplex_map
    (h : Relation.EqvGen
      (fun a b : U ⟶ V => ∃ h : ∀ n : SimplexCategory, (Δ[1] : SSet.{0}).obj (op n) →
          (U.obj n ⟶ V.obj n),
        (∀ ⦃n m : SimplexCategory⦄ (g : n ⟶ m) (α : (Δ[1] : SSet.{0}).obj (op m)),
            U.map g ≫ h m α = h n ((Δ[1] : SSet.{0}).map g.op α) ≫ V.map g) ∧
          (∀ n : SimplexCategory, h n (stdSimplex.const 1 0 (op n)) = a.app n) ∧
          (∀ n : SimplexCategory, h n (stdSimplex.const 1 1 (op n)) = b.app n)) a b) :
    homotopic A (ComplexShape.up ℕ) ((alternatingCofaceMapComplex A).map a)
      ((alternatingCofaceMapComplex A).map b)

Tag 0FKK, a lemma

Tag 0FKK in the Stacks Project.

AlgebraicTopology.homotopyEquivalences_alternatingCofaceMapComplex_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/SimplicialObject/Homotopy/Cosimplicial.lean, line 869. The attribute's comment: “the first sentence, with the source's additive A weakened to preadditive, which is all s uses; being a homotopy equivalence of cochain complexes is HomologicalComplex.homotopyEquivalences, which pins the map s(a) rather than saying s(U) and s(V) are homotopy equivalent. A homotopy equivalence of cosimplicial objects is spelled out, being unnamed in this development (the source defines it by duality with 019N): a homotopy is its family of components as in 0FKJ and 07KB, which needs no products in A, and being homotopic is Relation.EqvGen of the existence of such a family, the spelling of 01A0. The source's second assertion, for the normalized cochain complex Q of 019I, gets no declaration: Q has no name here, and once it and the homotopy equivalence π : s(U) ⟶ Q(U) are named it follows from this statement by the two-out-of-three property, as 019T deduces the simplicial N(a) from s(a)”.

Stacks 0FKK. The Moore cochain complex of a homotopy equivalence of cosimplicial objects is a homotopy equivalence of cochain complexes. Let a : U ⟶ V be a homotopy equivalence of cosimplicial objects of a preadditive category A: there is b : V ⟶ U such that a ≫ b is homotopic to 𝟙 U and b ≫ a is homotopic to 𝟙 V, where two morphisms f, g of cosimplicial objects are homotopic when they are related by the equivalence relation generated by the existence of a homotopy from one to the other, a homotopy being a family of morphisms h_{n, α} indexed by the simplices α ∈ Δ[1]ₙ with h_{m, α} ∘ U(u) = V(u) ∘ h_{n, α ∘ u} for every morphism u : ⦋n⦌ ⟶ ⦋m⦌ of Δ whose components at the constant maps ⦋n⦌ ⟶ ⦋1⦌ with values 0 and 1 are f_n and g_n ([Stacks, Tag 0FKJ]). Then s(a) : s(U) ⟶ s(V) is a homotopy equivalence of cochain complexes.

public theorem homotopyEquivalences_alternatingCofaceMapComplex_map
    (ha : ∃ b : V ⟶ U,
      Relation.EqvGen (fun f₁ f₂ : U ⟶ U => ∃ h : ∀ n : SimplexCategory,
          (Δ[1] : SSet.{0}).obj (op n) → (U.obj n ⟶ U.obj n),
        (∀ ⦃n m : SimplexCategory⦄ (u : n ⟶ m) (α : (Δ[1] : SSet.{0}).obj (op m)),
            U.map u ≫ h m α = h n ((Δ[1] : SSet.{0}).map u.op α) ≫ U.map u) ∧
          (∀ n : SimplexCategory, h n (stdSimplex.const 1 0 (op n)) = f₁.app n) ∧
          (∀ n : SimplexCategory, h n (stdSimplex.const 1 1 (op n)) = f₂.app n))
        (a ≫ b) (𝟙 U) ∧
      Relation.EqvGen (fun f₁ f₂ : V ⟶ V => ∃ h : ∀ n : SimplexCategory,
          (Δ[1] : SSet.{0}).obj (op n) → (V.obj n ⟶ V.obj n),
        (∀ ⦃n m : SimplexCategory⦄ (u : n ⟶ m) (α : (Δ[1] : SSet.{0}).obj (op m)),
            V.map u ≫ h m α = h n ((Δ[1] : SSet.{0}).map u.op α) ≫ V.map u) ∧
          (∀ n : SimplexCategory, h n (stdSimplex.const 1 0 (op n)) = f₁.app n) ∧
          (∀ n : SimplexCategory, h n (stdSimplex.const 1 1 (op n)) = f₂.app n))
        (b ≫ a) (𝟙 V)) :
    HomologicalComplex.homotopyEquivalences A (ComplexShape.up ℕ)
      ((alternatingCofaceMapComplex A).map a)

Sources

LeanCategoryTheory.CosimplicialObject.Homotopy · CategoryTheory.CosimplicialObject.exists_hom_power_iff · CategoryTheory.CosimplicialObject.exists_homotopy_iff · CategoryTheory.CosimplicialObject.exists_homotopy_iff_nonempty_homotopy_op · CategoryTheory.homotopic_whiskerRight · CategoryTheory.Arrow.exists_homotopy_mapCechConerve_id · AlgebraicTopology.homotopic_alternatingCofaceMapComplex_map · AlgebraicTopology.homotopyEquivalences_alternatingCofaceMapComplex_map

Section14.29 More homotopies in abelian categories #

Section 14.29 of the Stacks Project, Tag 01A1. 3 tags here are carried by 3 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 01A2, a lemma

Tag 01A2 in the Stacks Project.

HomologicalComplex.cylinder.exists_map_descEquiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/SimplicialObject/ChainHomotopyLift.lean, line 188.

Stacks 01A2. Let C be an additive category and c a complex shape in which every index is the target of a relation (as for chain complexes). Then the cylinder ⋄K = K.cylinder of a complex K represents the functor M ↦ {(a, b, h) | a, b : K ⟶ M and h a homotopy from a to b}: the map sending f : ⋄K ⟶ M to the triple obtained by composing the two inclusions ι₀ K, ι₁ K : K ⟶ ⋄K and the canonical homotopy between them with f is a bijection. Moreover K ↦ ⋄K is functorial, by the unique action on morphisms compatible with the inclusions and with the canonical homotopy.

public theorem exists_map_descEquiv (hc : ∀ j, ∃ i, c.Rel i j) :
    ∃ map : ∀ (K L : HomologicalComplex C c), (K ⟶ L) → (K.cylinder ⟶ L.cylinder),
      (∀ K : HomologicalComplex C c, map K K (𝟙 K) = 𝟙 K.cylinder) ∧
      (∀ (K L M : HomologicalComplex C c) (φ : K ⟶ L) (ψ : L ⟶ M),
        map K M (φ ≫ ψ) = map K L φ ≫ map L M ψ) ∧
      (∀ (K L : HomologicalComplex C c) (φ : K ⟶ L), ι₀ K ≫ map K L φ = φ ≫ ι₀ L) ∧
      (∀ (K L : HomologicalComplex C c) (φ : K ⟶ L), ι₁ K ≫ map K L φ = φ ≫ ι₁ L) ∧
      (∀ (K L : HomologicalComplex C c) (φ : K ⟶ L) (i j : ι) (hij : c.Rel j i),
        inlX K i j hij ≫ (map K L φ).f j = φ.f i ≫ inlX L i j hij) ∧
      ∀ K M : HomologicalComplex C c,
        ∃ e : (Σ (a : K ⟶ M) (b : K ⟶ M), Homotopy a b) ≃ (K.cylinder ⟶ M),
          ∀ x : Σ (a : K ⟶ M) (b : K ⟶ M), Homotopy a b,
            ι₀ K ≫ e x = x.1 ∧ ι₁ K ≫ e x = x.2.1 ∧
              ∀ (i j : ι) (hij : c.Rel j i),
                inlX K i j hij ≫ (e x).f j = x.2.2.hom i j

Tag 01A3, a lemma

Tag 01A3 in the Stacks Project.

CochainComplex.diamond.exists_unique_comparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/SimplicialObject/ChainHomotopyLift.lean, line 1260.

Stacks 01A3. Let 0 → A ⊕ A → B → Cpx → 0 be a short exact sequence of complexes, split in each degree by s n : Cpx_n ⟶ B_n. If the associated connecting morphism δ(s) : Cpx → A[-1] ⊕ A[-1] factors through (1, -1) : A[-1] → A[-1] ⊕ A[-1] as δ(s) = (1, -1) ∘ f, then there is a unique morphism φ : B ⟶ ⋄A fitting into a commutative diagram of the two short exact sequences whose vertical maps are compatible with the splittings s n and σ A n.

theorem exists_unique_comparison
    (A B Cpx : CochainComplex C ℤ)
    (i : double A ⟶ B) (r : B ⟶ Cpx)
    (p q : ∀ n, B.X n ⟶ A.X n) (s : ∀ n, Cpx.X n ⟶ B.X n)
    (f : Cpx ⟶ shift1 A)
    -- degreewise biproduct splitting `B_n ≅ (A_n ⊕ A_n) ⊕ C_n`
    (hsr : ∀ n, s n ≫ r.f n = 𝟙 _)
    (hip : ∀ n, i.f n ≫ biprod.lift (p n) (q n) = 𝟙 _)
    (hsplit : ∀ n,
      biprod.lift (p n) (q n) ≫ i.f n + r.f n ≫ s n = 𝟙 (B.X n))
    -- the factorization `δ(s) = (1,-1) ∘ f`
    (hfac1 : ∀ n, s n ≫ B.d n (n + 1) ≫ p (n + 1) = f.f n)
    (hfac2 : ∀ n, s n ≫ B.d n (n + 1) ≫ q (n + 1) = -(f.f n)) :
    ∃! φ : B ⟶ diamond A,
      (i ≫ φ = ι A) ∧
      (φ ≫ ρ A = r ≫ f) ∧
      (∀ n, s n ≫ φ.f n = f.f n ≫ σ A n)

Tag 01A4, a lemma

Tag 01A4 in the Stacks Project.

CategoryTheory.SimplicialObject.exists_homotopy_of_homotopy_normalizedMooreComplex_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/SimplicialObject/ChainHomotopyLift.lean, line 800. The attribute's comment: “the homotopy of 019K is presented by the family of components h_{n + 1, i + 1} ∘ sⁿᵢ it corresponds to under 019L, which is Mathlib's SimplicialObject.Homotopy, and out of which the chain homotopy s(h) of 019Q is built; N(h) is s(h) conjugated by the canonical splitting N ⊆ s of 019A”.

Stacks 01A4. Let a, b : U ⟶ V be morphisms of simplicial objects of an abelian category and let H be a chain homotopy between the induced maps N(a), N(b) : N(U) ⟶ N(V) of normalized Moore complexes. Then a and b are simplicially homotopic, and moreover the homotopy K can be chosen so that the chain homotopy it induces on normalized Moore complexes is H itself: Hₙ = p_V ∘ s(K)ₙ ∘ ι_U, where s(K) is the chain homotopy of K on the alternating face map complexes ([Stacks, Tag 019Q]) and ι_U, p_V are the canonical inclusion of and projection onto the normalized Moore complex. By [Stacks, Tag 019L] such a K is the same thing as a homotopy h : U × Δ[1] ⟶ V from a to b in the sense of [Stacks, Tag 019K], with K.h i = sⁿᵢ ≫ h_{n + 1, i + 1}.

public theorem exists_homotopy_of_homotopy_normalizedMooreComplex_map
    (H : _root_.Homotopy ((normalizedMooreComplex A).map a) ((normalizedMooreComplex A).map b)) :
    ∃ K : Homotopy a b, ∀ n : ℕ, H.hom n (n + 1) =
      (inclusionOfMooreComplexMap U).f n ≫ K.toChainHomotopy.hom n (n + 1) ≫
        (PInftyToNormalizedMooreComplex V).f (n + 1)

Sources

LeanHomologicalComplex.cylinder.exists_map_descEquiv · CochainComplex.diamond.exists_unique_comparison · CategoryTheory.SimplicialObject.exists_homotopy_of_homotopy_normalizedMooreComplex_map

Section14.30 Trivial Kan fibrations #

Section 14.30 of the Stacks Project, Tag 08NK. 8 tags here are carried by 8 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 08NL, a definition

Tag 08NL in the Stacks Project.

SSet.trivialKanFibrations, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/SimplicialSet/TrivialKanFibration.lean, line 77. The attribute's comment: “the two clauses X₀ → Y₀ surjective and lifting for n ≥ 1 are the single right lifting property against all boundary inclusions, the case n = 0 being the surjectivity since ∂Δ[0] = ⊥”.

Stacks 08NL. The class of trivial Kan fibrations: the morphisms f : X ⟶ Y of simplicial sets having the right lifting property with respect to every boundary inclusion ∂Δ[n].ι : ∂Δ[n] ⟶ Δ[n], that is, such that X₀ → Y₀ is surjective and, for n ≥ 1, every commutative square with ∂Δ[n] ⟶ X on top and Δ[n] ⟶ Y at the bottom has a diagonal filler Δ[n] ⟶ X.

public def trivialKanFibrations : MorphismProperty SSet.{u}

Tag 08NM, a lemma

Tag 08NM in the Stacks Project.

SSet.trivialKanFibrations_eq_rlp_monomorphisms, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/SimplicialSet/TrivialKanFibration.lean, line 246. The attribute's comment: “stated as the equality of morphism properties; the source's containment ≤ is the content, the reverse being antitone_rlp on I_le_monomorphisms, and "Z → W termwise injective" is monomorphisms SSet”.

A trivial Kan fibration lifts against any degreewise injective map. For a trivial Kan fibration f : X ⟶ Y of simplicial sets, every solid commutative square
Z --b--> X
|        |
v        v
W --a--> Y
with Z ⟶ W a monomorphism, i.e. injective in every degree, admits a diagonal W ⟶ X making both triangles commute; conversely such a morphism f is a trivial Kan fibration, the boundary inclusions being monomorphisms. Equivalently, the trivial Kan fibrations are precisely the right lifting class of the monomorphisms of simplicial sets.

public theorem trivialKanFibrations_eq_rlp_monomorphisms :
    trivialKanFibrations.{u} = (monomorphisms SSet.{u}).rlp

Tag 08NN, a lemma

Tag 08NN in the Stacks Project.

SSet.trivialKanFibrations_isStableUnderBaseChange, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/SimplicialSet/TrivialKanFibration.lean, line 85.

Stacks 08NN. Trivial Kan fibrations are stable under arbitrary base change. This is the general base-change closure of a right lifting class, applied to the boundary-inclusion definition above.

public instance trivialKanFibrations_isStableUnderBaseChange :
    trivialKanFibrations.{u}.IsStableUnderBaseChange

Tag 08NP, a lemma

Tag 08NP in the Stacks Project.

SSet.trivialKanFibrations_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/SimplicialSet/TrivialKanFibration.lean, line 481.

Stacks 08NP. The composition of two trivial Kan fibrations is a trivial Kan fibration.

public theorem trivialKanFibrations_comp {X Y Z : SSet.{u}} (f : X ⟶ Y) (g : Y ⟶ Z)
    (hf : trivialKanFibrations f) (hg : trivialKanFibrations g) :
    trivialKanFibrations (f ≫ g)

Tag 08NQ, a lemma

Tag 08NQ in the Stacks Project.

SSet.trivialKanFibrations_limit_π_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/SimplicialSet/TrivialKanFibration.lean, line 491.

Stacks 08NQ. Let ⋯ → U² → U¹ → U⁰ be a tower of simplicial sets, encoded as a functor F : ℕᵒᵖ ⥤ SSet, and let U = limₜ Uᵗ be its levelwise inverse limit. If every transition map Uᵗ⁺¹ ⟶ Uᵗ is a trivial Kan fibration, then the projection π⁰ : U ⟶ U⁰ is a trivial Kan fibration.

public theorem trivialKanFibrations_limit_π_zero (F : ℕᵒᵖ ⥤ SSet.{u})
    (h : ∀ t : ℕ, trivialKanFibrations (F.map (homOfLE (Nat.le_succ t)).op)) :
    trivialKanFibrations (limit.π F (Opposite.op 0))

Tag 08NR, a lemma

Tag 08NR in the Stacks Project.

SSet.isStableUnderProductsOfShape_trivialKanFibrations, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/SimplicialSet/TrivialKanFibration.lean, line 258. The attribute's comment: “stability under products is stated for arbitrary product cones, as IsStableUnderProductsOfShape for the class of Tag 08NL; the source's ∏ X_i → ∏ Y_i is the case of Limits.Pi.map, and the index type is in an arbitrary universe where the source says "a set"”.

A product of trivial Kan fibrations is a trivial Kan fibration. If f i : X i ⟶ Y i is a family of trivial Kan fibrations of simplicial sets, that is, of morphisms having the right lifting property with respect to every boundary inclusion ∂Δ[n].ι, then so is the induced morphism ∏ X i ⟶ ∏ Y i between any products of the X i and of the Y i.

public instance isStableUnderProductsOfShape_trivialKanFibrations (J : Type w) :
    trivialKanFibrations.{u}.IsStableUnderProductsOfShape J

Tag 08Q5, a lemma

Tag 08Q5 in the Stacks Project.

SSet.isStableUnderFilteredColimits_trivialKanFibrations, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/SimplicialSet/TrivialKanFibration.lean, line 382. The attribute's comment: “stability under filtered colimits is stated for arbitrary colimit cocones over an arbitrary filtered index category, as IsStableUnderFilteredColimits for the class of Tag 08NL; the source's colim X₁ → colim X₂ is the case of colimMap, and the index category is in arbitrary universes, the hypothesis HasColimitsOfSize being what makes the colimits degreewise as in the source's hint”.

A filtered colimit of trivial Kan fibrations is a trivial Kan fibration. If J is a filtered category and f : X₁ ⟶ X₂ is a morphism of diagrams J ⥤ SSet whose components f.app j are all trivial Kan fibrations, that is, all have the right lifting property with respect to every boundary inclusion ∂Δ[n].ι, then so is the induced morphism colim X₁ ⟶ colim X₂ between any colimits of X₁ and of X₂.

public instance isStableUnderFilteredColimits_trivialKanFibrations
    [HasColimitsOfSize.{w, w'} (Type u)] :
    MorphismProperty.IsStableUnderFilteredColimits.{w, w'} trivialKanFibrations.{u}

Tag 08NS, a lemma

Tag 08NS in the Stacks Project.

SSet.trivialKanFibrations_isHomotopyEquiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/SimplicialSet/TrivialKanFibration.lean, line 691.

Stacks 08NS. A trivial Kan fibration f : X ⟶ Y of simplicial sets — one with the right lifting property against every boundary inclusion ∂Δ[n] ↪ Δ[n] — is a homotopy equivalence: there is a g : Y ⟶ X with f ≫ g homotopic to 𝟙 X and g ≫ f homotopic to 𝟙 Y.

theorem trivialKanFibrations_isHomotopyEquiv
    {X Y : SSet.{u}} (f : X ⟶ Y) (hf : trivialKanFibrations f) :
    ∃ g : Y ⟶ X,
      Nonempty (Homotopy (f ≫ g) (𝟙 X)) ∧
      Nonempty (Homotopy (g ≫ f) (𝟙 Y))

Sources

LeanSSet.trivialKanFibrations · SSet.trivialKanFibrations_eq_rlp_monomorphisms · SSet.trivialKanFibrations_isStableUnderBaseChange · SSet.trivialKanFibrations_comp · SSet.trivialKanFibrations_limit_π_zero · SSet.isStableUnderProductsOfShape_trivialKanFibrations · SSet.isStableUnderFilteredColimits_trivialKanFibrations · SSet.trivialKanFibrations_isHomotopyEquiv

Section14.31 Kan fibrations #

Section 14.31 of the Stacks Project, Tag 08NT. 9 tags here are carried by 8 declarations of the repository (all in StacksFrontier) and 3 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 08NU, a definition

Tag 08NU in the Stacks Project.

Declarations registered for the tag:

SSet.modelCategoryQuillen.fibration_iff registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch14.lean, line 130 (StacksFrontier): “Kan fibration: right lifting property against the horn inclusions J”.
SSet.modelCategoryQuillen.J registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch14.lean, line 132 (StacksFrontier): “Kan fibration: J, the horn inclusions Λ[n+1, i] ⟶ Δ[n+1]”.
SSet.KanComplex registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch14.lean, line 134 (StacksFrontier): “Kan complex: S ⟶ ⊤_ SSet is a Kan fibration”.

Tag 08NV, a lemma

Tag 08NV in the Stacks Project.

SSet.modelCategoryQuillen.isStableUnderBaseChange_fibrations, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/SimplicialSet/KanFibration.lean, line 94.

Stacks 08NV. Kan fibrations of simplicial sets are stable under arbitrary base change. Under fibrations_eq, they are a right lifting class, and every right lifting class has this closure property.

public theorem isStableUnderBaseChange_fibrations :
    (fibrations SSet.{u}).IsStableUnderBaseChange

Tag 08NW, a lemma

Tag 08NW in the Stacks Project.

SSet.hasLiftingProperty_horn_ι_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/SimplicialSet/KanFibration.lean, line 79. The attribute's comment: “the source's lifting condition, one horn inclusion Λ[n + 1, i].ι of Tag 08NU at a time; the same statement for the bundled predicate HomotopicalAlgebra.Fibration of the Quillen model structure on SSet is upstream's multiplicativity of fibrations SSet”.

Stacks 08NW. The composition of two Kan fibrations is a Kan fibration: if f : X ⟶ Y and g : Y ⟶ Z are morphisms of simplicial sets each having the right lifting property with respect to all horn inclusions, then so does f ≫ g.

public theorem hasLiftingProperty_horn_ι_comp {X Y Z : SSet.{u}} {f : X ⟶ Y} {g : Y ⟶ Z}
    (hf : ∀ (n : ℕ) (i : Fin (n + 2)), HasLiftingProperty Λ[n + 1, i].ι f)
    (hg : ∀ (n : ℕ) (i : Fin (n + 2)), HasLiftingProperty Λ[n + 1, i].ι g) :
    ∀ (n : ℕ) (i : Fin (n + 2)), HasLiftingProperty Λ[n + 1, i].ι (f ≫ g)

Tag 08NX, a lemma

Tag 08NX in the Stacks Project.

SSet.fibration_limit_π_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/SimplicialSet/KanFibration.lean, line 513. The attribute's comment: “Kan fibrations are Mathlib's fibrations for the Quillen model structure on SSet, whose generating family J is the horn inclusions of Tag 08NU”.

Stacks 08NX. Let F : ℕᵒᵖ ⥤ SSet be a tower ⋯ → U² → U¹ → U⁰ of simplicial sets each of whose transition morphisms Uᵗ⁺¹ ⟶ Uᵗ is a Kan fibration. Then the canonical projection limit F ⟶ U⁰ = F.obj (op 0) from the inverse limit to the bottom term is a Kan fibration.

theorem fibration_limit_π_zero (F : ℕᵒᵖ ⥤ SSet)
    (hF : ∀ t : ℕ, Fibration (F.map (homOfLE (Nat.le_succ t)).op)) :
    Fibration (limit.π F (Opposite.op 0))

Tag 08NY, a lemma

Tag 08NY in the Stacks Project.

SSet.modelCategoryQuillen.isStableUnderProductsOfShape_fibrations, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/SimplicialSet/KanFibration.lean, line 107. The attribute's comment: “Kan fibrations are Mathlib's fibrations for the Quillen model structure on SSet, whose generating family J is the horn inclusions of Tag 08NU; stability under products is stated for arbitrary product cones, the source's ∏ X_i → ∏ Y_i being the case of Limits.Pi.map”.

Stacks 08NY. A product of Kan fibrations is a Kan fibration: if f i : X i ⟶ Y i is a family of morphisms of simplicial sets each having the right lifting property with respect to all horn inclusions, then so does the induced morphism ∏ X i ⟶ ∏ Y i between any products of the X i and the Y i.

public instance isStableUnderProductsOfShape_fibrations (J : Type w) :
    (fibrations SSet.{u}).IsStableUnderProductsOfShape J

Tag 08NZ, a lemma

Tag 08NZ in the Stacks Project.

CategoryTheory.SimplicialObject.kanComplex_forget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/SimplicialSet/KanComplex/SimplicialGroup.lean, line 64. The attribute's comment: “a simplicial group is Mathlib's SimplicialObject GrpCat, and its underlying simplicial set is X ⋙ forget GrpCat”.

Stacks 08NZ. Let X be a simplicial group. Then the underlying simplicial set of X is a Kan complex.

theorem kanComplex_forget (X : SimplicialObject GrpCat.{u}) :
    KanComplex (X ⋙ forget GrpCat)

Tag 08P0, a lemma

Tag 08P0 in the Stacks Project.

CategoryTheory.SimplicialObject.fibration_whiskerRight_forget_of_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/SimplicialSet/KanFibration.lean, line 424. The attribute's comment: “stated for simplicial groups written additively, commutativity being unused by the source's argument (which reduces to Tag 08NZ, a statement about simplicial groups); the source's simplicial abelian groups are the case of Functor.whiskerRight f (forget₂ AddCommGrpCat AddGrpCat), whose conclusion is the same term by rfl. Kan fibrations are Mathlib's fibrations for the Quillen model structure on SSet, whose generating family J is the horn inclusions of Tag 08NU”.

Stacks 08P0. A termwise surjective homomorphism of simplicial groups is a Kan fibration: if f : X ⟶ Y is a morphism of simplicial groups such that X_n → Y_n is surjective for every n, then the induced morphism of underlying simplicial sets has the right lifting property with respect to all horn inclusions.

public theorem fibration_whiskerRight_forget_of_surjective
    {X Y : SimplicialObject AddGrpCat.{u}} (f : X ⟶ Y)
    (hf : ∀ n : SimplexCategoryᵒᵖ, Function.Surjective (f.app n).hom) :
    Fibration (Functor.whiskerRight f (forget AddGrpCat.{u}))

Tag 08P1, a lemma

Tag 08P1 in the Stacks Project.

CategoryTheory.SimplicialObject.trivialKanFibrations_whiskerRight_forget_of_surjective_of_quasiIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/SimplicialSet/TrivialKanFibration/SimplicialAbelianGroup.lean, line 863. The attribute's comment: “trivial Kan fibrations are the class SSet.trivialKanFibrations of Tag 08NL, the right lifting class of the boundary inclusions, the source's surjectivity of X₀ → Y₀ being its case n = 0; the associated chain complex is s, Mathlib's alternatingFaceMapComplex, the hypothesis being equivalent to the one for the normalized complex N by Tag 019C”.

Stacks 08P1. If f : X ⟶ Y is a morphism of simplicial abelian groups such that X_n → Y_n is surjective for every n and such that s(X) → s(Y) is a quasi-isomorphism of associated chain complexes, then the induced morphism of underlying simplicial sets has the right lifting property with respect to all boundary inclusions ∂Δ[n].ι : ∂Δ[n] ⟶ Δ[n].

public theorem trivialKanFibrations_whiskerRight_forget_of_surjective_of_quasiIso
    {X Y : SimplicialObject AddCommGrpCat.{u}} (f : X ⟶ Y)
    (hf : ∀ n : SimplexCategoryᵒᵖ, Function.Surjective (f.app n).hom)
    [QuasiIso ((alternatingFaceMapComplex AddCommGrpCat.{u}).map f)] :
    SSet.trivialKanFibrations (Functor.whiskerRight f (forget AddCommGrpCat.{u}))

Tag 08P2, a lemma

Tag 08P2 in the Stacks Project.

AlgebraicTopology.quasiIso_alternatingFaceMapComplex_map_of_homotopyEquivalences_forget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/SimplicialSet/TrivialKanFibration/SimplicialAbelianGroup.lean, line 910. The attribute's comment: “the homotopy equivalence is asked of the underlying simplicial sets, SimplicialObject.homotopyEquivalences (Type u) (Tag 019N at C = Type u) applied to Functor.whiskerRight f (forget AddCommGrpCat); the associated chain complex is s, Mathlib's alternatingFaceMapComplex, so that the conclusion is verbatim the hypothesis of 08P1, the version for the normalized complex N being equivalent to it by Tag 019C”.

Stacks 08P2. Let f : X ⟶ Y be a morphism of simplicial abelian groups whose underlying morphism of simplicial sets X ⋙ forget ⟶ Y ⋙ forget is a homotopy equivalence, i.e. admits a morphism of simplicial sets back whose two composites with it are homotopic to the identities ([Stacks, Tag 019N]). Then the induced morphism s(X) ⟶ s(Y) of Moore complexes is a quasi-isomorphism.

public theorem quasiIso_alternatingFaceMapComplex_map_of_homotopyEquivalences_forget
    {X Y : SimplicialObject AddCommGrpCat.{u}} (f : X ⟶ Y)
    (hf : SimplicialObject.homotopyEquivalences (Type u)
      (Functor.whiskerRight f (forget AddCommGrpCat.{u}))) :
    QuasiIso ((alternatingFaceMapComplex AddCommGrpCat.{u}).map f)

Sources

LeanSSet.modelCategoryQuillen.fibration_iff · SSet.modelCategoryQuillen.J · SSet.KanComplex · SSet.modelCategoryQuillen.isStableUnderBaseChange_fibrations · SSet.hasLiftingProperty_horn_ι_comp · SSet.fibration_limit_π_zero · SSet.modelCategoryQuillen.isStableUnderProductsOfShape_fibrations · CategoryTheory.SimplicialObject.kanComplex_forget

Section14.32 A homotopy equivalence #

Section 14.32 of the Stacks Project, Tag 01A5. 3 tags here are carried by 4 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 01A6, a lemma

Tag 01A6 in the Stacks Project.

SSet.trivialKanFibrations_of_coskeletal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/SimplicialSet/TrivialKanFibration/CechNerve.lean, line 167.

Stacks 01A6. Let f : V ⟶ U be a morphism of simplicial sets and let n ≥ 0. Assume: 1. fᵢ is bijective for every i < n; 2. fₙ is surjective; 3. the canonical (unit) morphism U → cosk_n sk_n U is an isomorphism; 4. the canonical (unit) morphism V → cosk_n sk_n V is an isomorphism. Then f is a trivial Kan fibration.

theorem trivialKanFibrations_of_coskeletal
    {V U : SSet} (f : V ⟶ U) (n : ℕ)
    (h1 : ∀ i : ℕ, i < n → Function.Bijective (f.app (op ⦋i⦌)))
    (h2 : Function.Surjective (f.app (op ⦋n⦌)))
    (h3 : IsIso ((coskAdj n).unit.app U))
    (h4 : IsIso ((coskAdj n).unit.app V)) :
    trivialKanFibrations f

Tag 01A9, a lemma

Tag 01A9 in the Stacks Project.

SSet.nonempty_homotopy_of_app_eq_of_isCoskeletal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/SimplicialSet/TrivialKanFibration/CechNerve.lean, line 415. The attribute's comment: “the conclusion is strengthened from f⁰ and f¹ being homotopic to the existence of a homotopy from f⁰ to f¹, which is what both of the source's proofs produce; hypothesis (3) of the source, that V ⟶ cosk_n sk_n V is an isomorphism, is dropped, since neither of the source's proofs uses it: maps into an n-coskeletal object are exactly maps of their n-truncations, by coskAdj n, for an arbitrary source; coskeletality of U is Mathlib's IsCoskeletal, equivalent to the source's U ⟶ cosk_n sk_n U being an isomorphism”. References: SGA 4 Vbis (3.0.2.4), “simplicial sets”.

Two maps into an n-coskeletal simplicial set agreeing below degree n are homotopic, [Stacks, Tag 01A9]. Let f₀, f₁ : V ⟶ U be maps of simplicial sets whose components V_i ⟶ U_i agree for every i < n, and assume that the canonical morphism U ⟶ cosk_n sk_n U is an isomorphism, i.e. that U is n-coskeletal. Then there is a simplicial homotopy V ⊗ Δ[1] ⟶ U from f₀ to f₁; in particular f₀ and f₁ are homotopic. No hypothesis on V is needed.

theorem nonempty_homotopy_of_app_eq_of_isCoskeletal {V U : SSet.{u}} (n : ℕ) [U.IsCoskeletal n]
    (f₀ f₁ : V ⟶ U) (h : ∀ i < n, f₀.app (op ⦋i⦌) = f₁.app (op ⦋i⦌)) :
    Nonempty (Homotopy f₀ f₁)

Tag 01AB, a lemma

Tag 01AB in the Stacks Project.

SSet.hasLiftingProperty_augmentedCechNerve_hom, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/SimplicialSet/TrivialKanFibration/CechNerve.lean, line 471. The attribute's comment: “the lifting property proved is against every map injective on vertices, hence against every monomorphism of simplicial sets, not only the boundary inclusions”.

The augmentation of the Čech nerve of a surjection of sets has the right lifting property with respect to every morphism of simplicial sets injective on vertices, [Stacks, Tag 01AB]. Monomorphisms of simplicial sets are injective in every degree, so the class of morphisms covered contains every monomorphism, and in particular the boundary inclusions ∂Δ[n] ⟶ Δ[n] against which trivialKanFibrations asks for lifts.

lemma hasLiftingProperty_augmentedCechNerve_hom (F : Arrow (Type u))
    (hF : Function.Surjective F.hom) {K L : SSet.{u}} {i : K ⟶ L}
    (hi : Function.Injective (i.app (op ⦋0⦌))) :
    HasLiftingProperty i F.augmentedCechNerve.hom

SSet.trivialKanFibrations_augmentedCechNerve_hom_of_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/SimplicialSet/TrivialKanFibration/CechNerve.lean, line 528. The attribute's comment: “the simplicial set of the source's Example 016E is the Čech nerve (Arrow.mk f).cechNerve, and the source's morphism from it to the constant simplicial set with value B is the augmentation (Arrow.mk f).augmentedCechNerve.hom”.

The Čech nerve of a surjection of sets is a trivial Kan fibration, [Stacks, Tag 01AB]. Let f : A ⟶ B be a surjective map of sets and let U be the simplicial set with U_n = A ×_B A ×_B ⋯ ×_B A (n + 1 factors), the Čech nerve of f. Then the augmentation of U over the constant simplicial set with value B, given in degree n by the projection (a_0, …, a_n) ↦ f a_0 to the base, is a trivial Kan fibration.

theorem trivialKanFibrations_augmentedCechNerve_hom_of_surjective {A B : Type u} {f : A ⟶ B}
    (hf : Function.Surjective f) : trivialKanFibrations (Arrow.mk f).augmentedCechNerve.hom

Sources

LeanSSet.trivialKanFibrations_of_coskeletal · SSet.nonempty_homotopy_of_app_eq_of_isCoskeletal · SSet.hasLiftingProperty_augmentedCechNerve_hom · SSet.trivialKanFibrations_augmentedCechNerve_hom_of_surjective

Section14.33 Preparation for standard resolutions #

Section 14.33 of the Stacks Project, Tag 0G5L. 6 tags here are carried by 9 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0G5M, an example

Tag 0G5M in the Stacks Project.

CategoryTheory.Functor.iterate, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/StandardResolution/Godement.lean, line 97.

Stacks 0G5M. The n-fold composite Y ∘ … ∘ Y of an endofunctor Y : C ⥤ C with itself, with Y.iterate 0 = 𝟭 C and Y.iterate (n + 1) = Y.iterate n ⋙ Y, so that the copy of Y added at each step is the outermost one. On objects it is the n-fold iterate of Y.obj, whence the name. Godement's X_n, a composite of n + 1 copies of Y, is Y.iterate (n + 1), and his X_{-1} is Y.iterate 0.

public def iterate (Y : C ⥤ C) : ℕ → C ⥤ C

CategoryTheory.Functor.iterate_add, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/StandardResolution/Godement.lean, line 120.

Stacks 0G5M. The powers of an endofunctor are additive: Y^{m+n} = Y^m ∘ Y^n in ⋙-order, i.e. Y.iterate (m + n) = Y.iterate m ⋙ Y.iterate n. This is the observation X_{n+m+1} = X_n ∘ X_m, where X_n = Y.iterate (n + 1).

public theorem iterate_add (Y : C ⥤ C) (m n : ℕ) :
    Y.iterate (m + n) = Y.iterate m ⋙ Y.iterate n

CategoryTheory.Godement.face, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/StandardResolution/Godement.lean, line 138.

Stacks 0G5M. The face d^n_j : X_n ⟶ X_{n-1} attached to a transformation d : Y ⟶ 𝟭 C, for n ≥ 0 and 0 ≤ j ≤ n: it whiskers d into the j-th of the n + 1 copies of Y in X_n = Y.iterate (n + 1), counted from the left, i.e. from the outside, so that d^n_j = 1_{X_{j-1}} ⋆ d ⋆ 1_{X_{n-j-1}}. It is defined by the recursion d^n_0 = d ⋆ 1_{X_{n-1}} and d^{n+1}_{j+1} = 1_Y ⋆ d^n_j; in particular face d 0 0 = d : X_0 = Y ⟶ 𝟭 C is the augmentation. No compatibility between d and a comultiplication is assumed.

public def face (d : Y ⟶ 𝟭 C) :
    (n : ℕ) → Fin (n + 1) → (Y.iterate (n + 1) ⟶ Y.iterate n)

CategoryTheory.Godement.degeneracy, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/StandardResolution/Godement.lean, line 152.

Stacks 0G5M. The degeneracy s^n_j : X_n ⟶ X_{n+1} attached to a transformation s : Y ⟶ Y ⋙ Y, for n ≥ 0 and 0 ≤ j ≤ n: it whiskers s into the j-th of the n + 1 copies of Y in X_n = Y.iterate (n + 1), counted from the left, i.e. from the outside, so that s^n_j = 1_{X_{j-1}} ⋆ s ⋆ 1_{X_{n-j-1}}. It is defined by the recursion s^n_0 = s ⋆ 1_{X_{n-1}} and s^{n+1}_{j+1} = 1_Y ⋆ s^n_j. No compatibility between s and a counit is assumed.

public def degeneracy (s : Y ⟶ Y ⋙ Y) :
    (n : ℕ) → Fin (n + 1) → (Y.iterate (n + 1) ⟶ Y.iterate (n + 2))

Tag 0G5N, a lemma

Tag 0G5N in the Stacks Project.

CategoryTheory.Godement.exists_augmented_standardResolution, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/StandardResolution/Godement.lean, line 612.

Stacks 0G5N. Let Y : C ⥤ C be an endofunctor with transformations d : Y ⟶ 𝟭 C and s : Y ⟶ Y ⋙ Y satisfying the counit identities 1_Y = (d ⋆ 1_Y) ∘ s = (1_Y ⋆ d) ∘ s and coassociativity (s ⋆ 1_Y) ∘ s = (1_Y ⋆ s) ∘ s, i.e. let (Y, d, s) be a comonad on C. Then the powers X_n = Y.iterate (n + 1), with the faces Godement.face d and the degeneracies Godement.degeneracy s, are a simplicial object of the category C ⥤ C of endofunctors of C, augmented over X_{-1} = Y.iterate 0 = 𝟭 C by face d 0 0 = d : X_0 = Y ⟶ 𝟭 C.

public theorem exists_augmented_standardResolution {C : Type u} [Category.{v} C] {Y : C ⥤ C}
    (d : Y ⟶ 𝟭 C) (s : Y ⟶ Y ⋙ Y)
    (left_counit : s ≫ Functor.whiskerLeft Y d = 𝟙 Y)
    (right_counit : s ≫ Functor.whiskerRight d Y = 𝟙 Y)
    (coassoc : s ≫ Functor.whiskerLeft Y s = s ≫ Functor.whiskerRight s Y) :
    ∃ (X : SimplicialObject.Augmented (C ⥤ C))
      (h : ∀ n : ℕ, X.left.obj (op ⦋n⦌) = Y.iterate (n + 1)) (hX : X.right = 𝟭 C),
      (∀ (n : ℕ) (j : Fin (n + 2)),
        X.left.δ j = eqToHom (h (n + 1)) ≫ face d (n + 1) j ≫ eqToHom (h n).symm) ∧
      (∀ (n : ℕ) (j : Fin (n + 1)),
        X.left.σ j = eqToHom (h n) ≫ degeneracy s n j ≫ eqToHom (h (n + 1)).symm) ∧
      X.hom.app (op ⦋0⦌) = eqToHom (h 0) ≫ face d 0 0 ≫ eqToHom hX.symm

Tag 0G5P, an example

Tag 0G5P in the Stacks Project.

CategoryTheory.Godement.exists_augmented_standardResolution_whisker, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/StandardResolution/Godement.lean, line 698.

Stacks 0G5P. Let Y : C ⥤ C be an endofunctor with transformations d : Y ⟶ 𝟭 C and s : Y ⟶ Y ⋙ Y satisfying the counit identities 1_Y = (d ⋆ 1_Y) ∘ s = (1_Y ⋆ d) ∘ s and coassociativity (s ⋆ 1_Y) ∘ s = (1_Y ⋆ s) ∘ s, i.e. let (Y, d, s) be a comonad on C, and let F : A ⥤ C and G : C ⥤ B be functors. Then the conjugated powers G ∘ X_n ∘ F = F ⋙ Y.iterate (n+1) ⋙ G, with the faces 1_G ⋆ d^n_j ⋆ 1_F and degeneracies 1_G ⋆ s^n_j ⋆ 1_F obtained from Godement.face d and Godement.degeneracy s by whiskering with F and G, are a simplicial object of the category A ⥤ B of functors from A to B, augmented over G ∘ F = F ⋙ G by 1_G ⋆ d ⋆ 1_F.

public theorem exists_augmented_standardResolution_whisker
    {A : Type u₁} [Category.{v₁} A] {B : Type u₂} [Category.{v₂} B]
    {C : Type u} [Category.{v} C] {Y : C ⥤ C}
    (d : Y ⟶ 𝟭 C) (s : Y ⟶ Y ⋙ Y) (F : A ⥤ C) (G : C ⥤ B)
    (left_counit : s ≫ Functor.whiskerLeft Y d = 𝟙 Y)
    (right_counit : s ≫ Functor.whiskerRight d Y = 𝟙 Y)
    (coassoc : s ≫ Functor.whiskerLeft Y s = s ≫ Functor.whiskerRight s Y) :
    ∃ (X : SimplicialObject.Augmented (A ⥤ B))
      (h : ∀ n : ℕ, X.left.obj (op ⦋n⦌) = F ⋙ Y.iterate (n + 1) ⋙ G)
      (hX : X.right = F ⋙ G),
      (∀ (n : ℕ) (j : Fin (n + 2)),
        X.left.δ j = eqToHom (h (n + 1)) ≫
          Functor.whiskerRight (Functor.whiskerLeft F (face d (n + 1) j)) G ≫
            eqToHom (h n).symm) ∧
      (∀ (n : ℕ) (j : Fin (n + 1)),
        X.left.σ j = eqToHom (h n) ≫
          Functor.whiskerRight (Functor.whiskerLeft F (degeneracy s n j)) G ≫
            eqToHom (h (n + 1)).symm) ∧
      X.hom.app (op ⦋0⦌) = eqToHom (h 0) ≫
        Functor.whiskerRight (Functor.whiskerLeft F (face d 0 0)) G ≫ eqToHom hX.symm

Tag 0G5Q, a lemma

Tag 0G5Q in the Stacks Project.

CategoryTheory.SimplicialObject.Augmented.exists_section_of_comp_hom_app_zero_eq_id, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/StandardResolution/Godement.lean, line 768.

Stacks 0G5Q. Let X be an augmented simplicial object of D, with augmentation ε = X.hom : X.left ⟶ const X.right, and let h₀ : X.right ⟶ X_0 satisfy ε_0 ∘ h₀ = 1. Then there is a morphism of simplicial objects h : const X.right ⟶ X.left restricting to h₀ in degree 0 and satisfying ε ∘ h = 1; necessarily h_n = u_n ∘ h₀ with u_n : X_0 ⟶ X_n induced by the unique morphism ⦋n⦌ ⟶ ⦋0⦌.

public theorem exists_section_of_comp_hom_app_zero_eq_id {D : Type u} [Category.{v} D]
    (X : SimplicialObject.Augmented D) (h₀ : X.right ⟶ X.left.obj (op ⦋0⦌))
    (hh₀ : h₀ ≫ X.hom.app (op ⦋0⦌) = 𝟙 X.right) :
    ∃ h : (SimplicialObject.const D).obj X.right ⟶ X.left,
      h.app (op ⦋0⦌) = h₀ ∧ h ≫ X.hom = 𝟙 ((SimplicialObject.const D).obj X.right)

Tag 0G5R, a lemma

Tag 0G5R in the Stacks Project.

CategoryTheory.Godement.exists_homotopy_hcomp_hcomp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/StandardResolution/Whiskering.lean, line 657.

Stacks 0G5R. Let Y : C ⥤ C be an endofunctor with transformations d : Y ⟶ 𝟭 C and s : Y ⟶ Y ⋙ Y, let F, F' : A ⥤ C and G, G' : C ⥤ B be functors, and let Z, Z' be the augmented simplicial objects G ∘ X ∘ F and G' ∘ X ∘ F' of A ⥤ B obtained by conjugating the powers X_n = Y.iterate (n + 1). Let (a_n) : G ∘ X ⟶ G' ∘ X and (b_n) : X ∘ F ⟶ X ∘ F' be morphisms of simplicial objects, i.e. families commuting with the faces Godement.face d and degeneracies Godement.degeneracy s, compatible via the augmentations with a : G ⟶ G' and b : F ⟶ F'. Then the two horizontal composites a ⋆ (b_n) and (a_n) ⋆ b are morphisms Z ⟶ Z' of augmented simplicial objects with component a ⋆ b over the augmentations, and they are homotopic: there is a simplicial homotopy from (a_n) ⋆ b to a ⋆ (b_n), given by h_{n, i} = a_{i-1} ⋆ b_{n-i}.

public theorem exists_homotopy_hcomp_hcomp
    {A : Type u₁} [Category.{v₁} A] {B : Type u₂} [Category.{v₂} B]
    {C : Type u} [Category.{v} C] {Y : C ⥤ C}
    (d : Y ⟶ 𝟭 C) (s : Y ⟶ Y ⋙ Y) (F F' : A ⥤ C) (G G' : C ⥤ B)
    (a : G ⟶ G') (b : F ⟶ F')
    (an : (n : ℕ) → (Y.iterate (n + 1) ⋙ G ⟶ Y.iterate (n + 1) ⋙ G'))
    (bn : (n : ℕ) → (F ⋙ Y.iterate (n + 1) ⟶ F' ⋙ Y.iterate (n + 1)))
    (han_face : ∀ (n : ℕ) (j : Fin (n + 2)),
      an (n + 1) ≫ Functor.whiskerRight (face d (n + 1) j) G' =
        Functor.whiskerRight (face d (n + 1) j) G ≫ an n)
    (han_degeneracy : ∀ (n : ℕ) (j : Fin (n + 1)),
      an n ≫ Functor.whiskerRight (degeneracy s n j) G' =
        Functor.whiskerRight (degeneracy s n j) G ≫ an (n + 1))
    (han_aug : an 0 ≫ Functor.whiskerRight (face d 0 0) G' =
      Functor.whiskerRight (face d 0 0) G ≫ a)
    (hbn_face : ∀ (n : ℕ) (j : Fin (n + 2)),
      bn (n + 1) ≫ Functor.whiskerLeft F' (face d (n + 1) j) =
        Functor.whiskerLeft F (face d (n + 1) j) ≫ bn n)
    (hbn_degeneracy : ∀ (n : ℕ) (j : Fin (n + 1)),
      bn n ≫ Functor.whiskerLeft F' (degeneracy s n j) =
        Functor.whiskerLeft F (degeneracy s n j) ≫ bn (n + 1))
    (hbn_aug : bn 0 ≫ Functor.whiskerLeft F' (face d 0 0) =
      Functor.whiskerLeft F (face d 0 0) ≫ b)
    (Z Z' : SimplicialObject.Augmented (A ⥤ B))
    (hZ : ∀ n : ℕ, Z.left.obj (op ⦋n⦌) = F ⋙ Y.iterate (n + 1) ⋙ G)
    (hZr : Z.right = F ⋙ G)
    (hZδ : ∀ (n : ℕ) (j : Fin (n + 2)), Z.left.δ j = eqToHom (hZ (n + 1)) ≫
      Functor.whiskerRight (Functor.whiskerLeft F (face d (n + 1) j)) G ≫ eqToHom (hZ n).symm)
    (hZσ : ∀ (n : ℕ) (j : Fin (n + 1)), Z.left.σ j = eqToHom (hZ n) ≫
      Functor.whiskerRight (Functor.whiskerLeft F (degeneracy s n j)) G ≫
        eqToHom (hZ (n + 1)).symm)
    (hZhom : Z.hom.app (op ⦋0⦌) = eqToHom (hZ 0) ≫
      Functor.whiskerRight (Functor.whiskerLeft F (face d 0 0)) G ≫ eqToHom hZr.symm)
    (hZ' : ∀ n : ℕ, Z'.left.obj (op ⦋n⦌) = F' ⋙ Y.iterate (n + 1) ⋙ G')
    (hZr' : Z'.right = F' ⋙ G')
    (hZδ' : ∀ (n : ℕ) (j : Fin (n + 2)), Z'.left.δ j = eqToHom (hZ' (n + 1)) ≫
      Functor.whiskerRight (Functor.whiskerLeft F' (face d (n + 1) j)) G' ≫ eqToHom (hZ' n).symm)
    (hZσ' : ∀ (n : ℕ) (j : Fin (n + 1)), Z'.left.σ j = eqToHom (hZ' n) ≫
      Functor.whiskerRight (Functor.whiskerLeft F' (degeneracy s n j)) G' ≫
        eqToHom (hZ' (n + 1)).symm)
    (hZhom' : Z'.hom.app (op ⦋0⦌) = eqToHom (hZ' 0) ≫
      Functor.whiskerRight (Functor.whiskerLeft F' (face d 0 0)) G' ≫ eqToHom hZr'.symm) :
    ∃ α β : Z ⟶ Z',
      (∀ n : ℕ, α.left.app (op ⦋n⦌) = eqToHom (hZ n) ≫
        NatTrans.hcomp (F := F ⋙ Y.iterate (n + 1)) (bn n) a ≫ eqToHom (hZ' n).symm) ∧
      (∀ n : ℕ, β.left.app (op ⦋n⦌) = eqToHom (hZ n) ≫
        NatTrans.hcomp b (an n) ≫ eqToHom (hZ' n).symm) ∧
      α.right = eqToHom hZr ≫ NatTrans.hcomp b a ≫ eqToHom hZr'.symm ∧
      β.right = eqToHom hZr ≫ NatTrans.hcomp b a ≫ eqToHom hZr'.symm ∧
      Nonempty (SimplicialObject.Homotopy β.left α.left)

Tag 0G5S, a lemma

Tag 0G5S in the Stacks Project.

CategoryTheory.Godement.exists_homotopy_whiskerLeft_whiskerRight, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/StandardResolution/Whiskering.lean, line 959.

Stacks 0G5S. Let Y : C ⥤ C be an endofunctor with transformations d : Y ⟶ 𝟭 C and s : Y ⟶ Y ⋙ Y, and let X be an augmented simplicial object of the category C ⥤ C of endofunctors of C whose terms are the powers X_n = Y.iterate (n + 1), whose faces and degeneracies are Godement.face d and Godement.degeneracy s, and whose augmentation has target 𝟭 C. Let f : 𝟭 C ⟶ 𝟭 C be an endomorphism of the identity functor. Then the two whiskerings f ⋆ 1_{X_n} and 1_{X_n} ⋆ f of f onto the terms of X are morphisms of simplicial objects, compatible with f through the augmentation ε : X ⟶ 𝟭 C, i.e. they are endomorphisms of X in the category of augmented simplicial objects with component f over 𝟭 C. Moreover they are homotopic: there is a simplicial homotopy from 1_X ⋆ f to f ⋆ 1_X, given by h_{n, i} = 1_i ⋆ f ⋆ 1_{n + 1 - i}.

public theorem exists_homotopy_whiskerLeft_whiskerRight {C : Type u} [Category.{v} C]
    {Y : C ⥤ C} (d : Y ⟶ 𝟭 C) (s : Y ⟶ Y ⋙ Y) (f : 𝟭 C ⟶ 𝟭 C)
    (X : SimplicialObject.Augmented (C ⥤ C))
    (h : ∀ n : ℕ, X.left.obj (op ⦋n⦌) = Y.iterate (n + 1)) (hX : X.right = 𝟭 C)
    (hδ : ∀ (n : ℕ) (j : Fin (n + 2)),
      X.left.δ j = eqToHom (h (n + 1)) ≫ face d (n + 1) j ≫ eqToHom (h n).symm)
    (hσ : ∀ (n : ℕ) (j : Fin (n + 1)),
      X.left.σ j = eqToHom (h n) ≫ degeneracy s n j ≫ eqToHom (h (n + 1)).symm) :
    ∃ α β : X ⟶ X,
      (∀ n : ℕ, α.left.app (op ⦋n⦌) =
        eqToHom (h n) ≫ Functor.whiskerLeft (Y.iterate (n + 1)) f ≫ eqToHom (h n).symm) ∧
      (∀ n : ℕ, β.left.app (op ⦋n⦌) =
        eqToHom (h n) ≫ Functor.whiskerRight f (Y.iterate (n + 1)) ≫ eqToHom (h n).symm) ∧
      α.right = eqToHom hX ≫ f ≫ eqToHom hX.symm ∧
      β.right = eqToHom hX ≫ f ≫ eqToHom hX.symm ∧
      Nonempty (SimplicialObject.Homotopy β.left α.left)

Sources

LeanCategoryTheory.Functor.iterate · CategoryTheory.Functor.iterate_add · CategoryTheory.Godement.face · CategoryTheory.Godement.degeneracy · CategoryTheory.Godement.exists_augmented_standardResolution · CategoryTheory.Godement.exists_augmented_standardResolution_whisker · CategoryTheory.SimplicialObject.Augmented.exists_section_of_comp_hom_app_zero_eq_id · CategoryTheory.Godement.exists_homotopy_hcomp_hcomp

Section14.34 Standard resolutions #

Section 14.34 of the Stacks Project, Tag 08N8. 9 tags here are carried by 7 declarations of the repository (all in StacksFrontier) and 3 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 08N9, a situation

Tag 08N9 in the Stacks Project.

Declarations registered for the tag:

CategoryTheory.Adjunction registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch14.lean, line 30 (StacksFrontier): “the situation: V : A ⥤ S with a left adjoint U : S ⥤ A, as the adjunction U ⊣ V”. References: SGA 3 I (5.3.1.1); SGA 4 II (6.5); SGA 4 IV (1.5); SGA 4 IV (3.1), “more general”.

Tag 08NB, an equation

Tag 08NB in the Stacks Project.

Declarations registered for the tag:

CategoryTheory.Adjunction.right_triangle registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch14.lean, line 122 (StacksFrontier): “V → VUV → V is the identity (for adj : U ⊣ V, Mathlib's F = U, G = V; up to unitors)”.
CategoryTheory.Adjunction.left_triangle registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch14.lean, line 125 (StacksFrontier): “U → UVU → U is the identity (same conventions)”.

Tag 08NC, a lemma

Tag 08NC in the Stacks Project.

CategoryTheory.Comonad.exists_augmented_standardResolution, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/StandardResolution/Basic.lean, line 179.

Stacks 08NC. Let G be a comonad on a category A, with counit G.ε : G ⟶ 𝟭 A and comultiplication G.δ : G ⟶ G ⋙ G. The iterates Z (n + 1) of G, with Z 0 = 𝟭 A, carry faces d n j : Z (n + 1) ⟶ Z n and degeneracies s n j : Z (n + 1) ⟶ Z (n + 2) for 0 ≤ j ≤ n, obtained by whiskering G.ε, resp. G.δ, into the j-th factor G counted from the left in the composite Z (n + 1) = G ∘ ⋯ ∘ G, and these are the faces and degeneracies of a simplicial object of the category A ⥤ A of endofunctors of A, augmented over the constant simplicial object 𝟭 A by ε₀ = d 0 0 = G.ε.

public theorem exists_augmented_standardResolution {A : Type u} [Category.{v} A]
    (G : Comonad A) :
    ∃ (Z : ℕ → (A ⥤ A)) (hZ : ∀ n : ℕ, Z (n + 1) = Z n ⋙ (G : A ⥤ A))
      (d : ∀ n : ℕ, Fin (n + 1) → (Z (n + 1) ⟶ Z n))
      (s : ∀ n : ℕ, Fin (n + 1) → (Z (n + 1) ⟶ Z (n + 2))),
      Z 0 = 𝟭 A ∧
      (∀ n : ℕ, d n 0 = eqToHom (hZ n) ≫ Functor.whiskerLeft (Z n) G.ε) ∧
      (∀ (n : ℕ) (j : Fin (n + 1)),
        d (n + 1) j.succ =
          eqToHom (hZ (n + 1)) ≫ Functor.whiskerRight (d n j) (G : A ⥤ A) ≫
            eqToHom (hZ n).symm) ∧
      (∀ n : ℕ,
        s n 0 = eqToHom (hZ n) ≫ Functor.whiskerLeft (Z n) G.δ ≫
          Functor.whiskerRight (eqToHom (hZ n).symm) (G : A ⥤ A) ≫ eqToHom (hZ (n + 1)).symm) ∧
      (∀ (n : ℕ) (j : Fin (n + 1)),
        s (n + 1) j.succ =
          eqToHom (hZ (n + 1)) ≫ Functor.whiskerRight (s n j) (G : A ⥤ A) ≫
            eqToHom (hZ (n + 2)).symm) ∧
      ∃ (X : SimplicialObject.Augmented (A ⥤ A))
        (h : ∀ n : ℕ, X.left.obj (op ⦋n⦌) = Z (n + 1)) (hX : X.right = Z 0),
        (∀ (n : ℕ) (j : Fin (n + 2)),
          X.left.δ j = eqToHom (h (n + 1)) ≫ d (n + 1) j ≫ eqToHom (h n).symm) ∧
        (∀ (n : ℕ) (j : Fin (n + 1)),
          X.left.σ j = eqToHom (h n) ≫ s n j ≫ eqToHom (h (n + 1)).symm) ∧
        X.hom.app (op ⦋0⦌) = eqToHom (h 0) ≫ d 0 0 ≫ eqToHom hX.symm

Tag 08ND, a lemma

Tag 08ND in the Stacks Project.

CategoryTheory.Adjunction.exists_homotopyInverse_whiskered_standardResolution, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/StandardResolution/Basic.lean, line 494.

Stacks 08ND. Let V : A ⥤ S have a left adjoint U : S ⥤ A, and let X be the standard resolution: the augmented simplicial object of A ⥤ A with terms the iterates Z (n + 1) of the comonad U ∘ V, faces and degeneracies d, s whiskering its counit, resp. its comultiplication, into the j-th factor, point Z 0 = 𝟭 A and augmentation ε₀ = d 0 0. Then the whiskered augmentations 1_V ⋆ ε : V ∘ X ⟶ V and ε ⋆ 1_U : X ∘ U ⟶ U are homotopy equivalences: each admits a morphism r in the other direction such that both composites with it are homotopic to the identities, homotopic meaning related by the equivalence relation generated by the existence of a simplicial homotopy.

public theorem exists_homotopyInverse_whiskered_standardResolution
    {A : Type u₁} [Category.{v₁} A] {S : Type u₂} [Category.{v₂} S]
    {U : S ⥤ A} {V : A ⥤ S} (adj : U ⊣ V)
    (Z : ℕ → (A ⥤ A)) (hZ : ∀ n : ℕ, Z (n + 1) = Z n ⋙ (adj.toComonad : A ⥤ A))
    (d : ∀ n : ℕ, Fin (n + 1) → (Z (n + 1) ⟶ Z n))
    (s : ∀ n : ℕ, Fin (n + 1) → (Z (n + 1) ⟶ Z (n + 2)))
    (hZ₀ : Z 0 = 𝟭 A)
    (hd₀ : ∀ n : ℕ, d n 0 = eqToHom (hZ n) ≫ Functor.whiskerLeft (Z n) adj.toComonad.ε)
    (hd : ∀ (n : ℕ) (j : Fin (n + 1)), d (n + 1) j.succ =
      eqToHom (hZ (n + 1)) ≫ Functor.whiskerRight (d n j) (adj.toComonad : A ⥤ A) ≫
        eqToHom (hZ n).symm)
    (hs₀ : ∀ n : ℕ, s n 0 = eqToHom (hZ n) ≫ Functor.whiskerLeft (Z n) adj.toComonad.δ ≫
      Functor.whiskerRight (eqToHom (hZ n).symm) (adj.toComonad : A ⥤ A) ≫
        eqToHom (hZ (n + 1)).symm)
    (hs : ∀ (n : ℕ) (j : Fin (n + 1)), s (n + 1) j.succ =
      eqToHom (hZ (n + 1)) ≫ Functor.whiskerRight (s n j) (adj.toComonad : A ⥤ A) ≫
        eqToHom (hZ (n + 2)).symm)
    (X : SimplicialObject.Augmented (A ⥤ A))
    (h : ∀ n : ℕ, X.left.obj (Opposite.op ⦋n⦌) = Z (n + 1)) (hX : X.right = Z 0)
    (hδ : ∀ (n : ℕ) (j : Fin (n + 2)),
      X.left.δ j = eqToHom (h (n + 1)) ≫ d (n + 1) j ≫ eqToHom (h n).symm)
    (hσ : ∀ (n : ℕ) (j : Fin (n + 1)),
      X.left.σ j = eqToHom (h n) ≫ s n j ≫ eqToHom (h (n + 1)).symm)
    (hε : X.hom.app (Opposite.op ⦋0⦌) = eqToHom (h 0) ≫ d 0 0 ≫ eqToHom hX.symm)
    (a : X.left ⋙ (Functor.whiskeringRight A A S).obj V ⟶
      (Functor.const SimplexCategoryᵒᵖ).obj (X.right ⋙ V))
    (ha : ∀ n : SimplexCategoryᵒᵖ, a.app n = Functor.whiskerRight (X.hom.app n) V)
    (b : X.left ⋙ (Functor.whiskeringLeft S A A).obj U ⟶
      (Functor.const SimplexCategoryᵒᵖ).obj (U ⋙ X.right))
    (hb : ∀ n : SimplexCategoryᵒᵖ, b.app n = Functor.whiskerLeft U (X.hom.app n)) :
    (∃ r : (Functor.const SimplexCategoryᵒᵖ).obj (X.right ⋙ V) ⟶
        X.left ⋙ (Functor.whiskeringRight A A S).obj V,
      Relation.EqvGen (fun f g => Nonempty (SimplicialObject.Homotopy f g)) (a ≫ r) (𝟙 _) ∧
      Relation.EqvGen (fun f g => Nonempty (SimplicialObject.Homotopy f g)) (r ≫ a) (𝟙 _)) ∧
    (∃ r : (Functor.const SimplexCategoryᵒᵖ).obj (U ⋙ X.right) ⟶
        X.left ⋙ (Functor.whiskeringLeft S A A).obj U,
      Relation.EqvGen (fun f g => Nonempty (SimplicialObject.Homotopy f g)) (b ≫ r) (𝟙 _) ∧
      Relation.EqvGen (fun f g => Nonempty (SimplicialObject.Homotopy f g)) (r ≫ b) (𝟙 _))

Tag 0G5T, an example

Tag 0G5T in the Stacks Project.

AlgebraicTopology.homotopyEquivalences_forget_iff_quasiIso_of_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/StandardResolution/Basic.lean, line 1094.

Stacks 0G5T. Let R be a ring and let f : X ⟶ Y be a morphism of simplicial R-modules which is surjective in each degree. Then the underlying morphism of simplicial sets X ⋙ forget ⟶ Y ⋙ forget is a homotopy equivalence — it admits a morphism of simplicial sets back whose two composites with it are homotopic to the identities — if and only if the induced morphism s(X) ⟶ s(Y) of associated chain complexes of R-modules is a quasi-isomorphism. Applied to the augmentation X(M) ⟶ M of the standard resolution of an R-module M by free modules, whose underlying augmentation of simplicial sets is a homotopy equivalence, this says that M is the only nonzero homology group of the complex associated to X(M).

public theorem homotopyEquivalences_forget_iff_quasiIso_of_surjective {R : Type u} [Ring R]
    {X Y : SimplicialObject (ModuleCat.{v} R)} (f : X ⟶ Y)
    (hf : ∀ n : SimplexCategoryᵒᵖ, Function.Surjective (f.app n).hom) :
    SimplicialObject.homotopyEquivalences (Type v)
        (Functor.whiskerRight f (forget (ModuleCat.{v} R))) ↔
      QuasiIso ((alternatingFaceMapComplex (ModuleCat.{v} R)).map f)

Tag 08NA, an example

Tag 08NA in the Stacks Project.

AlgebraicTopology.homotopyEquivalences_forget_iff_quasiIso_forget₂_of_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/StandardResolution/Basic.lean, line 1115.

Stacks 08NA. Let A be a ring and let f : X ⟶ Y be a morphism of simplicial A-algebras which is surjective in each degree. Then the underlying morphism of simplicial sets is a homotopy equivalence if and only if the induced morphism s(X) ⟶ s(Y) of the chain complexes associated to the underlying simplicial A-modules is a quasi-isomorphism. Applied to the augmentation X(B) ⟶ B of the standard resolution of a commutative A-algebra B by the polynomial algebras A[A[⋯[B]⋯]], whose underlying augmentation of simplicial sets is a homotopy equivalence, this says that B is the only nonzero homology group of the complex of A-modules associated to X(B).

public theorem homotopyEquivalences_forget_iff_quasiIso_forget₂_of_surjective {A : Type u}
    [CommRing A] {X Y : SimplicialObject (AlgCat.{v} A)} (f : X ⟶ Y)
    (hf : ∀ n : SimplexCategoryᵒᵖ, Function.Surjective (f.app n).hom) :
    SimplicialObject.homotopyEquivalences (Type v)
        (Functor.whiskerRight f (forget (AlgCat.{v} A))) ↔
      QuasiIso ((alternatingFaceMapComplex (ModuleCat.{v} A)).map
        (Functor.whiskerRight f (forget₂ (AlgCat.{v} A) (ModuleCat.{v} A))))

Tag 0G5U, an example

Tag 0G5U in the Stacks Project.

ModuleCat.free_standardResolution_face_degeneracy_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/StandardResolution/Basic.lean, line 1179.

Stacks 0G5U. Let R be a ring, M an R-module and R[N] the free R-module on the underlying set of an R-module N, with [n] = ModuleCat.comonadMk n and ∑ᵢ f nᵢ rᵢ = ModuleCat.comonadSum ξ f for ξ = ∑ᵢ rᵢ[nᵢ]. For the simplicial R-module X(M) with X₁(M) = R[R[M]] and X₂(M) = R[R[R[M]]], and a typical element ξ = ∑ᵢ rᵢ[∑ⱼ r_ij[m_ij]] of X₁(M), the two faces d₀, d₁ : R[R[M]] → R[M] — the counit of the free-forgetful adjunction contracting the outer, resp. the inner, bracket — are given by d₀(ξ) = ∑_{i,j} rᵢr_ij[m_ij] and d₁(ξ) = ∑ᵢ rᵢ[∑ⱼ r_ij m_ij], and the two degeneracies s₀, s₁ : R[R[M]] → R[R[R[M]]] — its comultiplication doubling the outer, resp. the inner, bracket — by s₀(ξ) = ∑ᵢ rᵢ[[∑ⱼ r_ij[m_ij]]] and s₁(ξ) = ∑ᵢ rᵢ[∑ⱼ r_ij[[m_ij]]].

public theorem free_standardResolution_face_degeneracy_apply {R : Type u} [Ring R]
    (M : ModuleCat.{u} R)
    (ξ : ((adj R).toComonad.obj ((adj R).toComonad.obj M) : Type u)) :
    (adj R).toComonad.ε.app ((adj R).toComonad.obj M) ξ = comonadSum ξ (fun x r => r • x) ∧
      (adj R).toComonad.map ((adj R).toComonad.ε.app M) ξ =
        comonadSum ξ (fun x r => r • comonadMk (comonadSum x (fun m c => c • m))) ∧
      (adj R).toComonad.δ.app ((adj R).toComonad.obj M) ξ =
        comonadSum ξ (fun x r => r • comonadMk (comonadMk x)) ∧
      (adj R).toComonad.map ((adj R).toComonad.δ.app M) ξ =
        comonadSum ξ (fun x r =>
          r • comonadMk (comonadSum x (fun m c => c • comonadMk (comonadMk m))))

Tag 09CB, an example

Tag 09CB in the Stacks Project.

AlgCat.face_eq_lift_and_degeneracy_eq_lift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/StandardResolution/Basic.lean, line 607.

Stacks 09CB. Let A be a ring and let X be an A-algebra. In the tower Xₙ = A[A[⋯[X]⋯]] (n + 1 brackets) of the standard resolution of X for the free/forget adjunction, each stage being the free algebra on the previous one, the faces dⁿⱼ and degeneracies sⁿⱼ are described on the variables by: dⁿ₀ substitutes for the variable [z] the element z, so it is FreeAlgebra.lift A id and d⁰₀ : A[X] ⟶ X is the augmentation; sⁿ₀ sends [z] to [[z]]; and dⁿ⁺¹ⱼ₊₁, sⁿ⁺¹ⱼ₊₁ send [z] to [dⁿⱼ(z)], resp. [sⁿⱼ(z)]. In degree 1, for x = ∑ a_k [b_{k,1}] ⋯ [b_{k,n_k}] ∈ A[X], this is d₀([x]) = x, d₁([x]) = [∑ a_k b_{k,1} ⋯ b_{k,n_k}], s₀([x]) = [[x]] and s₁([x]) = [∑ a_k [[b_{k,1}]] ⋯ [[b_{k,n_k}]]].

public theorem face_eq_lift_and_degeneracy_eq_lift {A : Type u} [CommRing A] (X : AlgCat.{u} A)
    (n : ℕ) :
    ((Godement.face (adj (R := A)).toComonad.ε n 0).app X).hom = FreeAlgebra.lift A id ∧
      (∀ j : Fin (n + 1), ((Godement.face (adj (R := A)).toComonad.ε (n + 1) j.succ).app X).hom =
        FreeAlgebra.lift A (FreeAlgebra.ι A ∘
          ((Godement.face (adj (R := A)).toComonad.ε n j).app X).hom)) ∧
      ((Godement.degeneracy (adj (R := A)).toComonad.δ n 0).app X).hom =
        FreeAlgebra.lift A (fun z => FreeAlgebra.ι A (FreeAlgebra.ι A z)) ∧
      (∀ j : Fin (n + 1),
        ((Godement.degeneracy (adj (R := A)).toComonad.δ (n + 1) j.succ).app X).hom =
          FreeAlgebra.lift A (FreeAlgebra.ι A ∘
            ((Godement.degeneracy (adj (R := A)).toComonad.δ n j).app X).hom))

Tag 08NE, an example

Tag 08NE in the Stacks Project.

AlgCat.exists_homotopyInverse_whiskered_standardResolution, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicTopology/StandardResolution/Basic.lean, line 967.

Stacks 08NE. Let A be a ring, let U : Sets → Alg_A be the free algebra functor and V the forgetful functor, and let X be the standard resolution of the comonad Y = U ∘ V: the augmented simplicial object of Fun(Alg_A, Alg_A) with terms the iterates Xₙ = Y^{n+1}, so that Xₙ(B) = A[A[⋯[B]⋯]] with n + 1 brackets, faces Godement.face, degeneracies Godement.degeneracy, point 𝟭 and augmentation d⁰₀. Then the whiskered augmentations 1_V ⋆ ε : V ∘ X ⟶ V and ε ⋆ 1_U : X ∘ U ⟶ U are homotopy equivalences with their homotopy inverses displayed: in degree n the first is the map of sets b ↦ [⋯[b]⋯] (n + 1 brackets) and the second is the A-algebra map ∑ a [e₁]⋯[e_p] ↦ ∑ a [⋯[e₁]⋯]⋯[⋯[e_p]⋯] sending a variable [e] to [⋯[e]⋯] (n + 2 brackets), and both composites of each with the augmentation are homotopic to the identity, homotopic meaning related by the equivalence relation generated by the existence of a simplicial homotopy. Evaluating the first clause at an A-algebra B gives the homotopy equivalence of the underlying simplicial sets of X(B) ⟶ B, and the second at a set E the homotopy equivalence of simplicial A-algebras X(A[E]) ⟶ A[E].

public theorem exists_homotopyInverse_whiskered_standardResolution {A : Type u} [CommRing A]
    (X : SimplicialObject.Augmented (AlgCat.{u} A ⥤ AlgCat.{u} A))
    (h : ∀ n : ℕ, X.left.obj (op ⦋n⦌) =
      (AlgCat.adj A).toComonad.toFunctor.iterate (n + 1))
    (hX : X.right = 𝟭 (AlgCat.{u} A))
    (hδ : ∀ (n : ℕ) (j : Fin (n + 2)), X.left.δ j =
      eqToHom (h (n + 1)) ≫ Godement.face (AlgCat.adj A).toComonad.ε (n + 1) j ≫
        eqToHom (h n).symm)
    (hσ : ∀ (n : ℕ) (j : Fin (n + 1)), X.left.σ j =
      eqToHom (h n) ≫ Godement.degeneracy (AlgCat.adj A).toComonad.δ n j ≫
        eqToHom (h (n + 1)).symm)
    (hε : X.hom.app (op ⦋0⦌) =
      eqToHom (h 0) ≫ Godement.face (AlgCat.adj A).toComonad.ε 0 0 ≫ eqToHom hX.symm)
    (a : X.left ⋙ (Functor.whiskeringRight (AlgCat.{u} A) (AlgCat.{u} A) (Type u)).obj
        (forget (AlgCat.{u} A)) ⟶
      (Functor.const SimplexCategoryᵒᵖ).obj (X.right ⋙ forget (AlgCat.{u} A)))
    (ha : ∀ n : SimplexCategoryᵒᵖ,
      a.app n = Functor.whiskerRight (X.hom.app n) (forget (AlgCat.{u} A)))
    (b : X.left ⋙ (Functor.whiskeringLeft (Type u) (AlgCat.{u} A) (AlgCat.{u} A)).obj
        (AlgCat.free A) ⟶
      (Functor.const SimplexCategoryᵒᵖ).obj (AlgCat.free A ⋙ X.right))
    (hb : ∀ n : SimplexCategoryᵒᵖ,
      b.app n = Functor.whiskerLeft (AlgCat.free A) (X.hom.app n))
    (ρ : ∀ n : ℕ, forget (AlgCat.{u} A) ⟶
      (AlgCat.adj A).toComonad.toFunctor.iterate (n + 1) ⋙ forget (AlgCat.{u} A))
    (hρ₀ : ∀ (B : AlgCat.{u} A) (x : B), (ρ 0).app B x = comonadι B x)
    (hρ : ∀ (n : ℕ) (B : AlgCat.{u} A) (x : B),
      (ρ (n + 1)).app B x = comonadι _ ((ρ n).app B x))
    (τ : ∀ n : ℕ, AlgCat.free A ⟶
      AlgCat.free A ⋙ (AlgCat.adj A).toComonad.toFunctor.iterate (n + 1))
    (hτ₀ : ∀ (E : Type u) (e : E), ((τ 0).app E).hom (freeι E e) = comonadι _ (freeι E e))
    (hτ : ∀ (n : ℕ) (E : Type u) (e : E), ((τ (n + 1)).app E).hom (freeι E e) =
      comonadι _ (((τ n).app E).hom (freeι E e))) :
    (∃ r : (Functor.const SimplexCategoryᵒᵖ).obj (X.right ⋙ forget (AlgCat.{u} A)) ⟶
        X.left ⋙ (Functor.whiskeringRight (AlgCat.{u} A) (AlgCat.{u} A) (Type u)).obj
          (forget (AlgCat.{u} A)),
      (∀ n : ℕ, r.app (op ⦋n⦌) =
        eqToHom (congrArg (fun F => F ⋙ forget (AlgCat.{u} A)) hX) ≫ ρ n ≫
          eqToHom (congrArg (fun F => F ⋙ forget (AlgCat.{u} A)) (h n)).symm) ∧
      Relation.EqvGen (fun f g => Nonempty (SimplicialObject.Homotopy f g)) (a ≫ r) (𝟙 _) ∧
      Relation.EqvGen (fun f g => Nonempty (SimplicialObject.Homotopy f g)) (r ≫ a) (𝟙 _)) ∧
    (∃ r : (Functor.const SimplexCategoryᵒᵖ).obj (AlgCat.free A ⋙ X.right) ⟶
        X.left ⋙ (Functor.whiskeringLeft (Type u) (AlgCat.{u} A) (AlgCat.{u} A)).obj
          (AlgCat.free A),
      (∀ n : ℕ, r.app (op ⦋n⦌) =
        eqToHom (congrArg (fun F => AlgCat.free A ⋙ F) hX) ≫ τ n ≫
          eqToHom (congrArg (fun F => AlgCat.free A ⋙ F) (h n)).symm) ∧
      Relation.EqvGen (fun f g => Nonempty (SimplicialObject.Homotopy f g)) (b ≫ r) (𝟙 _) ∧
      Relation.EqvGen (fun f g => Nonempty (SimplicialObject.Homotopy f g)) (r ≫ b) (𝟙 _))

Sources

LeanCategoryTheory.Adjunction · CategoryTheory.Adjunction.right_triangle · CategoryTheory.Adjunction.left_triangle · CategoryTheory.Comonad.exists_augmented_standardResolution · CategoryTheory.Adjunction.exists_homotopyInverse_whiskered_standardResolution · AlgebraicTopology.homotopyEquivalences_forget_iff_quasiIso_of_surjective · AlgebraicTopology.homotopyEquivalences_forget_iff_quasiIso_forget₂_of_surjective · ModuleCat.free_standardResolution_face_degeneracy_apply

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

14.23 Simplicial objects and… to 14.34 Standard resolutions

Section14.23 Simplicial objects and chain complexes#

Tag 0195, a lemma

Tag 0196, a lemma

Tag 0197, a lemma

Tag 0198, a lemma

Tag 0199, a lemma

Tag 019A, a lemma

Tag 0FKI, a remark

Tag 019B, a lemma

Tag 019C, a lemma

Sources

Section14.24 Dold-Kan#

Tag 019E, a lemma

Tag 019F, a lemma

Tag 019G, a theorem

Sources

Section14.25 Dold-Kan for cosimplicial objects#

Tag 019I, a lemma

Sources

Section14.26 Homotopies#

Tag 019K, a definition

Tag 019L, a lemma

Tag 019M, a remark

Tag 08RJ, a remark

Tag 019N, a definition

Tag 08Q3, an example

Tag 019O, a lemma

Tag 019P, a lemma

Tag 08Q4, a lemma

Sources

Section14.27 Homotopies in abelian categories#

Tag 019R, an equation

Tag 019S, a lemma

Tag 019T, a lemma

Sources

Section14.28 Homotopies and cosimplicial objects#

Tag 019W, a definition

Tag 07KB, an equation

Tag 0FKJ, a remark

Tag 019X, a lemma

Tag 019Y, a lemma

Tag 019Z, a lemma

Tag 01A0, a lemma

Tag 0FKK, a lemma

Sources

Section14.29 More homotopies in abelian categories#

Tag 01A2, a lemma

Tag 01A3, a lemma

Tag 01A4, a lemma

Sources

Section14.30 Trivial Kan fibrations#

Tag 08NL, a definition

Tag 08NM, a lemma

Tag 08NN, a lemma

Tag 08NP, a lemma

Tag 08NQ, a lemma

Tag 08NR, a lemma

Tag 08Q5, a lemma

Tag 08NS, a lemma

Sources

Section14.31 Kan fibrations#

Tag 08NU, a definition

Tag 08NV, a lemma

Tag 08NW, a lemma

Tag 08NX, a lemma

Tag 08NY, a lemma

Tag 08NZ, a lemma

Tag 08P0, a lemma

Tag 08P1, a lemma

Tag 08P2, a lemma

Sources

Section14.32 A homotopy equivalence#

Tag 01A6, a lemma

Tag 01A9, a lemma

Tag 01AB, a lemma

Sources

Section14.33 Preparation for standard resolutions#

Tag 0G5M, an example

Tag 0G5N, a lemma

Section14.23 Simplicial objects and chain complexes #

Section14.24 Dold-Kan #

Section14.25 Dold-Kan for cosimplicial objects #

Section14.26 Homotopies #

Section14.27 Homotopies in abelian categories #

Section14.28 Homotopies and cosimplicial objects #

Section14.29 More homotopies in abelian categories #

Section14.30 Trivial Kan fibrations #

Section14.31 Kan fibrations #

Section14.32 A homotopy equivalence #

Section14.33 Preparation for standard resolutions #

Section14.34 Standard resolutions #