From 41bcf038e6080d57b3f20f26379d2d84b6effe46 Mon Sep 17 00:00:00 2001 From: Emily Riehl Date: Wed, 29 Jan 2025 15:38:42 -0500 Subject: [PATCH] some sorried WalkingIso infrastructure plus a new map --- .../SimplicialSet/CoherentIso.lean | 84 ++++++++++++++++++- .../SimplicialSet/CoherentIsoModels.lean | 37 +++++++- 2 files changed, 116 insertions(+), 5 deletions(-) diff --git a/InfinityCosmos/ForMathlib/AlgebraicTopology/SimplicialSet/CoherentIso.lean b/InfinityCosmos/ForMathlib/AlgebraicTopology/SimplicialSet/CoherentIso.lean index 63d95ab..2d1395a 100644 --- a/InfinityCosmos/ForMathlib/AlgebraicTopology/SimplicialSet/CoherentIso.lean +++ b/InfinityCosmos/ForMathlib/AlgebraicTopology/SimplicialSet/CoherentIso.lean @@ -5,8 +5,9 @@ Authors: Johns Hopkins Category Theory Seminar -/ import InfinityCosmos.ForMathlib.AlgebraicTopology.SimplicialCategory.Basic -import Mathlib.CategoryTheory.CodiscreteCategory +import Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal import Mathlib.AlgebraicTopology.SimplicialSet.Nerve +import Mathlib.CategoryTheory.CodiscreteCategory universe u v u' v' @@ -77,10 +78,85 @@ end CategoryTheory namespace SSet def coherentIso : SSet.{u} := nerve WalkingIso +namespace coherentIso + +open Simplicial SimplicialCategory SSet SimplexCategory Truncated Functor + +def pt (i : WalkingIso) : Δ[0] ⟶ coherentIso := + (yonedaEquiv coherentIso _).symm (WalkingIso.coev i) + +def oneSimplex (X₀ X₁ : WalkingIso) : Δ[1] ⟶ coherentIso := + (yonedaEquiv coherentIso _).symm + (ComposableArrows.mk₁ (X₀ := X₀) (X₁ := X₁) ⟨⟩) + +theorem oneSimplex_ext {X₀ X₁ Y₀ Y₁ : WalkingIso} (e₀ : X₀ = Y₀) (e₁ : X₁ = Y₁) : + oneSimplex X₀ X₁ = oneSimplex Y₀ Y₁ := + congrArg (yonedaEquiv coherentIso _).symm (ComposableArrows.ext₁ e₀ e₁ rfl) + +def twoSimplex (X₀ X₁ X₂ : WalkingIso) : Δ[2] ⟶ coherentIso := + (yonedaEquiv coherentIso _).symm + (ComposableArrows.mk₂ (X₀ := X₀) (X₁ := X₁) (X₂ := X₂) ⟨⟩ ⟨⟩) + +theorem oneSimplex_const (X₀ : WalkingIso) : + oneSimplex X₀ X₀ = stdSimplex.map ([1].const [0] 0) ≫ pt X₀ := by + unfold oneSimplex pt + sorry + +theorem twoSimplex_δ0 (X₀ X₁ X₂ : WalkingIso) : + stdSimplex.δ 0 ≫ twoSimplex X₀ X₁ X₂ = oneSimplex X₁ X₂ := rfl + +theorem twoSimplex_δ1 (X₀ X₁ X₂ : WalkingIso) : + stdSimplex.δ 1 ≫ twoSimplex X₀ X₁ X₂ = oneSimplex X₀ X₂ := by + unfold twoSimplex oneSimplex + sorry + +theorem twoSimplex_δ2 (X₀ X₁ X₂ : WalkingIso) : + stdSimplex.δ 2 ≫ twoSimplex X₀ X₁ X₂ = oneSimplex X₀ X₁ := by + unfold twoSimplex oneSimplex + sorry + + + +theorem twoSimplex_ext {X₀ X₁ X₂ Y₀ Y₁ Y₂ : WalkingIso} + (e₀ : X₀ = Y₀) (e₁ : X₁ = Y₁) (e₂ : X₂ = Y₂) : twoSimplex X₀ X₁ X₂ = twoSimplex Y₀ Y₁ Y₂ := + congrArg (yonedaEquiv coherentIso _).symm (ComposableArrows.ext₂ e₀ e₁ e₂ rfl rfl) + +def hom : Δ[1] ⟶ coherentIso := + (yonedaEquiv coherentIso _).symm + (ComposableArrows.mk₁ (X₀ := WalkingIso.zero) (X₁ := WalkingIso.one) ⟨⟩) + +def inv : Δ[1] ⟶ coherentIso := + (yonedaEquiv coherentIso _).symm + (ComposableArrows.mk₁ (X₀ := WalkingIso.one) (X₁ := WalkingIso.zero) ⟨⟩) + +def homInvId : Δ[2] ⟶ coherentIso := + (yonedaEquiv coherentIso _).symm + (ComposableArrows.mk₂ + (X₀ := WalkingIso.zero) (X₁ := WalkingIso.one) (X₂ := WalkingIso.zero) ⟨⟩ ⟨⟩) + +noncomputable def isPointwiseRightKanExtensionAt (n : ℕ) : + (rightExtensionInclusion coherentIso 0).IsPointwiseRightKanExtensionAt ⟨[n]⟩ where + lift s x := sorry + fac s j := sorry + uniq s m hm := sorry + +noncomputable def isPointwiseRightKanExtension : + (rightExtensionInclusion coherentIso 0).IsPointwiseRightKanExtension := + fun Δ => isPointwiseRightKanExtensionAt Δ.unop.len + +theorem isRightKanExtension : + coherentIso.IsRightKanExtension (𝟙 ((Truncated.inclusion 0).op ⋙ coherentIso)) := + RightExtension.IsPointwiseRightKanExtension.isRightKanExtension + isPointwiseRightKanExtension + +theorem is0Coskeletal : SimplicialObject.IsCoskeletal (n := 0) (coherentIso) where + isRightKanExtension := isRightKanExtension + +def simplex {n : ℕ} (obj : Fin n → WalkingIso) : Δ[n] ⟶ coherentIso := sorry -open Simplicial SimplicialCategory +def simplex_ext {n : ℕ} (obj obj' : Fin n → WalkingIso) + (hyp : (i : Fin n) → obj i = obj' i) : coherentIso.simplex obj = coherentIso.simplex obj' := sorry -def coherentIso.pt (i : WalkingIso) : Δ[0] ⟶ coherentIso := - (yonedaEquiv coherentIso [0]).symm (WalkingIso.coev i) +end coherentIso end SSet diff --git a/InfinityCosmos/ForMathlib/AlgebraicTopology/SimplicialSet/CoherentIsoModels.lean b/InfinityCosmos/ForMathlib/AlgebraicTopology/SimplicialSet/CoherentIsoModels.lean index 8e4f7cc..1801bc7 100644 --- a/InfinityCosmos/ForMathlib/AlgebraicTopology/SimplicialSet/CoherentIsoModels.lean +++ b/InfinityCosmos/ForMathlib/AlgebraicTopology/SimplicialSet/CoherentIsoModels.lean @@ -20,6 +20,7 @@ def delta12' : Δ[1] ⟶ Δ[2] := stdSimplex.δ 0 --TODO: Figure out if this is /-- The edge in Δ[2] from vertex 0 to 1 -/ def delta01 : Δ[1] ⟶ Δ[2] := mapFromSimplex (edge 2 0 1 (by decide)) +def delta01' : Δ[1] ⟶ Δ[2] := stdSimplex.δ 2 --TODO: Figure out if this is a better way to define /-- The pushout of the diagram Δ[1] --> Δ[2] @@ -38,6 +39,7 @@ representing the following square shaped diagram: 2 ------> 3 -/ noncomputable def Sq := pushout delta12 delta01 +noncomputable def Sq' := pushout (stdSimplex.δ 0 : Δ[1] ⟶ Δ[2]) (stdSimplex.δ 2 : Δ[1] ⟶ Δ[2]) /-- The map X ⨿ Y ⟶ Z ⨿ W defined by maps X ⟶ Z and Y ⟶ W -/ noncomputable def mapOnComponents {C} [Category C] {X Y Z W : C} [HasColimits C] (f : X ⟶ Z) (g : Y ⟶ W) @@ -45,9 +47,13 @@ noncomputable def mapOnComponents {C} [Category C] {X Y Z W : C} [HasColimits C] /-- The constant map of any Δ[n] into Δ[0] corresponding to the unique degenerate n-simplex -/ def constantMap (n : ℕ) : Δ[n] ⟶ Δ[0] := mapFromSimplex (const 0 0 _) +def constantMap' (n : ℕ) : Δ[n] ⟶ Δ[0] := stdSimplex.map (SimplexCategory.const _ _ 0) noncomputable def map0Coprod0 : (Δ[1] ⨿ Δ[1] ⟶ Δ[0] ⨿ Δ[0] : Type u) := mapOnComponents (constantMap 1) (constantMap 1) +noncomputable def map0Coprod0' : (Δ[1] ⨿ Δ[1] ⟶ Δ[0] ⨿ Δ[0] : Type u) := + coprod.map + (stdSimplex.map (SimplexCategory.const _ _ 0)) (stdSimplex.map (SimplexCategory.const _ _ 0)) /-- The map Δ[1] ⨿ Δ[1] defined by the two maps @@ -58,8 +64,13 @@ The map Δ[1] ⨿ Δ[1] defined by the two maps delta12 ι₂ Δ[1] -------> Δ[2] -------> Sq -/ +-- ER: Warning: this is wrong: replace the lefthand instances of delta01 with delta02! noncomputable def map01Coprod34 : (Δ[1] ⨿ Δ[1] ⟶ Sq : Type u) := - coprod.desc (delta01 ≫ (pushout.inl delta12 delta01)) (delta01 ≫ (pushout.inr delta12 delta01)) + coprod.desc (delta01 ≫ (pushout.inl delta12 delta01)) (delta01 ≫ (pushout.inr delta12 delta01)) +noncomputable def map01Coprod34' : (Δ[1] ⨿ Δ[1] ⟶ Sq' : Type u) := + coprod.desc + ((stdSimplex.δ 1) ≫ (pushout.inl delta12' delta01')) + ((stdSimplex.δ 1) ≫ (pushout.inr delta12' delta01')) /-- The pushout of the diagram @@ -82,12 +93,35 @@ which we can visualize as the following square meaning we can recognize the map from 1 to 2 having a left and right inverse. -/ noncomputable def Model2dCoherentIso := pushout map01Coprod34 map0Coprod0 +noncomputable def Model2dCoherentIso' := pushout map01Coprod34' map0Coprod0' + +noncomputable def map2dModel'toCoherentIso : Model2dCoherentIso' ⟶ coherentIso := by + refine pushout.desc ?_ ?_ ?_ + · refine pushout.desc ?_ ?_ ?_ + · exact (coherentIso.twoSimplex WalkingIso.zero WalkingIso.one WalkingIso.zero) + · exact (coherentIso.twoSimplex WalkingIso.one WalkingIso.zero WalkingIso.one) + · rw [coherentIso.twoSimplex_δ0 WalkingIso.zero WalkingIso.one WalkingIso.zero] + rw [← coherentIso.twoSimplex_δ2 WalkingIso.one WalkingIso.zero WalkingIso.one] + · exact coprod.desc (coherentIso.pt WalkingIso.zero) (coherentIso.pt WalkingIso.one) + · unfold map0Coprod0' map01Coprod34' + apply coprod.hom_ext + · unfold delta01' delta12' + simp only [coprod.desc_comp, Category.assoc, colimit.ι_desc, PushoutCocone.mk_pt, + PushoutCocone.mk_ι_app, BinaryCofan.ι_app_left, BinaryCofan.mk_inl, coprod.map_desc] + rw [coherentIso.twoSimplex_δ1 _ _ _, ← coherentIso.oneSimplex_const] + · unfold delta01' delta12' + simp only [coprod.desc_comp, Category.assoc, colimit.ι_desc, + PushoutCocone.mk_pt, PushoutCocone.mk_ι_app, + BinaryCofan.mk_pt, BinaryCofan.ι_app_right, BinaryCofan.mk_inr, coprod.map_desc] + rw [coherentIso.twoSimplex_δ1 _ _ _, ← coherentIso.oneSimplex_const] /-- The 0-simplex at vertex 0 of Δ[1] -/ def delta0 : Δ[0] ⟶ Δ[1] := mapFromSimplex (const 1 0 (Opposite.op [0])) +def delta0' : Δ[0] ⟶ Δ[1] := stdSimplex.δ 1 /-- The 0-simplex at vertex 1 of Δ[1] -/ def delta1 : Δ[0] ⟶ Δ[1] := mapFromSimplex (const 1 1 (Opposite.op [0])) +def delta1' : Δ[0] ⟶ Δ[1] := stdSimplex.δ 0 /-- The pushout of the diagram @@ -102,6 +136,7 @@ representing the diagram 1 <--- 0 ---> 1 -/ noncomputable def Cospan00 := pushout delta0 delta0 +noncomputable def Cospan00' := pushout delta0' delta0' /-- The pushout of the diagram