feat(algebraic_topology/cech_nerve): The Cech nerve is a right adjoin…

…t. (#7716)

Also fixes the namespace in the file `algebraic_topology/cech_nerve.lean`.

This is needed for LTE



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/algebraic_topology/cech_nerve.lean

@@ -44,7 +44,7 @@ def cech_nerve : simplicial_object C :=
 { obj := λ n, wide_pullback f.right
     (λ i : ulift (fin (n.unop.len + 1)), f.left) (λ i, f.hom),
   map := λ m n g, wide_pullback.lift (wide_pullback.base _)
-    (λ i, wide_pullback.π _ $ ulift.up $ g.unop.to_preorder_hom i.down) (by tidy) }
+    (λ i, wide_pullback.π (λ i, f.hom) $ ulift.up $ g.unop.to_preorder_hom i.down) (by tidy) }
 
 /-- The augmented Čech nerve associated to an arrow. -/
 @[simps]
@@ -55,6 +55,7 @@ def augmented_cech_nerve : simplicial_object.augmented C :=
 
 end category_theory.arrow
 
+namespace category_theory
 namespace simplicial_object
 
 variables [∀ (n : ℕ) (f : arrow C),
@@ -87,4 +88,238 @@ def augmented_cech_nerve : arrow C ⥤ simplicial_object.augmented C :=
   { left := cech_nerve.map F,
     right := F.right } }
 
+/-- A helper function used in defining the Čech adjunction. -/
+@[simps]
+def equivalence_right_to_left (X : simplicial_object.augmented C) (F : arrow C)
+  (G : X ⟶ F.augmented_cech_nerve) : augmented.to_arrow.obj X ⟶ F :=
+{ left := G.left.app _ ≫ wide_pullback.π (λ i, F.hom) ⟨0⟩,
+  right := G.right,
+  w' := begin
+    have := G.w,
+    apply_fun (λ e, e.app (opposite.op $ simplex_category.mk 0)) at this,
+    tidy,
+  end }
+
+/-- A helper function used in defining the Čech adjunction. -/
+@[simps]
+def equivalence_left_to_right (X : simplicial_object.augmented C) (F : arrow C)
+  (G : augmented.to_arrow.obj X ⟶ F) : X ⟶ F.augmented_cech_nerve :=
+{ left :=
+  { app := λ x, limits.wide_pullback.lift (X.hom.app _ ≫ G.right)
+      (λ i, X.left.map (simplex_category.const x.unop i.down).op ≫ G.left) (by tidy),
+    naturality' := begin
+      intros x y f,
+      ext,
+      { dsimp,
+        simp only [wide_pullback.lift_π, category.assoc],
+        rw [← category.assoc, ← X.left.map_comp],
+        refl },
+      { dsimp,
+        simp only [functor.const.obj_map, nat_trans.naturality_assoc,
+          wide_pullback.lift_base, category.assoc],
+        erw category.id_comp }
+    end },
+  right := G.right }
+
+/-- A helper function used in defining the Čech adjunction. -/
+@[simps]
+def cech_nerve_equiv (X : simplicial_object.augmented C) (F : arrow C) :
+  (augmented.to_arrow.obj X ⟶ F) ≃ (X ⟶ F.augmented_cech_nerve) :=
+{ to_fun := equivalence_left_to_right _ _,
+  inv_fun := equivalence_right_to_left _ _,
+  left_inv := begin
+    intro A,
+    dsimp,
+    ext,
+    { dsimp,
+      erw wide_pullback.lift_π,
+      nth_rewrite 1 ← category.id_comp A.left,
+      congr' 1,
+      convert X.left.map_id _,
+      rw ← op_id,
+      congr' 1,
+      ext ⟨a,ha⟩,
+      change a < 1 at ha,
+      change 0 = a,
+      linarith },
+    { refl, }
+  end,
+  right_inv := begin
+    intro A,
+    dsimp,
+    ext _ ⟨j⟩,
+    { dsimp,
+      simp only [arrow.cech_nerve_map, wide_pullback.lift_π, nat_trans.naturality_assoc],
+      erw wide_pullback.lift_π,
+      refl },
+    { dsimp,
+      erw wide_pullback.lift_base,
+      have := A.w,
+      apply_fun (λ e, e.app x) at this,
+      rw nat_trans.comp_app at this,
+      erw this,
+      refl },
+    { refl }
+  end }
+
+/-- The augmented Čech nerve construction is right adjoint to the `to_arrow` functor. -/
+abbreviation cech_nerve_adjunction :
+  (augmented.to_arrow : _ ⥤ arrow C) ⊣ augmented_cech_nerve :=
+adjunction.mk_of_hom_equiv { hom_equiv := cech_nerve_equiv }
+
 end simplicial_object
+
+end category_theory
+
+namespace category_theory.arrow
+
+variables (f : arrow C)
+variables [∀ n : ℕ, has_wide_pushout f.left (λ i : ulift (fin (n+1)), f.right) (λ i, f.hom)]
+
+/-- The Čech conerve associated to an arrow. -/
+@[simps]
+def cech_conerve : cosimplicial_object C :=
+{ obj := λ n, wide_pushout f.left
+    (λ i : ulift (fin (n.len + 1)), f.right) (λ i, f.hom),
+  map := λ m n g, wide_pushout.desc (wide_pushout.head _)
+    (λ i, wide_pushout.ι (λ i, f.hom) $ ulift.up $ g.to_preorder_hom i.down)
+    begin
+      rintros ⟨⟨j⟩⟩,
+      dsimp,
+      rw [wide_pushout.arrow_ι (λ i, f.hom)],
+    end }
+
+/-- The augmented Čech conerve associated to an arrow. -/
+@[simps]
+def augmented_cech_conerve : cosimplicial_object.augmented C :=
+{ left := f.left,
+  right := f.cech_conerve,
+  hom := { app := λ i, wide_pushout.head _ } }
+
+end category_theory.arrow
+
+namespace category_theory
+namespace cosimplicial_object
+
+variables [∀ (n : ℕ) (f : arrow C),
+  has_wide_pushout f.left (λ i : ulift (fin (n+1)), f.right) (λ i, f.hom)]
+
+/-- The Čech conerve construction, as a functor from `arrow C`. -/
+@[simps]
+def cech_conerve : arrow C ⥤ cosimplicial_object C :=
+{ obj := λ f, f.cech_conerve,
+  map := λ f g F,
+  { app := λ n, wide_pushout.desc (F.left ≫ wide_pushout.head _)
+      (λ i, F.right ≫ wide_pushout.ι _ i)
+      (λ i, by { rw [←arrow.w_assoc F, wide_pushout.arrow_ι (λ i, g.hom)], }) },
+  -- tidy needs a bit of help here...
+  map_id' := by { intros i, ext, tidy },
+  map_comp' := begin
+    intros f g h F G,
+    ext,
+    all_goals {
+      dsimp,
+      simp only [category.assoc, limits.wide_pushout.head_desc_assoc,
+        limits.wide_pushout.ι_desc_assoc, limits.colimit.ι_desc],
+      simpa only [← category.assoc], },
+  end }
+
+/-- The augmented Čech conerve construction, as a functor from `arrow C`. -/
+@[simps]
+def augmented_cech_conerve : arrow C ⥤ cosimplicial_object.augmented C :=
+{ obj := λ f, f.augmented_cech_conerve,
+  map := λ f g F,
+  { left := F.left,
+    right := cech_conerve.map F, } }
+
+/-- A helper function used in defining the Čech conerve adjunction. -/
+@[simps]
+def equivalence_left_to_right (F : arrow C) (X : cosimplicial_object.augmented C)
+  (G : F.augmented_cech_conerve ⟶ X) : F ⟶ augmented.to_arrow.obj X :=
+{ left := G.left,
+  right :=
+    (wide_pushout.ι (λ i, F.hom) (_root_.ulift.up 0) ≫ G.right.app (simplex_category.mk 0) : _),
+  w' := begin
+    have := G.w,
+    apply_fun (λ e, e.app (simplex_category.mk 0)) at this,
+    dsimp at this,
+    simpa only [category_theory.functor.id_map, augmented.to_arrow_obj_hom,
+      wide_pushout.arrow_ι_assoc (λ i, F.hom)],
+  end }
+
+/-- A helper function used in defining the Čech conerve adjunction. -/
+@[simps]
+def equivalence_right_to_left (F : arrow C) (X : cosimplicial_object.augmented C)
+  (G : F ⟶ augmented.to_arrow.obj X) : F.augmented_cech_conerve ⟶ X :=
+{ left := G.left,
+  right := { app := λ x, limits.wide_pushout.desc (G.left ≫ X.hom.app _)
+      (λ i, G.right ≫ X.right.map (simplex_category.const x i.down))
+      begin
+        rintros ⟨j⟩,
+        rw ←arrow.w_assoc G,
+        dsimp,
+        have t := X.hom.naturality (x.const j),
+        dsimp at t, simp only [category.id_comp] at t,
+        rw ←t,
+      end,
+    naturality' := begin
+      intros x y f,
+      ext,
+      { dsimp,
+        simp only [wide_pushout.ι_desc_assoc, wide_pushout.ι_desc],
+        rw [category.assoc, ←X.right.map_comp],
+        refl },
+      { dsimp,
+        simp only [functor.const.obj_map, ←nat_trans.naturality,
+          wide_pushout.head_desc_assoc, wide_pushout.head_desc, category.assoc],
+        erw category.id_comp }
+    end }, }
+
+/-- A helper function used in defining the Čech conerve adjunction. -/
+@[simps]
+def cech_conerve_equiv (F : arrow C) (X : cosimplicial_object.augmented C) :
+  (F.augmented_cech_conerve ⟶ X) ≃ (F ⟶ augmented.to_arrow.obj X) :=
+{ to_fun := equivalence_left_to_right _ _,
+  inv_fun := equivalence_right_to_left _ _,
+  left_inv := begin
+    intro A,
+    dsimp,
+    ext,
+    { refl, },
+    { cases j,
+      dsimp,
+      simp only [arrow.cech_conerve_map, wide_pushout.ι_desc, category.assoc,
+        ←nat_trans.naturality, wide_pushout.ι_desc_assoc],
+      refl },
+    { dsimp,
+      erw wide_pushout.head_desc,
+      have := A.w,
+      apply_fun (λ e, e.app x) at this,
+      rw nat_trans.comp_app at this,
+      erw this,
+      refl },
+  end,
+  right_inv := begin
+    intro A,
+    dsimp,
+    ext,
+    { refl, },
+    { dsimp,
+      erw wide_pushout.ι_desc,
+      nth_rewrite 1 ← category.comp_id A.right,
+      congr' 1,
+      convert X.right.map_id _,
+      ext ⟨a,ha⟩,
+      change a < 1 at ha,
+      change 0 = a,
+      linarith },
+  end }
+
+/-- The augmented Čech conerve construction is left adjoint to the `to_arrow` functor. -/
+abbreviation cech_conerve_adjunction :
+  augmented_cech_conerve ⊣ (augmented.to_arrow : _ ⥤ arrow C) :=
+adjunction.mk_of_hom_equiv { hom_equiv := cech_conerve_equiv }
+
+end cosimplicial_object
+
+end category_theory

src/algebraic_topology/simplex_category.lean

@@ -114,6 +114,14 @@ instance small_category : small_category.{u} simplex_category :=
   id := λ m, simplex_category.hom.id _,
   comp := λ _ _ _ f g, simplex_category.hom.comp g f, }
 
+/-- The constant morphism from [0]. -/
+def const (x : simplex_category.{u}) (i : fin (x.len+1)) : [0] ⟶ x :=
+  hom.mk $ ⟨λ _, i, by tauto⟩
+
+@[simp]
+lemma const_comp (x y : simplex_category.{u}) (i : fin (x.len + 1)) (f : x ⟶ y) :
+  const x i ≫ f = const y (f.to_preorder_hom i) := rfl
+
 /--
 Make a morphism `[n] ⟶ [m]` from a monotone map between fin's.
 This is useful for constructing morphisms beetween `[n]` directly

src/algebraic_topology/simplicial_object.lean

@@ -8,7 +8,7 @@ import category_theory.category.ulift
 import category_theory.limits.functor_category
 import category_theory.opposites
 import category_theory.adjunction.limits
-import category_theory.comma
+import category_theory.arrow
 
 /-!
 # Simplicial objects in a category.
@@ -180,6 +180,23 @@ def drop : augmented C ⥤ simplicial_object C := comma.fst _ _
 @[simps]
 def point : augmented C ⥤ C := comma.snd _ _
 
+/-- The functor from augmented objects to arrows. -/
+@[simps]
+def to_arrow : augmented C ⥤ arrow C :=
+{ obj := λ X,
+  { left := (drop.obj X) _[0],
+    right := (point.obj X),
+    hom := X.hom.app _ },
+  map := λ X Y η,
+  { left := (drop.map η).app _,
+    right := (point.map η),
+    w' := begin
+      dsimp,
+      rw ← nat_trans.comp_app,
+      erw η.w,
+      refl,
+    end } }
+
 variable (C)
 
 /-- Functor composition induces a functor on augmented simplicial objects. -/
@@ -366,6 +383,23 @@ def drop : augmented C ⥤ cosimplicial_object C := comma.snd _ _
 @[simps]
 def point : augmented C ⥤ C := comma.fst _ _
 
+/-- The functor from augmented objects to arrows. -/
+@[simps]
+def to_arrow : augmented C ⥤ arrow C :=
+{ obj := λ X,
+  { left := (point.obj X),
+    right := (drop.obj X) _[0],
+    hom := X.hom.app _ },
+  map := λ X Y η,
+  { left := (point.map η),
+    right := (drop.map η).app _,
+    w' := begin
+      dsimp,
+      rw ← nat_trans.comp_app,
+      erw ← η.w,
+      refl,
+    end } }
+
 variable (C)
 
 /-- Functor composition induces a functor on augmented cosimplicial objects. -/