some sorried WalkingIso infrastructure plus a new map

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

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,16 +39,21 @@ 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)
     : (X ⨿ Y ⟶ Z ⨿ W : Type u) := coprod.desc (f ≫ coprod.inl) (g ≫ coprod.inr)
 
 /-- 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