From 86e936232dc0f78d82fbf2e918b36bd74107176b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Tue, 30 Aug 2022 09:26:20 +0000 Subject: [PATCH] feat(algebraic_topology): the category simplicial_object.split (#16274) This PR introduces the category of simplicial objects equipped with a splitting. --- .../split_simplicial_object.lean | 122 +++++++++++++++++- 1 file changed, 121 insertions(+), 1 deletion(-) diff --git a/src/algebraic_topology/split_simplicial_object.lean b/src/algebraic_topology/split_simplicial_object.lean index 892ae93101879..eef5946db01dd 100644 --- a/src/algebraic_topology/split_simplicial_object.lean +++ b/src/algebraic_topology/split_simplicial_object.lean @@ -14,7 +14,8 @@ import category_theory.limits.shapes.finite_products In this file, we introduce the notion of split simplicial object. If `C` is a category that has finite coproducts, a splitting `s : splitting X` of a simplical object `X` in `C` consists -of the datum of a sequence of objects `s.N : ℕ → C` and a +of the datum of a sequence of objects `s.N : ℕ → C` (which +we shall refer to as "nondegenerate simplices") and a sequence of morphisms `s.ι n : s.N n → X _[n]` that have the property that a certain canonical map identifies `X _[n]` with the coproduct of objects `s.N i` indexed by all possible @@ -23,6 +24,9 @@ assume that the morphisms `s.ι n` are monomorphisms: in the most common categories, this would be a consequence of the axioms.) +Simplicial objects equipped with a splitting form a category +`simplicial_object.split C`. + ## References * [Stacks: Splitting simplicial objects] https://stacks.math.columbia.edu/tag/017O @@ -223,6 +227,122 @@ begin erw [colimit.ι_desc, cofan.mk_ι_app], end +/-- A simplicial object that is isomorphic to a split simplicial object is split. -/ +@[simps] +def of_iso (e : X ≅ Y) : splitting Y := +{ N := s.N, + ι := λ n, s.ι n ≫ e.hom.app (op [n]), + map_is_iso' := λ Δ, begin + convert (infer_instance : is_iso ((s.iso Δ).hom ≫ e.hom.app Δ)), + tidy, + end, } + end splitting +variable (C) + +/-- The category `simplicial_object.split C` is the category of simplicial objects +in `C` equipped with a splitting, and morphisms are morphisms of simplicial objects +which are compatible with the splittings. -/ +@[ext, nolint has_nonempty_instance] +structure split := (X : simplicial_object C) (s : splitting X) + +namespace split + +variable {C} + +/-- The object in `simplicial_object.split C` attached to a splitting `s : splitting X` +of a simplicial object `X`. -/ +@[simps] +def mk' {X : simplicial_object C} (s : splitting X) : split C := ⟨X, s⟩ + +/-- Morphisms in `simplicial_object.split C` are morphisms of simplicial objects that +are compatible with the splittings. -/ +@[nolint has_nonempty_instance] +structure hom (S₁ S₂ : split C) := +(F : S₁.X ⟶ S₂.X) +(f : Π (n : ℕ), S₁.s.N n ⟶ S₂.s.N n) +(comm' : ∀ (n : ℕ), S₁.s.ι n ≫ F.app (op [n]) = f n ≫ S₂.s.ι n) + +@[ext] +lemma hom.ext {S₁ S₂ : split C} (Φ₁ Φ₂ : hom S₁ S₂) (h : ∀ (n : ℕ), Φ₁.f n = Φ₂.f n) : + Φ₁ = Φ₂ := +begin + rcases Φ₁ with ⟨F₁, f₁, c₁⟩, + rcases Φ₂ with ⟨F₂, f₂, c₂⟩, + have h' : f₁ = f₂ := by { ext, apply h, }, + subst h', + simp only [eq_self_iff_true, and_true], + apply S₁.s.hom_ext, + intro n, + dsimp, + rw [c₁, c₂], +end + +restate_axiom hom.comm' +attribute [simp, reassoc] hom.comm + +end split + +instance : category (split C) := +{ hom := split.hom, + id := λ S, { F := 𝟙 _, f := λ n, 𝟙 _, comm' := by tidy, }, + comp := λ S₁ S₂ S₃ Φ₁₂ Φ₂₃, + { F := Φ₁₂.F ≫ Φ₂₃.F, f := λ n, Φ₁₂.f n ≫ Φ₂₃.f n, comm' := by tidy, }, } + +variable {C} + +namespace split + +lemma congr_F {S₁ S₂ : split C} {Φ₁ Φ₂ : S₁ ⟶ S₂} (h : Φ₁ = Φ₂) : Φ₁.F = Φ₂.F := by rw h +lemma congr_f {S₁ S₂ : split C} {Φ₁ Φ₂ : S₁ ⟶ S₂} (h : Φ₁ = Φ₂) (n : ℕ) : + Φ₁.f n = Φ₂.f n := by rw h + +@[simp] +lemma id_F (S : split C) : (𝟙 S : S ⟶ S).F = 𝟙 (S.X) := rfl + +@[simp] +lemma id_f (S : split C) (n : ℕ) : (𝟙 S : S ⟶ S).f n = 𝟙 (S.s.N n) := rfl + +@[simp] +lemma comp_F {S₁ S₂ S₃ : split C} (Φ₁₂ : S₁ ⟶ S₂) (Φ₂₃ : S₂ ⟶ S₃) : + (Φ₁₂ ≫ Φ₂₃).F = Φ₁₂.F ≫ Φ₂₃.F := rfl + +@[simp] +lemma comp_f {S₁ S₂ S₃ : split C} (Φ₁₂ : S₁ ⟶ S₂) (Φ₂₃ : S₂ ⟶ S₃) (n : ℕ) : + (Φ₁₂ ≫ Φ₂₃).f n = Φ₁₂.f n ≫ Φ₂₃.f n := rfl + +@[simp, reassoc] +lemma ι_summand_naturality_symm {S₁ S₂ : split C} (Φ : S₁ ⟶ S₂) + {Δ : simplex_categoryᵒᵖ} (A : splitting.index_set Δ) : + S₁.s.ι_summand A ≫ Φ.F.app Δ = Φ.f A.1.unop.len ≫ S₂.s.ι_summand A := +by rw [S₁.s.ι_summand_eq, S₂.s.ι_summand_eq, assoc, Φ.F.naturality, ← Φ.comm_assoc] + +variable (C) + +/-- The functor `simplicial_object.split C ⥤ simplicial_object C` which forgets +the splitting. -/ +@[simps] +def forget : split C ⥤ simplicial_object C := +{ obj := λ S, S.X, + map := λ S₁ S₂ Φ, Φ.F, } + +/-- The functor `simplicial_object.split C ⥤ C` which sends a simplicial object equipped +with a splitting to its nondegenerate `n`-simplices. -/ +@[simps] +def eval_N (n : ℕ) : split C ⥤ C := +{ obj := λ S, S.s.N n, + map := λ S₁ S₂ Φ, Φ.f n, } + +/-- The inclusion of each summand in the coproduct decomposition of simplices +in split simplicial objects is a natural transformation of functors +`simplicial_object.split C ⥤ C` -/ +@[simps] +def nat_trans_ι_summand {Δ : simplex_categoryᵒᵖ} (A : splitting.index_set Δ) : + eval_N C A.1.unop.len ⟶ forget C ⋙ (evaluation simplex_categoryᵒᵖ C).obj Δ := +{ app := λ S, S.s.ι_summand A, + naturality' := λ S₁ S₂ Φ, (ι_summand_naturality_symm Φ A).symm, } + +end split + end simplicial_object