From 31ba155fbe0f78c7091df64fe087418203f964a0 Mon Sep 17 00:00:00 2001 From: Adam Topaz Date: Tue, 1 Jun 2021 05:20:12 +0000 Subject: [PATCH] feat(algebraic_topology/cech_nerve): The Cech nerve is a right adjoint. (#7716) Also fixes the namespace in the file `algebraic_topology/cech_nerve.lean`. This is needed for LTE Co-authored-by: Scott Morrison --- src/algebraic_topology/cech_nerve.lean | 237 +++++++++++++++++- src/algebraic_topology/simplex_category.lean | 8 + src/algebraic_topology/simplicial_object.lean | 36 ++- 3 files changed, 279 insertions(+), 2 deletions(-) diff --git a/src/algebraic_topology/cech_nerve.lean b/src/algebraic_topology/cech_nerve.lean index f1e13ba9f41be..4a0ce5ebc27b3 100644 --- a/src/algebraic_topology/cech_nerve.lean +++ b/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 diff --git a/src/algebraic_topology/simplex_category.lean b/src/algebraic_topology/simplex_category.lean index 5281c9f780845..cd1a04b5e184e 100644 --- a/src/algebraic_topology/simplex_category.lean +++ b/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 diff --git a/src/algebraic_topology/simplicial_object.lean b/src/algebraic_topology/simplicial_object.lean index 650476a0471ae..e77f6117894c2 100644 --- a/src/algebraic_topology/simplicial_object.lean +++ b/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. -/