From d7653b8dff5cae5d672f7fe77302da9ab9e0f051 Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Tue, 6 Jul 2021 18:26:45 +0000 Subject: [PATCH] chore(category_theory/monad/algebra): lint and golf (#8160) Adds a module docstring and golfs some proofs, including removing `erw`. --- src/category_theory/monad/algebra.lean | 16 ++-- src/category_theory/monad/limits.lean | 103 +++++++++++-------------- 2 files changed, 55 insertions(+), 64 deletions(-) diff --git a/src/category_theory/monad/algebra.lean b/src/category_theory/monad/algebra.lean index 51a087aa1311c..818e23b8f5512 100644 --- a/src/category_theory/monad/algebra.lean +++ b/src/category_theory/monad/algebra.lean @@ -48,7 +48,7 @@ variables {T : monad C} /-- A morphism of Eilenberg–Moore algebras for the monad `T`. -/ @[ext] structure hom (A B : algebra T) := (f : A.A ⟶ B.A) -(h' : T.map f ≫ B.a = A.a ≫ f . obviously) +(h' : (T : C ⥤ C).map f ≫ B.a = A.a ≫ f . obviously) restate_axiom hom.h' attribute [simp, reassoc] hom.h @@ -90,7 +90,8 @@ To construct an isomorphism of algebras, it suffices to give an isomorphism of t commutes with the structure morphisms. -/ @[simps] -def iso_mk {A B : algebra T} (h : A.A ≅ B.A) (w : T.map h.hom ≫ B.a = A.a ≫ h.hom) : A ≅ B := +def iso_mk {A B : algebra T} (h : A.A ≅ B.A) (w : (T : C ⥤ C).map h.hom ≫ B.a = A.a ≫ h.hom) : + A ≅ B := { hom := { f := h.hom }, inv := { f := h.inv, @@ -143,7 +144,7 @@ Given an algebra morphism whose carrier part is an isomorphism, we get an algebr -/ lemma algebra_iso_of_iso {A B : algebra T} (f : A ⟶ B) [is_iso f.f] : is_iso f := ⟨⟨{ f := inv f.f, - h' := by { rw [is_iso.eq_comp_inv f.f, category.assoc, ← f.h], dsimp, simp } }, by tidy⟩⟩ + h' := by { rw [is_iso.eq_comp_inv f.f, category.assoc, ← f.h], simp } }, by tidy⟩⟩ instance forget_reflects_iso : reflects_isomorphisms (forget T) := { reflects := λ A B, algebra_iso_of_iso T } @@ -229,7 +230,7 @@ namespace comonad @[nolint has_inhabited_instance] structure coalgebra (G : comonad C) : Type (max u₁ v₁) := (A : C) -(a : A ⟶ G.obj A) +(a : A ⟶ (G : C ⥤ C).obj A) (counit' : a ≫ G.ε.app A = 𝟙 A . obviously) (coassoc' : a ≫ G.δ.app A = a ≫ G.map a . obviously) @@ -243,7 +244,7 @@ variables {G : comonad C} /-- A morphism of Eilenberg-Moore coalgebras for the comonad `G`. -/ @[ext, nolint has_inhabited_instance] structure hom (A B : coalgebra G) := (f : A.A ⟶ B.A) -(h' : A.a ≫ G.map f = f ≫ B.a . obviously) +(h' : A.a ≫ (G : C ⥤ C).map f = f ≫ B.a . obviously) restate_axiom hom.h' attribute [simp, reassoc] hom.h @@ -283,7 +284,8 @@ To construct an isomorphism of coalgebras, it suffices to give an isomorphism of commutes with the structure morphisms. -/ @[simps] -def iso_mk {A B : coalgebra G} (h : A.A ≅ B.A) (w : A.a ≫ G.map h.hom = h.hom ≫ B.a) : A ≅ B := +def iso_mk {A B : coalgebra G} (h : A.A ≅ B.A) (w : A.a ≫ (G : C ⥤ C).map h.hom = h.hom ≫ B.a) : + A ≅ B := { hom := { f := h.hom }, inv := { f := h.inv, @@ -304,7 +306,7 @@ Given a coalgebra morphism whose carrier part is an isomorphism, we get a coalge -/ lemma coalgebra_iso_of_iso {A B : coalgebra G} (f : A ⟶ B) [is_iso f.f] : is_iso f := ⟨⟨{ f := inv f.f, - h' := by { rw [is_iso.eq_inv_comp f.f, ←f.h_assoc], dsimp, simp } }, by tidy⟩⟩ + h' := by { rw [is_iso.eq_inv_comp f.f, ←f.h_assoc], simp } }, by tidy⟩⟩ instance forget_reflects_iso : reflects_isomorphisms (forget G) := { reflects := λ A B, coalgebra_iso_of_iso G } diff --git a/src/category_theory/monad/limits.lean b/src/category_theory/monad/limits.lean index 6e6f4f2ebfe9f..16210718bf8b7 100644 --- a/src/category_theory/monad/limits.lean +++ b/src/category_theory/monad/limits.lean @@ -7,6 +7,20 @@ import category_theory.monad.adjunction import category_theory.adjunction.limits import category_theory.limits.preserves.shapes.terminal +/-! +# Limits and colimits in the category of algebras + +This file shows that the forgetful functor `forget T : algebra T ⥤ C` for a monad `T : C ⥤ C` +creates limits and creates any colimits which `T` preserves. +This is used to show that `algebra T` has any limits which `C` has, and any colimits which `C` has +and `T` preserves. +This is generalised to the case of a monadic functor `D ⥤ C`. + +## TODO + +Dualise for the category of coalgebras and comonadic left adjoints. +-/ + namespace category_theory open category open category_theory.limits @@ -22,42 +36,32 @@ variables {J : Type v₁} [small_category J] namespace forget_creates_limits -variables (D : J ⥤ algebra T) (c : cone (D ⋙ forget T)) (t : is_limit c) +variables (D : J ⥤ algebra T) (c : cone (D ⋙ T.forget)) (t : is_limit c) /-- (Impl) The natural transformation used to define the new cone -/ -@[simps] def γ : (D ⋙ forget T ⋙ ↑T) ⟶ (D ⋙ forget T) := { app := λ j, (D.obj j).a } +@[simps] def γ : (D ⋙ T.forget ⋙ ↑T) ⟶ D ⋙ T.forget := { app := λ j, (D.obj j).a } /-- (Impl) This new cone is used to construct the algebra structure -/ -@[simps] def new_cone : cone (D ⋙ forget T) := +@[simps π_app] def new_cone : cone (D ⋙ forget T) := { X := T.obj c.X, - π := (functor.const_comp _ _ ↑T).inv ≫ whisker_right c.π T ≫ (γ D) } + π := (functor.const_comp _ _ ↑T).inv ≫ whisker_right c.π T ≫ γ D } /-- The algebra structure which will be the apex of the new limit cone for `D`. -/ @[simps] def cone_point : algebra T := { A := c.X, a := t.lift (new_cone D c), - unit' := + unit' := t.hom_ext $ λ j, begin - apply t.hom_ext, - intro j, - erw [category.assoc, t.fac (new_cone D c), id_comp], - dsimp, - erw [id_comp, ← category.assoc, ← T.η.naturality, functor.id_map, category.assoc, - (D.obj j).unit, comp_id], + rw [category.assoc, t.fac, new_cone_π_app, ←T.η.naturality_assoc, functor.id_map, + (D.obj j).unit], + dsimp, simp -- See library note [dsimp, simp] end, - assoc' := + assoc' := t.hom_ext $ λ j, begin - apply t.hom_ext, - intro j, - rw [category.assoc, category.assoc, t.fac (new_cone D c)], - dsimp, - erw id_comp, - slice_lhs 1 2 {rw ← T.μ.naturality}, - slice_lhs 2 3 {rw (D.obj j).assoc}, - slice_rhs 1 2 {rw ← (T : C ⥤ C).map_comp}, - rw t.fac (new_cone D c), - dsimp, - erw [id_comp, functor.map_comp, category.assoc] + rw [category.assoc, category.assoc, t.fac (new_cone D c), new_cone_π_app, + ←functor.map_comp_assoc, t.fac (new_cone D c), new_cone_π_app, ←T.μ.naturality_assoc, + (D.obj j).assoc, functor.map_comp, category.assoc], + refl, end } /-- (Impl) Construct the lifted cone in `algebra T` which will be limiting. -/ @@ -71,24 +75,19 @@ variables (D : J ⥤ algebra T) (c : cone (D ⋙ forget T)) (t : is_limit c) def lifted_cone_is_limit : is_limit (lifted_cone D c t) := { lift := λ s, { f := t.lift ((forget T).map_cone s), - h' := + h' := t.hom_ext $ λ j, begin - apply t.hom_ext, intro j, - slice_rhs 2 3 {rw t.fac ((forget T).map_cone s) j}, - dsimp, - slice_lhs 2 3 {rw t.fac (new_cone D c) j}, dsimp, - rw category.id_comp, - slice_lhs 1 2 {rw ← (T : C ⥤ C).map_comp}, - rw t.fac ((forget T).map_cone s) j, - exact (s.π.app j).h + rw [category.assoc, category.assoc, t.fac, new_cone_π_app, ←functor.map_comp_assoc, t.fac, + functor.map_cone_π_app], + apply (s.π.app j).h, end }, uniq' := λ s m J, begin ext1, apply t.hom_ext, intro j, - simpa [t.fac (functor.map_cone (forget T) s) j] using congr_arg algebra.hom.f (J j), + simpa [t.fac ((forget T).map_cone s) j] using congr_arg algebra.hom.f (J j), end } end forget_creates_limits @@ -152,12 +151,12 @@ we will show is the colimiting object. We use the cocone constructed by `c` and -/ @[reducible] def lambda : ((T : C ⥤ C).map_cocone c).X ⟶ c.X := -(preserves_colimit.preserves t).desc (new_cocone c) +(is_colimit_of_preserves _ t).desc (new_cocone c) /-- (Impl) The key property defining the map `λ : TL ⟶ L`. -/ lemma commuting (j : J) : -T.map (c.ι.app j) ≫ lambda c t = (D.obj j).a ≫ c.ι.app j := -is_colimit.fac (preserves_colimit.preserves t) (new_cocone c) j +(T : C ⥤ C).map (c.ι.app j) ≫ lambda c t = (D.obj j).a ≫ c.ι.app j := +(is_colimit_of_preserves _ t).fac (new_cocone c) j variables [preserves_colimit ((D ⋙ forget T) ⋙ ↑T) (T : C ⥤ C)] @@ -175,45 +174,35 @@ algebra T := begin apply t.hom_ext, intro j, - erw [comp_id, ← category.assoc, T.η.naturality, category.assoc, commuting, ← category.assoc], - erw algebra.unit, apply id_comp + rw [(show c.ι.app j ≫ T.η.app c.X ≫ _ = T.η.app (D.obj j).A ≫ _ ≫ _, + from T.η.naturality_assoc _ _), commuting, algebra.unit_assoc (D.obj j)], + dsimp, simp -- See library note [dsimp, simp] end, assoc' := begin - apply is_colimit.hom_ext (preserves_colimit.preserves (preserves_colimit.preserves t)), - intro j, - erw [← category.assoc, T.μ.naturality, ← functor.map_cocone_ι_app, category.assoc, - is_colimit.fac _ (new_cocone c) j], - rw ← category.assoc, - erw [← functor.map_comp, commuting], - dsimp, - erw [← category.assoc, algebra.assoc, category.assoc, functor.map_comp, category.assoc, - commuting], - apply_instance, apply_instance + refine (is_colimit_of_preserves _ (is_colimit_of_preserves _ t)).hom_ext (λ j, _), + rw [functor.map_cocone_ι_app, functor.map_cocone_ι_app, + (show (T : C ⥤ C).map ((T : C ⥤ C).map _) ≫ _ ≫ _ = _, from T.μ.naturality_assoc _ _), + ←functor.map_comp_assoc, commuting, functor.map_comp, category.assoc, commuting], + apply (D.obj j).assoc_assoc _, end } /-- (Impl) Construct the lifted cocone in `algebra T` which will be colimiting. -/ @[simps] def lifted_cocone : cocone D := { X := cocone_point c t, ι := { app := λ j, { f := c.ι.app j, h' := commuting _ _ _ }, - naturality' := λ A B f, by { ext1, dsimp, erw [comp_id, c.w] } } } + naturality' := λ A B f, by { ext1, dsimp, rw [comp_id], apply c.w } } } /-- (Impl) Prove that the lifted cocone is colimiting. -/ @[simps] def lifted_cocone_is_colimit : is_colimit (lifted_cocone c t) := { desc := λ s, { f := t.desc ((forget T).map_cocone s), - h' := + h' := (is_colimit_of_preserves (T : C ⥤ C) t).hom_ext $ λ j, begin dsimp, - apply is_colimit.hom_ext (preserves_colimit.preserves t), - intro j, - rw ← category.assoc, erw ← functor.map_comp, - erw t.fac', - rw ← category.assoc, erw forget_creates_colimits.commuting, - rw category.assoc, rw t.fac', + rw [←functor.map_comp_assoc, ←category.assoc, t.fac, commuting, category.assoc, t.fac], apply algebra.hom.h, - apply_instance end }, uniq' := λ s m J, by { ext1, apply t.hom_ext, intro j, simpa using congr_arg algebra.hom.f (J j) } }