From 4b47e20c33b6d0bd36df0dc2d27956e8242d7c1b Mon Sep 17 00:00:00 2001 From: Jack McKoen Date: Wed, 26 Jun 2024 13:48:25 -0600 Subject: [PATCH 01/29] splitequalizer --- .../Limits/Shapes/SplitCoequalizer.lean | 14 +- .../Limits/Shapes/SplitEqualizer.lean | 163 ++++++++++++++++++ 2 files changed, 170 insertions(+), 7 deletions(-) create mode 100644 Mathlib/CategoryTheory/Limits/Shapes/SplitEqualizer.lean diff --git a/Mathlib/CategoryTheory/Limits/Shapes/SplitCoequalizer.lean b/Mathlib/CategoryTheory/Limits/Shapes/SplitCoequalizer.lean index 85f95bc1223c0b..f603d8c2d5f347 100644 --- a/Mathlib/CategoryTheory/Limits/Shapes/SplitCoequalizer.lean +++ b/Mathlib/CategoryTheory/Limits/Shapes/SplitCoequalizer.lean @@ -24,9 +24,9 @@ A pair `f g : X ⟶ Y` has a `G`-split coequalizer if `G f, G g` has a split coe These definitions and constructions are useful in particular for the monadicity theorems. -## TODO +This file has been adapted to `Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer`. Please try +to keep them in sync. -Dualise to split equalizers. -/ @@ -62,13 +62,13 @@ structure IsSplitCoequalizer {Z : C} (π : Y ⟶ Z) where /-- A map in the opposite direction to `f` and `g` -/ leftSection : Y ⟶ X /-- Composition of `π` with `f` and with `g` agree -/ - condition : f ≫ π = g ≫ π + condition : f ≫ π = g ≫ π := by aesop_cat /-- `rightSection` splits `π` -/ - rightSection_π : rightSection ≫ π = 𝟙 Z + rightSection_π : rightSection ≫ π = 𝟙 Z := by aesop_cat /-- `leftSection` splits `g` -/ - leftSection_bottom : leftSection ≫ g = 𝟙 Y + leftSection_bottom : leftSection ≫ g = 𝟙 Y := by aesop_cat /-- `leftSection` composed with `f` is `pi` composed with `rightSection` -/ - leftSection_top : leftSection ≫ f = π ≫ rightSection + leftSection_top : leftSection ≫ f = π ≫ rightSection := by aesop_cat #align category_theory.is_split_coequalizer CategoryTheory.IsSplitCoequalizer #align category_theory.is_split_coequalizer.right_section CategoryTheory.IsSplitCoequalizer.rightSection #align category_theory.is_split_coequalizer.left_section CategoryTheory.IsSplitCoequalizer.leftSection @@ -77,7 +77,7 @@ structure IsSplitCoequalizer {Z : C} (π : Y ⟶ Z) where #align category_theory.is_split_coequalizer.left_section_top CategoryTheory.IsSplitCoequalizer.leftSection_top instance {X : C} : Inhabited (IsSplitCoequalizer (𝟙 X) (𝟙 X) (𝟙 X)) where - default := ⟨𝟙 X, 𝟙 X, rfl, Category.id_comp _, Category.id_comp _, rfl⟩ + default := { rightSection := 𝟙 X, leftSection := 𝟙 X } open IsSplitCoequalizer diff --git a/Mathlib/CategoryTheory/Limits/Shapes/SplitEqualizer.lean b/Mathlib/CategoryTheory/Limits/Shapes/SplitEqualizer.lean new file mode 100644 index 00000000000000..afc13fffa168af --- /dev/null +++ b/Mathlib/CategoryTheory/Limits/Shapes/SplitEqualizer.lean @@ -0,0 +1,163 @@ +/- +Copyright (c) 2024 Jack McKoen. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jack McKoen +-/ +import Mathlib.CategoryTheory.Limits.Shapes.Equalizers + +/-! +# Split Equalizers + +We define what it means for a triple of morphisms `f g : X ⟶ Y`, `ι : W ⟶ X` to be a split +equalizer: there is a retraction `r` of `ι` and a retraction `t` of `g`, which additionally satisfy +`t ≫ f = r ≫ ι`. + +In addition, we show that every split equalizer is an equalizer +(`CategoryTheory.IsSplitEqualizer.isEqualizer`) and absolute +(`CategoryTheory.IsSplitEqualizer.map`) + +A pair `f g : X ⟶ Y` has a split equalizer if there is a `W` and `ι : W ⟶ X` making `f,g,ι` a +split equalizer. +A pair `f g : X ⟶ Y` has a `G`-split equalizer if `G f, G g` has a split equalizer. + +These definitions and constructions are useful in particular for the comonadicity theorems. + +This file was adapted from `Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer`. Please try +to keep them in sync. + +-/ + + +namespace CategoryTheory + +universe v v₂ u u₂ + +variable {C : Type u} [Category.{v} C] +variable {D : Type u₂} [Category.{v₂} D] +variable (G : C ⥤ D) +variable {X Y : C} (f g : X ⟶ Y) + +/-- A split equalizer diagram consists of morphisms + + ι f + W → X ⇉ Y + g + +satisfying `ι ≫ f = ι ≫ g` together with morphisms + + r t + W ← X ← Y + +satisfying `ι ≫ r = 𝟙 W`, `g ≫ t = 𝟙 X` and `f ≫ t = r ≫ ι`. + +The name "equalizer" is appropriate, since any split equalizer is a equalizer, see +`Category_theory.IsSplitEqualizer.isEqualizer`. +Split equalizers are also absolute, since a functor preserves all the structure above. +-/ +structure IsSplitEqualizer {W : C} (ι : W ⟶ X) where + /-- A map from `X` to the equalizer -/ + leftRetraction : X ⟶ W + /-- A map in the opposite direction to `f` and `g` -/ + rightRetraction : Y ⟶ X + /-- Composition of `ι` with `f` and with `g` agree -/ + condition : ι ≫ f = ι ≫ g := by aesop_cat + /-- `leftRetraction` splits `ι` -/ + ι_leftRetraction : ι ≫ leftRetraction = 𝟙 W := by aesop_cat + /-- `rightRetraction` splits `g` -/ + bottom_rightRetraction : g ≫ rightRetraction = 𝟙 X := by aesop_cat + /-- `f` composed with `rightRetraction` is `leftRetraction` composed with `ι` -/ + top_rightRetraction : f ≫ rightRetraction = leftRetraction ≫ ι := by aesop_cat + +instance {X : C} : Inhabited (IsSplitEqualizer (𝟙 X) (𝟙 X) (𝟙 X)) where + default := { leftRetraction := 𝟙 X, rightRetraction := 𝟙 X } + +open IsSplitEqualizer + +attribute [reassoc] condition + +attribute [reassoc (attr := simp)] ι_leftRetraction bottom_rightRetraction top_rightRetraction + +variable {f g} + +/-- Split equalizers are absolute: they are preserved by any functor. -/ +@[simps] +def IsSplitEqualizer.map {W : C} {ι : W ⟶ X} (q : IsSplitEqualizer f g ι) (F : C ⥤ D) : + IsSplitEqualizer (F.map f) (F.map g) (F.map ι) where + leftRetraction := F.map q.leftRetraction + rightRetraction := F.map q.rightRetraction + condition := by rw [← F.map_comp, q.condition, F.map_comp] + ι_leftRetraction := by rw [← F.map_comp, q.ι_leftRetraction, F.map_id] + bottom_rightRetraction := by rw [← F.map_comp, q.bottom_rightRetraction, F.map_id] + top_rightRetraction := by rw [← F.map_comp, q.top_rightRetraction, F.map_comp] + +section + +open Limits + +/-- A split equalizer clearly induces a fork. -/ +@[simps! pt] +def IsSplitEqualizer.asFork {W : C} {h : W ⟶ X} (t : IsSplitEqualizer f g h) : + Fork f g := Fork.ofι h t.condition + +@[simp] +theorem IsSplitEqualizer.asFork_ι {W : C} {h : W ⟶ X} (t : IsSplitEqualizer f g h) : + t.asFork.ι = h := rfl + +/-- +The fork induced by a split equalizer is an equalizer, justifying the name. In some cases it +is more convenient to show a given fork is an equalizer by showing it is split. +-/ +def IsSplitEqualizer.isEqualizer {W : C} {h : W ⟶ X} (t : IsSplitEqualizer f g h) : + IsLimit t.asFork := + Fork.IsLimit.mk' _ fun s => + ⟨ s.ι ≫ t.leftRetraction, + by simp [- top_rightRetraction, ← t.top_rightRetraction, s.condition_assoc], + fun hm => by simp [← hm] ⟩ + +end +variable (f g) + +/-- +The pair `f,g` is a cosplit pair if there is an `h : W ⟶ X` so that `f, g, h` forms a split +equalizer in `C`. +-/ +class HasSplitEqualizer : Prop where + /-- There is some split equalizer -/ + splittable : ∃ (W : C) (h : W ⟶ X), Nonempty (IsSplitEqualizer f g h) + +/-- +The pair `f,g` is a `G`-cosplit pair if there is an `h : W ⟶ G X` so that `G f, G g, h` forms a +split equalizer in `D`. +-/ +abbrev Functor.IsCosplitPair : Prop := + HasSplitEqualizer (G.map f) (G.map g) + +/-- Get the equalizer object from the typeclass `IsCosplitPair`. -/ +noncomputable def HasSplitEqualizer.equalizerOfCosplit [HasSplitEqualizer f g] : C := + (@splittable _ _ _ _ f g).choose + +/-- Get the equalizer morphism from the typeclass `IsCosplitPair`. -/ +noncomputable def HasSplitEqualizer.equalizerι [HasSplitEqualizer f g] : + HasSplitEqualizer.equalizerOfCosplit f g ⟶ X := + (@splittable _ _ _ _ f g).choose_spec.choose + +/-- The equalizer morphism `equalizerι` gives a split equalizer on `f,g`. -/ +noncomputable def HasSplitEqualizer.isSplitEqualizer [HasSplitEqualizer f g] : + IsSplitEqualizer f g (HasSplitEqualizer.equalizerι f g) := + Classical.choice (@splittable _ _ _ _ f g).choose_spec.choose_spec + +/-- If `f, g` is cosplit, then `G f, G g` is cosplit. -/ +instance map_is_split_pair [HasSplitEqualizer f g] : HasSplitEqualizer (G.map f) (G.map g) where + splittable := + ⟨_, _, ⟨IsSplitEqualizer.map (HasSplitEqualizer.isSplitEqualizer f g) _⟩⟩ + +namespace Limits + +/-- If a pair has a split equalizer, it has a equalizer. -/ +instance (priority := 1) hasEqualizer_of_hasSplitEqualizer [HasSplitEqualizer f g] : + HasEqualizer f g := + HasLimit.mk ⟨_, (HasSplitEqualizer.isSplitEqualizer f g).isEqualizer⟩ + +end Limits + +end CategoryTheory From 3004dd41cc37c039d7dcca172b5c5025f61b4f20 Mon Sep 17 00:00:00 2001 From: Jack McKoen Date: Wed, 26 Jun 2024 14:31:35 -0600 Subject: [PATCH 02/29] equalizer --- Mathlib/CategoryTheory/Monad/Coequalizer.lean | 3 + Mathlib/CategoryTheory/Monad/Equalizer.lean | 127 ++++++++++++++++++ 2 files changed, 130 insertions(+) create mode 100644 Mathlib/CategoryTheory/Monad/Equalizer.lean diff --git a/Mathlib/CategoryTheory/Monad/Coequalizer.lean b/Mathlib/CategoryTheory/Monad/Coequalizer.lean index 56ffadb7d9b408..c1bd9d0d1a8357 100644 --- a/Mathlib/CategoryTheory/Monad/Coequalizer.lean +++ b/Mathlib/CategoryTheory/Monad/Coequalizer.lean @@ -18,6 +18,9 @@ coequalizer is reflexive. In `C`, this cofork diagram is a split coequalizer (in particular, it is still a coequalizer). This split coequalizer is known as the Beck coequalizer (as it features heavily in Beck's monadicity theorem). + +This file has been adapted to `CategoryTheory.Monad.Equalizer`. Please try to keep them in sync. + -/ diff --git a/Mathlib/CategoryTheory/Monad/Equalizer.lean b/Mathlib/CategoryTheory/Monad/Equalizer.lean new file mode 100644 index 00000000000000..8ca625caa8c14c --- /dev/null +++ b/Mathlib/CategoryTheory/Monad/Equalizer.lean @@ -0,0 +1,127 @@ +/- +Copyright (c) 2024 Jack McKoen. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jack McKoen +-/ +import Mathlib.CategoryTheory.Limits.Shapes.Reflexive +import Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer +import Mathlib.CategoryTheory.Monad.Algebra + +/-! +# Special equalizers associated to a comonad + +Associated to a comonad `T : C ⥤ C` we have important equalizer constructions: +Any coalgebra is an equalizer (in the category of coalgebras) of cofree coalgebras. Furthermore, +this equalizer is coreflexive. +In `C`, this fork diagram is a split equalizer (in particular, it is still an equalizer). +This split equalizer is known as the Beck equalizer (as it features heavily in Beck's +comonadicity theorem). + +This file is adapted from `CategoryTheory.Monad.Coequalizer`. Please try to keep them in sync. + +-/ + + +universe v₁ u₁ + +namespace CategoryTheory + +namespace Comonad + +open Limits + +variable {C : Type u₁} +variable [Category.{v₁} C] +variable {T : Comonad C} (X : Coalgebra T) + +/-! +Show that any coalgebra is an equalizer of cofree coalgebras. +-/ + + +/-- The top map in the equalizer diagram we will construct. -/ +@[simps!] +def CofreeEqualizer.topMap : (Comonad.cofree T).obj X.A ⟶ (Comonad.cofree T).obj (T.obj X.A) := + (Comonad.cofree T).map X.a + +/-- The bottom map in the coequalizer diagram we will construct. -/ +@[simps] +def CofreeEqualizer.bottomMap : (Comonad.cofree T).obj X.A ⟶ (Comonad.cofree T).obj (T.obj X.A) where + f := T.δ.app X.A + h := T.coassoc X.A + +/-- The fork map in the equalizer diagram we will construct. -/ +@[simps] +def CofreeEqualizer.ι : X ⟶ (Comonad.cofree T).obj X.A where + f := X.a + h := X.coassoc.symm + +theorem CofreeEqualizer.condition : + CofreeEqualizer.ι X ≫ CofreeEqualizer.topMap X = + CofreeEqualizer.ι X ≫ CofreeEqualizer.bottomMap X := + Coalgebra.Hom.ext _ _ X.coassoc.symm + +instance : IsCoreflexivePair (CofreeEqualizer.topMap X) (CofreeEqualizer.bottomMap X) := by + apply IsCoreflexivePair.mk' _ _ _ + · apply (cofree T).map (T.ε.app X.A) + · ext + dsimp + rw [← Functor.map_comp, X.counit, Functor.map_id] + · ext + apply Comonad.right_counit + +/-- Construct the Beck fork in the category of coalgebras. This fork is coreflexive as well as an +equalizer. +-/ +@[simps!] +def beckCoalgebraFork : Fork (CofreeEqualizer.topMap X) (CofreeEqualizer.bottomMap X) := + Fork.ofι _ (CofreeEqualizer.condition X) + +/-- The cofork constructed is a colimit. This shows that any algebra is a (reflexive) coequalizer of +free algebras. +-/ +def beckCoalgebraEqualizer : IsLimit (beckCoalgebraFork X) := + Fork.IsLimit.mk' _ fun s => by + have h₁ : s.ι.f ≫ (T : C ⥤ C).map X.a = s.ι.f ≫ T.δ.app X.A := + congr_arg Comonad.Coalgebra.Hom.f s.condition + have h₂ : s.pt.a ≫ (T : C ⥤ C).map s.ι.f = s.ι.f ≫ T.δ.app X.A := s.ι.h + refine ⟨⟨s.ι.f ≫ T.ε.app _, ?_⟩, ?_, ?_⟩ + · dsimp + rw [Functor.map_comp, reassoc_of% h₂, Comonad.right_counit] + dsimp + rw [Category.comp_id, Category.assoc] + erw [← T.ε.naturality, reassoc_of% h₁, Comonad.left_counit] -- TODO: missing simp lemmas + simp + · ext + simpa [← T.ε.naturality_assoc, T.left_counit_assoc] using h₁ =≫ T.ε.app ((T : C ⥤ C).obj X.A) + · intro m hm + ext + dsimp only + rw [← hm] + simp [beckCoalgebraFork, X.counit] + +/-- The Beck fork is a split equalizer. -/ +def beckSplitEqualizer : IsSplitEqualizer (T.map X.a) (T.δ.app _) X.a := + ⟨T.ε.app _, T.ε.app _, X.coassoc.symm, X.counit, T.left_counit _, (T.ε.naturality _)⟩ + +/-- This is the Beck fork. It is a split equalizer, in particular a equalizer. -/ +@[simps! pt] +def beckFork : Fork (T.map X.a) (T.δ.app _) := + (beckSplitEqualizer X).asFork + +@[simp] +theorem beckFork_ι : (beckFork X).ι = X.a := + rfl + +/-- The Beck fork is a equalizer. -/ +def beckEqualizer : IsLimit (beckFork X) := + (beckSplitEqualizer X).isEqualizer + +@[simp] +theorem beckEqualizer_lift (s : Fork (T.toFunctor.map X.a) (T.δ.app X.A)) : + (beckEqualizer X).lift s = s.ι ≫ T.ε.app _ := + rfl + +end Comonad + +end CategoryTheory From f2100891cea3212398c7bc11c7f760f6f4d876e6 Mon Sep 17 00:00:00 2001 From: Jack McKoen Date: Wed, 26 Jun 2024 14:58:09 -0600 Subject: [PATCH 03/29] change splitequalizer.lean --- .../Limits/Shapes/SplitEqualizer.lean | 2 +- .../CategoryTheory/Monad/Comonadicity.lean | 427 ++++++++++++++++++ 2 files changed, 428 insertions(+), 1 deletion(-) create mode 100644 Mathlib/CategoryTheory/Monad/Comonadicity.lean diff --git a/Mathlib/CategoryTheory/Limits/Shapes/SplitEqualizer.lean b/Mathlib/CategoryTheory/Limits/Shapes/SplitEqualizer.lean index afc13fffa168af..ce77564da18774 100644 --- a/Mathlib/CategoryTheory/Limits/Shapes/SplitEqualizer.lean +++ b/Mathlib/CategoryTheory/Limits/Shapes/SplitEqualizer.lean @@ -147,7 +147,7 @@ noncomputable def HasSplitEqualizer.isSplitEqualizer [HasSplitEqualizer f g] : Classical.choice (@splittable _ _ _ _ f g).choose_spec.choose_spec /-- If `f, g` is cosplit, then `G f, G g` is cosplit. -/ -instance map_is_split_pair [HasSplitEqualizer f g] : HasSplitEqualizer (G.map f) (G.map g) where +instance map_is_cosplit_pair [HasSplitEqualizer f g] : HasSplitEqualizer (G.map f) (G.map g) where splittable := ⟨_, _, ⟨IsSplitEqualizer.map (HasSplitEqualizer.isSplitEqualizer f g) _⟩⟩ diff --git a/Mathlib/CategoryTheory/Monad/Comonadicity.lean b/Mathlib/CategoryTheory/Monad/Comonadicity.lean new file mode 100644 index 00000000000000..22d9f54008cf12 --- /dev/null +++ b/Mathlib/CategoryTheory/Monad/Comonadicity.lean @@ -0,0 +1,427 @@ +/- +Copyright (c) 2020 Bhavik Mehta. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Bhavik Mehta +-/ +import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers +import Mathlib.CategoryTheory.Limits.Shapes.Reflexive +import Mathlib.CategoryTheory.Monad.Equalizer +import Mathlib.CategoryTheory.Monad.Limits + +/-! +# Comonadicity theorems + +We prove comonadicity theorems which can establish a given functor is comonadic. In particular, we +show three versions of Beck's comonadicity theorem, and the coreflexive (crude) comonadicity theorem: + +`G` is a monadic right adjoint if it has a right adjoint, and: + +* `D` has, `G` preserves and reflects `G`-split coequalizers, see + `CategoryTheory.Monad.monadicOfHasPreservesReflectsGSplitCoequalizers` +* `G` creates `G`-split coequalizers, see + `CategoryTheory.Monad.monadicOfCreatesGSplitCoequalizers` + (The converse of this is also shown, see + `CategoryTheory.Monad.createsGSplitCoequalizersOfMonadic`) +* `D` has and `G` preserves `G`-split coequalizers, and `G` reflects isomorphisms, see + `CategoryTheory.Monad.monadicOfHasPreservesGSplitCoequalizersOfReflectsIsomorphisms` +* `D` has and `G` preserves reflexive coequalizers, and `G` reflects isomorphisms, see + `CategoryTheory.Monad.monadicOfHasPreservesReflexiveCoequalizersOfReflectsIsomorphisms` + +## Tags + +Beck, monadicity, descent + +-/ + +universe v₁ v₂ u₁ u₂ + +namespace CategoryTheory + +namespace Comonad + +open Limits + +noncomputable section + +-- Hide the implementation details in this namespace. +namespace ComonadicityInternal + +variable {C : Type u₁} {D : Type u₂} +variable [Category.{v₁} C] [Category.{v₁} D] +variable {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G) + +/-- The "main pair" for a coalgebra `(A, α)` is the pair of morphisms `(F α, ε_FA)`. It is always a +reflexive pair, and will be used to construct the left adjoint to the comparison functor and show it +is an equivalence. +-/ +instance main_pair_reflexive (A : adj.toComonad.Coalgebra) : + IsCoreflexivePair (G.map A.a) (adj.unit.app (G.obj A.A)) := by + apply IsCoreflexivePair.mk' (G.map (adj.counit.app _)) _ _ + · rw [← G.map_comp, ← G.map_id] + exact congr_arg G.map A.counit + · rw [adj.right_triangle_components] + rfl + +/-- The "main pair" for a coalgebra `(A, α)` is the pair of morphisms `(F α, ε_FA)`. It is always a +`G`-split pair, and will be used to construct the left adjoint to the comparison functor and show it +is an equivalence. +-/ +instance main_pair_F_cosplit (A : adj.toComonad.Coalgebra) : + F.IsCosplitPair (G.map A.a) + (adj.unit.app (G.obj A.A)) where + splittable := ⟨_, _, ⟨beckSplitEqualizer A⟩⟩ +set_option linter.uppercaseLean3 false in + +/-- The object function for the right adjoint to the comparison functor. -/ +def comparisonRightAdjointObj (A : adj.toComonad.Coalgebra) + [HasEqualizer (G.map A.a) (adj.unit.app _)] : C := + equalizer (G.map A.a) (adj.unit.app _) + +/-- +We have a bijection of homsets which will be used to construct the right adjoint to the comparison +functor. +-/ +@[simps!] +def comparisonRightAdjointHomEquiv (A : adj.toComonad.Coalgebra) (B : C) + [HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] : + ((comparison adj).obj B ⟶ A) ≃ (B ⟶ comparisonRightAdjointObj adj A) where + toFun := by + intro f + dsimp [comparison, comparisonRightAdjointObj] at * + dsimp [comparison] at f + refine equalizer.lift (adj.homEquiv _ _ f.f) ?_ + sorry + invFun := by + intro f + dsimp [comparison, comparisonRightAdjointObj] at f ⊢ + refine ⟨?_, ?_⟩ + dsimp + refine (adj.homEquiv _ _).symm (f ≫ (equalizer.ι _ _)) + sorry + left_inv := sorry + right_inv := sorry + +/-- Construct the adjunction to the comparison functor. +-/ +def leftAdjointComparison + [∀ A : adj.toMonad.Algebra, HasCoequalizer (F.map A.a) + (adj.counit.app (F.obj A.A))] : + adj.toMonad.Algebra ⥤ D := by + refine + Adjunction.leftAdjointOfEquiv (G := comparison adj) + (F_obj := fun A => comparisonLeftAdjointObj adj A) (fun A B => ?_) ?_ + · apply comparisonLeftAdjointHomEquiv + · intro A B B' g h + ext1 + -- Porting note: the goal was previously closed by the following, which succeeds until + -- `Category.assoc`. + -- dsimp [comparisonLeftAdjointHomEquiv] + -- rw [← adj.homEquiv_naturality_right, Category.assoc] + simp [Cofork.IsColimit.homIso] +#align category_theory.monad.monadicity_internal.left_adjoint_comparison CategoryTheory.Monad.MonadicityInternal.leftAdjointComparison + +/-- Provided we have the appropriate coequalizers, we have an adjunction to the comparison functor. +-/ +@[simps! counit] +def comparisonAdjunction + [∀ A : adj.toMonad.Algebra, HasCoequalizer (F.map A.a) + (adj.counit.app (F.obj A.A))] : + leftAdjointComparison adj ⊣ comparison adj := + Adjunction.adjunctionOfEquivLeft _ _ +#align category_theory.monad.monadicity_internal.comparison_adjunction CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction + +variable {adj} + +theorem comparisonAdjunction_unit_f_aux + [∀ A : adj.toMonad.Algebra, HasCoequalizer (F.map A.a) + (adj.counit.app (F.obj A.A))] + (A : adj.toMonad.Algebra) : + ((comparisonAdjunction adj).unit.app A).f = + adj.homEquiv A.A _ + (coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A))) := + congr_arg (adj.homEquiv _ _) (Category.comp_id _) +#align category_theory.monad.monadicity_internal.comparison_adjunction_unit_f_aux CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction_unit_f_aux + +/-- This is a cofork which is helpful for establishing monadicity: the morphism from the Beck +coequalizer to this cofork is the unit for the adjunction on the comparison functor. +-/ +@[simps! pt] +def unitCofork (A : adj.toMonad.Algebra) + [HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] : + Cofork (G.map (F.map A.a)) (G.map (adj.counit.app (F.obj A.A))) := + Cofork.ofπ (G.map (coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A)))) + (by + change _ = G.map _ ≫ _ + rw [← G.map_comp, coequalizer.condition, G.map_comp]) +#align category_theory.monad.monadicity_internal.unit_cofork CategoryTheory.Monad.MonadicityInternal.unitCofork + +@[simp] +theorem unitCofork_π (A : adj.toMonad.Algebra) + [HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] : + (unitCofork A).π = G.map (coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A))) := + rfl +#align category_theory.monad.monadicity_internal.unit_cofork_π CategoryTheory.Monad.MonadicityInternal.unitCofork_π + +theorem comparisonAdjunction_unit_f + [∀ A : adj.toMonad.Algebra, HasCoequalizer (F.map A.a) + (adj.counit.app (F.obj A.A))] + (A : adj.toMonad.Algebra) : + ((comparisonAdjunction adj).unit.app A).f = (beckCoequalizer A).desc (unitCofork A) := by + apply Limits.Cofork.IsColimit.hom_ext (beckCoequalizer A) + rw [Cofork.IsColimit.π_desc] + dsimp only [beckCofork_π, unitCofork_π] + rw [comparisonAdjunction_unit_f_aux, ← adj.homEquiv_naturality_left A.a, coequalizer.condition, + adj.homEquiv_naturality_right, adj.homEquiv_unit, Category.assoc] + apply adj.right_triangle_components_assoc +#align category_theory.monad.monadicity_internal.comparison_adjunction_unit_f CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction_unit_f + +variable (adj) + +/-- The cofork which describes the counit of the adjunction: the morphism from the coequalizer of +this pair to this morphism is the counit. +-/ +@[simps!] +def counitCofork (B : D) : + Cofork (F.map (G.map (adj.counit.app B))) + (adj.counit.app (F.obj (G.obj B))) := + Cofork.ofπ (adj.counit.app B) (adj.counit_naturality _) +#align category_theory.monad.monadicity_internal.counit_cofork CategoryTheory.Monad.MonadicityInternal.counitCofork + +variable {adj} in +/-- The unit cofork is a colimit provided `G` preserves it. -/ +def unitColimitOfPreservesCoequalizer (A : adj.toMonad.Algebra) + [HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] + [PreservesColimit (parallelPair (F.map A.a) (adj.counit.app (F.obj A.A))) G] : + IsColimit (unitCofork (G := G) A) := + isColimitOfHasCoequalizerOfPreservesColimit G _ _ +#align category_theory.monad.monadicity_internal.unit_colimit_of_preserves_coequalizer CategoryTheory.Monad.MonadicityInternal.unitColimitOfPreservesCoequalizer + +/-- The counit cofork is a colimit provided `G` reflects it. -/ +def counitCoequalizerOfReflectsCoequalizer (B : D) + [ReflectsColimit (parallelPair (F.map (G.map (adj.counit.app B))) + (adj.counit.app (F.obj (G.obj B)))) G] : + IsColimit (counitCofork (adj := adj) B) := + isColimitOfIsColimitCoforkMap G _ (beckCoequalizer ((comparison adj).obj B)) +#align category_theory.monad.monadicity_internal.counit_coequalizer_of_reflects_coequalizer CategoryTheory.Monad.MonadicityInternal.counitCoequalizerOfReflectsCoequalizer + +-- Porting note: Lean 3 didn't seem to need this +instance + [∀ A : adj.toMonad.Algebra, HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] + (B : D) : HasColimit (parallelPair + (F.map (G.map (NatTrans.app adj.counit B))) + (NatTrans.app adj.counit (F.obj (G.obj B)))) := + inferInstanceAs <| HasCoequalizer + (F.map ((comparison adj).obj B).a) + (adj.counit.app (F.obj ((comparison adj).obj B).A)) + +theorem comparisonAdjunction_counit_app + [∀ A : adj.toMonad.Algebra, HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] (B : D) : + (comparisonAdjunction adj).counit.app B = colimit.desc _ (counitCofork adj B) := by + apply coequalizer.hom_ext + change + coequalizer.π _ _ ≫ coequalizer.desc ((adj.homEquiv _ B).symm (𝟙 _)) _ = + coequalizer.π _ _ ≫ coequalizer.desc _ _ + simp +#align category_theory.monad.monadicity_internal.comparison_adjunction_counit_app CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction_counit_app + +end MonadicityInternal + +open CategoryTheory Adjunction Monad MonadicityInternal + +variable {C : Type u₁} {D : Type u₂} +variable [Category.{v₁} C] [Category.{v₁} D] +variable {G : D ⥤ C} {F : C ⥤ D} (adj : F ⊣ G) + +variable (G) in +/-- +If `G` is monadic, it creates colimits of `G`-split pairs. This is the "boring" direction of Beck's +monadicity theorem, the converse is given in `monadicOfCreatesGSplitCoequalizers`. +-/ +def createsGSplitCoequalizersOfMonadic [MonadicRightAdjoint G] ⦃A B⦄ (f g : A ⟶ B) + [G.IsSplitPair f g] : CreatesColimit (parallelPair f g) G := by + apply (config := {allowSynthFailures := true}) monadicCreatesColimitOfPreservesColimit + -- Porting note: oddly (config := {allowSynthFailures := true}) had no effect here and below + · apply @preservesColimitOfIsoDiagram _ _ _ _ _ _ _ _ _ (diagramIsoParallelPair.{v₁} _).symm ?_ + dsimp + infer_instance + · apply @preservesColimitOfIsoDiagram _ _ _ _ _ _ _ _ _ (diagramIsoParallelPair.{v₁} _).symm ?_ + dsimp + infer_instance +set_option linter.uppercaseLean3 false in +#align category_theory.monad.creates_G_split_coequalizers_of_monadic CategoryTheory.Monad.createsGSplitCoequalizersOfMonadic + +section BeckMonadicity + +-- Porting note: added these to replace parametric instances lean4#2311 +-- When this is fixed the proofs below that struggle with instances should be reviewed. +-- [∀ ⦃A B⦄ (f g : A ⟶ B) [G.IsSplitPair f g], HasCoequalizer f g] +class HasCoequalizerOfIsSplitPair (G : D ⥤ C) : Prop where + out : ∀ {A B} (f g : A ⟶ B) [G.IsSplitPair f g], HasCoequalizer f g + +-- Porting note: cannot find synth order +-- instance {A B} (f g : A ⟶ B) [G.IsSplitPair f g] [HasCoequalizerOfIsSplitPair G] : +-- HasCoequalizer f g := HasCoequalizerOfIsSplitPair.out f g + +instance [HasCoequalizerOfIsSplitPair G] : ∀ (A : Algebra adj.toMonad), + HasCoequalizer (F.map A.a) + (adj.counit.app (F.obj A.A)) := + fun _ => HasCoequalizerOfIsSplitPair.out G _ _ + +-- Porting note: added these to replace parametric instances lean4#2311 +-- [∀ ⦃A B⦄ (f g : A ⟶ B) [G.IsSplitPair f g], PreservesColimit (parallelPair f g) G] +class PreservesColimitOfIsSplitPair (G : D ⥤ C) where + out : ∀ {A B} (f g : A ⟶ B) [G.IsSplitPair f g], PreservesColimit (parallelPair f g) G + +instance {A B} (f g : A ⟶ B) [G.IsSplitPair f g] [PreservesColimitOfIsSplitPair G] : + PreservesColimit (parallelPair f g) G := PreservesColimitOfIsSplitPair.out f g + +instance [PreservesColimitOfIsSplitPair G] : ∀ (A : Algebra adj.toMonad), + PreservesColimit (parallelPair (F.map A.a) + (NatTrans.app adj.counit (F.obj A.A))) G := + fun _ => PreservesColimitOfIsSplitPair.out _ _ + +-- Porting note: added these to replace parametric instances lean4#2311 +-- [∀ ⦃A B⦄ (f g : A ⟶ B) [G.IsSplitPair f g], ReflectsColimit (parallelPair f g) G] : +class ReflectsColimitOfIsSplitPair (G : D ⥤ C) where + out : ∀ {A B} (f g : A ⟶ B) [G.IsSplitPair f g], ReflectsColimit (parallelPair f g) G + +instance {A B} (f g : A ⟶ B) [G.IsSplitPair f g] [ReflectsColimitOfIsSplitPair G] : + ReflectsColimit (parallelPair f g) G := ReflectsColimitOfIsSplitPair.out f g + +instance [ReflectsColimitOfIsSplitPair G] : ∀ (A : Algebra adj.toMonad), + ReflectsColimit (parallelPair (F.map A.a) + (NatTrans.app adj.counit (F.obj A.A))) G := + fun _ => ReflectsColimitOfIsSplitPair.out _ _ + +/-- To show `G` is a monadic right adjoint, we can show it preserves and reflects `G`-split +coequalizers, and `C` has them. +-/ +def monadicOfHasPreservesReflectsGSplitCoequalizers [HasCoequalizerOfIsSplitPair G] + [PreservesColimitOfIsSplitPair G] [ReflectsColimitOfIsSplitPair G] : + MonadicRightAdjoint G where + adj := adj + eqv := by + have : ∀ (X : Algebra adj.toMonad), IsIso ((comparisonAdjunction adj).unit.app X) := by + intro X + apply @isIso_of_reflects_iso _ _ _ _ _ _ _ (Monad.forget adj.toMonad) ?_ _ + · change IsIso ((comparisonAdjunction adj).unit.app X).f + rw [comparisonAdjunction_unit_f] + change + IsIso + (IsColimit.coconePointUniqueUpToIso (beckCoequalizer X) + (unitColimitOfPreservesCoequalizer X)).hom + exact (IsColimit.coconePointUniqueUpToIso _ _).isIso_hom + have : ∀ (Y : D), IsIso ((comparisonAdjunction adj).counit.app Y) := by + intro Y + rw [comparisonAdjunction_counit_app] + -- Porting note: passing instances through + change IsIso (IsColimit.coconePointUniqueUpToIso _ ?_).hom + infer_instance + -- Porting note: passing instances through + apply @counitCoequalizerOfReflectsCoequalizer _ _ _ _ _ _ _ _ ?_ + letI _ : + G.IsSplitPair (F.map (G.map (adj.counit.app Y))) + (adj.counit.app (F.obj (G.obj Y))) := + MonadicityInternal.main_pair_G_split _ ((comparison adj).obj Y) + infer_instance + exact (comparisonAdjunction adj).toEquivalence.isEquivalence_inverse +set_option linter.uppercaseLean3 false in +#align category_theory.monad.monadic_of_has_preserves_reflects_G_split_coequalizers CategoryTheory.Monad.monadicOfHasPreservesReflectsGSplitCoequalizers + +-- Porting note: added these to replace parametric instances lean4#2311 +-- [∀ ⦃A B⦄ (f g : A ⟶ B) [G.IsSplitPair f g], CreatesColimit (parallelPair f g) G] : +class CreatesColimitOfIsSplitPair (G : D ⥤ C) where + out : ∀ {A B} (f g : A ⟶ B) [G.IsSplitPair f g], CreatesColimit (parallelPair f g) G + +instance {A B} (f g : A ⟶ B) [G.IsSplitPair f g] [CreatesColimitOfIsSplitPair G] : + CreatesColimit (parallelPair f g) G := CreatesColimitOfIsSplitPair.out f g + +instance [CreatesColimitOfIsSplitPair G] : ∀ (A : Algebra adj.toMonad), + CreatesColimit (parallelPair (F.map A.a) + (NatTrans.app adj.counit (F.obj A.A))) G := + fun _ => CreatesColimitOfIsSplitPair.out _ _ + +/-- +Beck's monadicity theorem. If `G` has a right adjoint and creates coequalizers of `G`-split pairs, +then it is monadic. +This is the converse of `createsGSplitOfMonadic`. +-/ +def monadicOfCreatesGSplitCoequalizers [CreatesColimitOfIsSplitPair G] : + MonadicRightAdjoint G := by + let I {A B} (f g : A ⟶ B) [G.IsSplitPair f g] : HasColimit (parallelPair f g ⋙ G) := by + apply @hasColimitOfIso _ _ _ _ _ _ ?_ (diagramIsoParallelPair.{v₁} _) + exact inferInstanceAs <| HasCoequalizer (G.map f) (G.map g) + have : HasCoequalizerOfIsSplitPair G := ⟨fun _ _ => hasColimit_of_created (parallelPair _ _) G⟩ + have : PreservesColimitOfIsSplitPair G := ⟨by intros; infer_instance⟩ + have : ReflectsColimitOfIsSplitPair G := ⟨by intros; infer_instance⟩ + exact monadicOfHasPreservesReflectsGSplitCoequalizers adj +set_option linter.uppercaseLean3 false in +#align category_theory.monad.monadic_of_creates_G_split_coequalizers CategoryTheory.Monad.monadicOfCreatesGSplitCoequalizers + +/-- An alternate version of Beck's monadicity theorem. If `G` reflects isomorphisms, preserves +coequalizers of `G`-split pairs and `C` has coequalizers of `G`-split pairs, then it is monadic. +-/ +def monadicOfHasPreservesGSplitCoequalizersOfReflectsIsomorphisms [G.ReflectsIsomorphisms] + [HasCoequalizerOfIsSplitPair G] [PreservesColimitOfIsSplitPair G] : + MonadicRightAdjoint G := by + have : ReflectsColimitOfIsSplitPair G := ⟨fun f g _ => by + have := HasCoequalizerOfIsSplitPair.out G f g + apply reflectsColimitOfReflectsIsomorphisms⟩ + apply monadicOfHasPreservesReflectsGSplitCoequalizers adj +set_option linter.uppercaseLean3 false in +#align category_theory.monad.monadic_of_has_preserves_G_split_coequalizers_of_reflects_isomorphisms CategoryTheory.Monad.monadicOfHasPreservesGSplitCoequalizersOfReflectsIsomorphisms + +end BeckMonadicity + +section ReflexiveMonadicity + +variable [HasReflexiveCoequalizers D] [G.ReflectsIsomorphisms] + +-- Porting note: added these to replace parametric instances lean4#2311 +-- [∀ ⦃A B⦄ (f g : A ⟶ B) [G.IsReflexivePair f g], PreservesColimit (parallelPair f g) G] : +class PreservesColimitOfIsReflexivePair (G : C ⥤ D) where + out : ∀ ⦃A B⦄ (f g : A ⟶ B) [IsReflexivePair f g], PreservesColimit (parallelPair f g) G + +instance {A B} (f g : A ⟶ B) [IsReflexivePair f g] [PreservesColimitOfIsReflexivePair G] : + PreservesColimit (parallelPair f g) G := PreservesColimitOfIsReflexivePair.out f g + +instance [PreservesColimitOfIsReflexivePair G] : ∀ X : Algebra adj.toMonad, + PreservesColimit (parallelPair (F.map X.a) + (NatTrans.app adj.counit (F.obj X.A))) G := + fun _ => PreservesColimitOfIsReflexivePair.out _ _ + +variable [PreservesColimitOfIsReflexivePair G] + +/-- Reflexive (crude) monadicity theorem. If `G` has a right adjoint, `D` has and `G` preserves +reflexive coequalizers and `G` reflects isomorphisms, then `G` is monadic. +-/ +def monadicOfHasPreservesReflexiveCoequalizersOfReflectsIsomorphisms : MonadicRightAdjoint G where + adj := adj + eqv := by + have : ∀ (X : Algebra adj.toMonad), IsIso ((comparisonAdjunction adj).unit.app X) := by + intro X + apply + @isIso_of_reflects_iso _ _ _ _ _ _ _ (Monad.forget adj.toMonad) ?_ _ + · change IsIso ((comparisonAdjunction adj).unit.app X).f + rw [comparisonAdjunction_unit_f] + exact (IsColimit.coconePointUniqueUpToIso (beckCoequalizer X) + (unitColimitOfPreservesCoequalizer X)).isIso_hom + have : ∀ (Y : D), IsIso ((comparisonAdjunction adj).counit.app Y) := by + intro Y + rw [comparisonAdjunction_counit_app] + -- Porting note: passing instances through + change IsIso (IsColimit.coconePointUniqueUpToIso _ ?_).hom + infer_instance + -- Porting note: passing instances through + apply @counitCoequalizerOfReflectsCoequalizer _ _ _ _ _ _ _ _ ?_ + apply reflectsColimitOfReflectsIsomorphisms + exact (comparisonAdjunction adj).toEquivalence.isEquivalence_inverse +#align category_theory.monad.monadic_of_has_preserves_reflexive_coequalizers_of_reflects_isomorphisms CategoryTheory.Monad.monadicOfHasPreservesReflexiveCoequalizersOfReflectsIsomorphisms + +end ReflexiveMonadicity + +end + +end Monad + +end CategoryTheory From 428178e0d9fe72936f16a8e93f1afe5efaca2f08 Mon Sep 17 00:00:00 2001 From: Jack McKoen Date: Wed, 26 Jun 2024 23:32:46 -0600 Subject: [PATCH 04/29] dualise limits and fill in comonadicity --- .../CategoryTheory/Monad/Comonadicity.lean | 457 +++++++++--------- Mathlib/CategoryTheory/Monad/Limits.lean | 284 +++++++++++ 2 files changed, 502 insertions(+), 239 deletions(-) diff --git a/Mathlib/CategoryTheory/Monad/Comonadicity.lean b/Mathlib/CategoryTheory/Monad/Comonadicity.lean index 22d9f54008cf12..24a55621609b23 100644 --- a/Mathlib/CategoryTheory/Monad/Comonadicity.lean +++ b/Mathlib/CategoryTheory/Monad/Comonadicity.lean @@ -29,7 +29,7 @@ show three versions of Beck's comonadicity theorem, and the coreflexive (crude) ## Tags -Beck, monadicity, descent +Beck, comonadicity, descent -/ @@ -54,7 +54,7 @@ variable {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G) reflexive pair, and will be used to construct the left adjoint to the comparison functor and show it is an equivalence. -/ -instance main_pair_reflexive (A : adj.toComonad.Coalgebra) : +instance main_pair_coreflexive (A : adj.toComonad.Coalgebra) : IsCoreflexivePair (G.map A.a) (adj.unit.app (G.obj A.A)) := by apply IsCoreflexivePair.mk' (G.map (adj.counit.app _)) _ _ · rw [← G.map_comp, ← G.map_id] @@ -70,7 +70,6 @@ instance main_pair_F_cosplit (A : adj.toComonad.Coalgebra) : F.IsCosplitPair (G.map A.a) (adj.unit.app (G.obj A.A)) where splittable := ⟨_, _, ⟨beckSplitEqualizer A⟩⟩ -set_option linter.uppercaseLean3 false in /-- The object function for the right adjoint to the comparison functor. -/ def comparisonRightAdjointObj (A : adj.toComonad.Coalgebra) @@ -85,343 +84,323 @@ functor. def comparisonRightAdjointHomEquiv (A : adj.toComonad.Coalgebra) (B : C) [HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] : ((comparison adj).obj B ⟶ A) ≃ (B ⟶ comparisonRightAdjointObj adj A) where - toFun := by - intro f - dsimp [comparison, comparisonRightAdjointObj] at * - dsimp [comparison] at f + toFun f := by refine equalizer.lift (adj.homEquiv _ _ f.f) ?_ + congr sorry - invFun := by - intro f - dsimp [comparison, comparisonRightAdjointObj] at f ⊢ - refine ⟨?_, ?_⟩ - dsimp - refine (adj.homEquiv _ _).symm (f ≫ (equalizer.ι _ _)) + invFun f := by + refine ⟨(adj.homEquiv _ _).symm (f ≫ (equalizer.ι _ _)), ?_⟩ + simp sorry - left_inv := sorry - right_inv := sorry + left_inv f := by aesop + right_inv f := by apply equalizer.hom_ext; simp /-- Construct the adjunction to the comparison functor. -/ -def leftAdjointComparison - [∀ A : adj.toMonad.Algebra, HasCoequalizer (F.map A.a) - (adj.counit.app (F.obj A.A))] : - adj.toMonad.Algebra ⥤ D := by +def rightAdjointComparison + [∀ A : adj.toComonad.Coalgebra, HasEqualizer (G.map A.a) + (adj.unit.app (G.obj A.A))] : + adj.toComonad.Coalgebra ⥤ C := by refine - Adjunction.leftAdjointOfEquiv (G := comparison adj) - (F_obj := fun A => comparisonLeftAdjointObj adj A) (fun A B => ?_) ?_ - · apply comparisonLeftAdjointHomEquiv + Adjunction.rightAdjointOfEquiv (F := comparison adj) + (G_obj := fun A => comparisonRightAdjointObj adj A) (fun A B => ?_) ?_ + · apply comparisonRightAdjointHomEquiv · intro A B B' g h - ext1 - -- Porting note: the goal was previously closed by the following, which succeeds until - -- `Category.assoc`. - -- dsimp [comparisonLeftAdjointHomEquiv] - -- rw [← adj.homEquiv_naturality_right, Category.assoc] - simp [Cofork.IsColimit.homIso] -#align category_theory.monad.monadicity_internal.left_adjoint_comparison CategoryTheory.Monad.MonadicityInternal.leftAdjointComparison - -/-- Provided we have the appropriate coequalizers, we have an adjunction to the comparison functor. + apply equalizer.hom_ext + simp + +/-- Provided we have the appropriate equalizers, we have an adjunction to the comparison functor. -/ @[simps! counit] def comparisonAdjunction - [∀ A : adj.toMonad.Algebra, HasCoequalizer (F.map A.a) - (adj.counit.app (F.obj A.A))] : - leftAdjointComparison adj ⊣ comparison adj := - Adjunction.adjunctionOfEquivLeft _ _ -#align category_theory.monad.monadicity_internal.comparison_adjunction CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction + [∀ A : adj.toComonad.Coalgebra, HasEqualizer (G.map A.a) + (adj.unit.app (G.obj A.A))] : + comparison adj ⊣ rightAdjointComparison adj := + Adjunction.adjunctionOfEquivRight _ _ variable {adj} -theorem comparisonAdjunction_unit_f_aux - [∀ A : adj.toMonad.Algebra, HasCoequalizer (F.map A.a) - (adj.counit.app (F.obj A.A))] - (A : adj.toMonad.Algebra) : - ((comparisonAdjunction adj).unit.app A).f = - adj.homEquiv A.A _ - (coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A))) := - congr_arg (adj.homEquiv _ _) (Category.comp_id _) -#align category_theory.monad.monadicity_internal.comparison_adjunction_unit_f_aux CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction_unit_f_aux - -/-- This is a cofork which is helpful for establishing monadicity: the morphism from the Beck -coequalizer to this cofork is the unit for the adjunction on the comparison functor. +theorem comparisonAdjunction_counit_f_aux + [∀ A : adj.toComonad.Coalgebra, HasEqualizer (G.map A.a) + (adj.unit.app (G.obj A.A))] + (A : adj.toComonad.Coalgebra) : + ((comparisonAdjunction adj).counit.app A).f = + (adj.homEquiv _ A.A).symm (equalizer.ι (G.map A.a) (adj.unit.app (G.obj A.A))) := + congr_arg (adj.homEquiv _ _).symm (Category.id_comp _) + +/-- This is a fork which is helpful for establishing comonadicity: the morphism from the Beck +equalizer to this fork is the counit for the adjunction on the comparison functor. -/ @[simps! pt] -def unitCofork (A : adj.toMonad.Algebra) - [HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] : - Cofork (G.map (F.map A.a)) (G.map (adj.counit.app (F.obj A.A))) := - Cofork.ofπ (G.map (coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A)))) +def counitFork (A : adj.toComonad.Coalgebra) + [HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] : + Fork (F.map (G.map A.a)) (F.map (adj.unit.app (G.obj A.A))) := + Fork.ofι (F.map (equalizer.ι (G.map A.a) (adj.unit.app (G.obj A.A)))) (by - change _ = G.map _ ≫ _ - rw [← G.map_comp, coequalizer.condition, G.map_comp]) -#align category_theory.monad.monadicity_internal.unit_cofork CategoryTheory.Monad.MonadicityInternal.unitCofork + change _ = F.map _ ≫ _ + rw [← F.map_comp, equalizer.condition, F.map_comp]) @[simp] -theorem unitCofork_π (A : adj.toMonad.Algebra) - [HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] : - (unitCofork A).π = G.map (coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A))) := +theorem unitFork_ι (A : adj.toComonad.Coalgebra) + [HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] : + (counitFork A).ι = F.map (equalizer.ι (G.map A.a) (adj.unit.app (G.obj A.A))) := rfl -#align category_theory.monad.monadicity_internal.unit_cofork_π CategoryTheory.Monad.MonadicityInternal.unitCofork_π - -theorem comparisonAdjunction_unit_f - [∀ A : adj.toMonad.Algebra, HasCoequalizer (F.map A.a) - (adj.counit.app (F.obj A.A))] - (A : adj.toMonad.Algebra) : - ((comparisonAdjunction adj).unit.app A).f = (beckCoequalizer A).desc (unitCofork A) := by - apply Limits.Cofork.IsColimit.hom_ext (beckCoequalizer A) - rw [Cofork.IsColimit.π_desc] - dsimp only [beckCofork_π, unitCofork_π] - rw [comparisonAdjunction_unit_f_aux, ← adj.homEquiv_naturality_left A.a, coequalizer.condition, - adj.homEquiv_naturality_right, adj.homEquiv_unit, Category.assoc] - apply adj.right_triangle_components_assoc -#align category_theory.monad.monadicity_internal.comparison_adjunction_unit_f CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction_unit_f + +theorem comparisonAdjunction_counit_f + [∀ A : adj.toComonad.Coalgebra, HasEqualizer (G.map A.a) + (adj.unit.app (G.obj A.A))] + (A : adj.toComonad.Coalgebra) : + ((comparisonAdjunction adj).counit.app A).f = (beckEqualizer A).lift (counitFork A) := by + apply Limits.Fork.IsLimit.hom_ext (beckEqualizer A) + rw [Fork.IsLimit.lift_ι] + dsimp only [beckFork_ι, unitFork_ι] + rw [comparisonAdjunction_counit_f_aux] + simp + suffices h : adj.counit.app A.A ≫ A.a = 𝟙 _ by { + rw [h] + simp only [Functor.comp_obj, Category.comp_id] + } + sorry variable (adj) -/-- The cofork which describes the counit of the adjunction: the morphism from the coequalizer of -this pair to this morphism is the counit. +/-- The fork which describes the unit of the adjunction: the morphism from the equalizer of +this pair to this morphism is the unit. -/ @[simps!] -def counitCofork (B : D) : - Cofork (F.map (G.map (adj.counit.app B))) - (adj.counit.app (F.obj (G.obj B))) := - Cofork.ofπ (adj.counit.app B) (adj.counit_naturality _) -#align category_theory.monad.monadicity_internal.counit_cofork CategoryTheory.Monad.MonadicityInternal.counitCofork +def unitFork (B : C) : + Fork (G.map (F.map (adj.unit.app B))) + (adj.unit.app (G.obj (F.obj B))) := + Fork.ofι (adj.unit.app B) (adj.unit_naturality _) variable {adj} in -/-- The unit cofork is a colimit provided `G` preserves it. -/ -def unitColimitOfPreservesCoequalizer (A : adj.toMonad.Algebra) - [HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] - [PreservesColimit (parallelPair (F.map A.a) (adj.counit.app (F.obj A.A))) G] : - IsColimit (unitCofork (G := G) A) := - isColimitOfHasCoequalizerOfPreservesColimit G _ _ -#align category_theory.monad.monadicity_internal.unit_colimit_of_preserves_coequalizer CategoryTheory.Monad.MonadicityInternal.unitColimitOfPreservesCoequalizer - -/-- The counit cofork is a colimit provided `G` reflects it. -/ -def counitCoequalizerOfReflectsCoequalizer (B : D) - [ReflectsColimit (parallelPair (F.map (G.map (adj.counit.app B))) - (adj.counit.app (F.obj (G.obj B)))) G] : - IsColimit (counitCofork (adj := adj) B) := - isColimitOfIsColimitCoforkMap G _ (beckCoequalizer ((comparison adj).obj B)) -#align category_theory.monad.monadicity_internal.counit_coequalizer_of_reflects_coequalizer CategoryTheory.Monad.MonadicityInternal.counitCoequalizerOfReflectsCoequalizer +/-- The counit fork is a limit provided `F` preserves it. -/ +def counitLimitOfPreservesEqualizer (A : adj.toComonad.Coalgebra) + [HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] + [PreservesLimit (parallelPair (G.map A.a) (adj.unit.app (G.obj A.A))) F] : + IsLimit (counitFork (G := G) A) := + isLimitOfHasEqualizerOfPreservesLimit F _ _ + +/-- The unit fork is a colimit provided `G` reflects it. -/ +def unitEqualizerOfCoreflectsEqualizer (B : C) + [ReflectsLimit (parallelPair (G.map (F.map (adj.unit.app B))) + (adj.unit.app (G.obj (F.obj B)))) F] : + IsLimit (unitFork (adj := adj) B) := + isLimitOfIsLimitForkMap F _ (beckEqualizer ((comparison adj).obj B)) -- Porting note: Lean 3 didn't seem to need this instance - [∀ A : adj.toMonad.Algebra, HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] - (B : D) : HasColimit (parallelPair - (F.map (G.map (NatTrans.app adj.counit B))) - (NatTrans.app adj.counit (F.obj (G.obj B)))) := - inferInstanceAs <| HasCoequalizer - (F.map ((comparison adj).obj B).a) - (adj.counit.app (F.obj ((comparison adj).obj B).A)) - -theorem comparisonAdjunction_counit_app - [∀ A : adj.toMonad.Algebra, HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] (B : D) : - (comparisonAdjunction adj).counit.app B = colimit.desc _ (counitCofork adj B) := by - apply coequalizer.hom_ext + [∀ A : adj.toComonad.Coalgebra, HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] + (B : C) : HasLimit (parallelPair + (G.map (F.map (NatTrans.app adj.unit B))) + (NatTrans.app adj.unit (G.obj (F.obj B)))) := + inferInstanceAs <| HasEqualizer + (G.map ((comparison adj).obj B).a) + (adj.unit.app (G.obj ((comparison adj).obj B).A)) + +theorem comparisonAdjunction_unit_app + [∀ A : adj.toComonad.Coalgebra, HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] (B : C) : + (comparisonAdjunction adj).unit.app B = limit.lift _ (unitFork adj B) := by + apply equalizer.hom_ext change - coequalizer.π _ _ ≫ coequalizer.desc ((adj.homEquiv _ B).symm (𝟙 _)) _ = - coequalizer.π _ _ ≫ coequalizer.desc _ _ + equalizer.lift ((adj.homEquiv B _) (𝟙 _)) _ ≫ equalizer.ι _ _ = + equalizer.lift _ _ ≫ equalizer.ι _ _ simp -#align category_theory.monad.monadicity_internal.comparison_adjunction_counit_app CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction_counit_app -end MonadicityInternal +end ComonadicityInternal -open CategoryTheory Adjunction Monad MonadicityInternal +open CategoryTheory Adjunction Comonad ComonadicityInternal variable {C : Type u₁} {D : Type u₂} variable [Category.{v₁} C] [Category.{v₁} D] variable {G : D ⥤ C} {F : C ⥤ D} (adj : F ⊣ G) +-- TODO: dualise `CategoryTheory.Monad.Limits` variable (G) in /-- -If `G` is monadic, it creates colimits of `G`-split pairs. This is the "boring" direction of Beck's -monadicity theorem, the converse is given in `monadicOfCreatesGSplitCoequalizers`. +If `F` is comonadic, it creates limits of `F`-cosplit pairs. This is the "boring" direction of Beck's +comonadicity theorem, the converse is given in `comonadicOfCreatesGSplitEqualizers`. -/ -def createsGSplitCoequalizersOfMonadic [MonadicRightAdjoint G] ⦃A B⦄ (f g : A ⟶ B) - [G.IsSplitPair f g] : CreatesColimit (parallelPair f g) G := by - apply (config := {allowSynthFailures := true}) monadicCreatesColimitOfPreservesColimit +def createsGSplitEqualizersOfComonadic [ComonadicLeftAdjoint F] ⦃A B⦄ (f g : A ⟶ B) + [F.IsCosplitPair f g] : CreatesLimit (parallelPair f g) F := by + apply (config := {allowSynthFailures := true}) comonadicCreatesLimitOfPreservesLimit -- Porting note: oddly (config := {allowSynthFailures := true}) had no effect here and below - · apply @preservesColimitOfIsoDiagram _ _ _ _ _ _ _ _ _ (diagramIsoParallelPair.{v₁} _).symm ?_ + · apply @preservesLimitOfIsoDiagram _ _ _ _ _ _ _ _ _ (diagramIsoParallelPair.{v₁} _).symm ?_ dsimp - infer_instance - · apply @preservesColimitOfIsoDiagram _ _ _ _ _ _ _ _ _ (diagramIsoParallelPair.{v₁} _).symm ?_ + sorry --infer_instance + · apply @preservesLimitOfIsoDiagram _ _ _ _ _ _ _ _ _ (diagramIsoParallelPair.{v₁} _).symm ?_ dsimp - infer_instance -set_option linter.uppercaseLean3 false in -#align category_theory.monad.creates_G_split_coequalizers_of_monadic CategoryTheory.Monad.createsGSplitCoequalizersOfMonadic + sorry --infer_instance -section BeckMonadicity +section BeckComonadicity --- Porting note: added these to replace parametric instances lean4#2311 --- When this is fixed the proofs below that struggle with instances should be reviewed. --- [∀ ⦃A B⦄ (f g : A ⟶ B) [G.IsSplitPair f g], HasCoequalizer f g] -class HasCoequalizerOfIsSplitPair (G : D ⥤ C) : Prop where - out : ∀ {A B} (f g : A ⟶ B) [G.IsSplitPair f g], HasCoequalizer f g +-- [∀ ⦃A B⦄ (f g : A ⟶ B) [G.IsCosplitPair f g], HasEqualizer f g] +class HasEqualizerOfIsCosplitPair (G : D ⥤ C) : Prop where + out : ∀ {A B} (f g : A ⟶ B) [G.IsCosplitPair f g], HasEqualizer f g -- Porting note: cannot find synth order -- instance {A B} (f g : A ⟶ B) [G.IsSplitPair f g] [HasCoequalizerOfIsSplitPair G] : -- HasCoequalizer f g := HasCoequalizerOfIsSplitPair.out f g -instance [HasCoequalizerOfIsSplitPair G] : ∀ (A : Algebra adj.toMonad), - HasCoequalizer (F.map A.a) - (adj.counit.app (F.obj A.A)) := - fun _ => HasCoequalizerOfIsSplitPair.out G _ _ +instance [HasEqualizerOfIsCosplitPair F] : ∀ (A : Coalgebra adj.toComonad), + HasEqualizer (G.map A.a) + (adj.unit.app (G.obj A.A)) := + fun _ => HasEqualizerOfIsCosplitPair.out F _ _ -- Porting note: added these to replace parametric instances lean4#2311 --- [∀ ⦃A B⦄ (f g : A ⟶ B) [G.IsSplitPair f g], PreservesColimit (parallelPair f g) G] -class PreservesColimitOfIsSplitPair (G : D ⥤ C) where - out : ∀ {A B} (f g : A ⟶ B) [G.IsSplitPair f g], PreservesColimit (parallelPair f g) G +-- [∀ ⦃A B⦄ (f g : A ⟶ B) [G.IsCosplitPair f g], PreservesLimit (parallelPair f g) G] +class PreservesLimitOfIsCosplitPair (G : D ⥤ C) where + out : ∀ {A B} (f g : A ⟶ B) [G.IsCosplitPair f g], PreservesLimit (parallelPair f g) G -instance {A B} (f g : A ⟶ B) [G.IsSplitPair f g] [PreservesColimitOfIsSplitPair G] : - PreservesColimit (parallelPair f g) G := PreservesColimitOfIsSplitPair.out f g +instance {A B} (f g : A ⟶ B) [G.IsCosplitPair f g] [PreservesLimitOfIsCosplitPair G] : + PreservesLimit (parallelPair f g) G := PreservesLimitOfIsCosplitPair.out f g -instance [PreservesColimitOfIsSplitPair G] : ∀ (A : Algebra adj.toMonad), - PreservesColimit (parallelPair (F.map A.a) - (NatTrans.app adj.counit (F.obj A.A))) G := - fun _ => PreservesColimitOfIsSplitPair.out _ _ +instance [PreservesLimitOfIsCosplitPair F] : ∀ (A : Coalgebra adj.toComonad), + PreservesLimit (parallelPair (G.map A.a) + (NatTrans.app adj.unit (G.obj A.A))) F := + fun _ => PreservesLimitOfIsCosplitPair.out _ _ -- Porting note: added these to replace parametric instances lean4#2311 --- [∀ ⦃A B⦄ (f g : A ⟶ B) [G.IsSplitPair f g], ReflectsColimit (parallelPair f g) G] : -class ReflectsColimitOfIsSplitPair (G : D ⥤ C) where - out : ∀ {A B} (f g : A ⟶ B) [G.IsSplitPair f g], ReflectsColimit (parallelPair f g) G +-- [∀ ⦃A B⦄ (f g : A ⟶ B) [G.IsCosplitPair f g], ReflectsLimit (parallelPair f g) G] : +class ReflectsLimitOfIsCosplitPair (G : D ⥤ C) where + out : ∀ {A B} (f g : A ⟶ B) [G.IsCosplitPair f g], ReflectsLimit (parallelPair f g) G -instance {A B} (f g : A ⟶ B) [G.IsSplitPair f g] [ReflectsColimitOfIsSplitPair G] : - ReflectsColimit (parallelPair f g) G := ReflectsColimitOfIsSplitPair.out f g +instance {A B} (f g : A ⟶ B) [G.IsCosplitPair f g] [ReflectsLimitOfIsCosplitPair G] : + ReflectsLimit (parallelPair f g) G := ReflectsLimitOfIsCosplitPair.out f g -instance [ReflectsColimitOfIsSplitPair G] : ∀ (A : Algebra adj.toMonad), - ReflectsColimit (parallelPair (F.map A.a) - (NatTrans.app adj.counit (F.obj A.A))) G := - fun _ => ReflectsColimitOfIsSplitPair.out _ _ +instance [ReflectsLimitOfIsCosplitPair F] : ∀ (A : Coalgebra adj.toComonad), + ReflectsLimit (parallelPair (G.map A.a) + (NatTrans.app adj.unit (G.obj A.A))) F := + fun _ => ReflectsLimitOfIsCosplitPair.out _ _ -/-- To show `G` is a monadic right adjoint, we can show it preserves and reflects `G`-split -coequalizers, and `C` has them. +/-- To show `F` is a comonadic left adjoint, we can show it preserves and reflects `F`-split +equalizers, and `C` has them. -/ -def monadicOfHasPreservesReflectsGSplitCoequalizers [HasCoequalizerOfIsSplitPair G] - [PreservesColimitOfIsSplitPair G] [ReflectsColimitOfIsSplitPair G] : - MonadicRightAdjoint G where +def comonadicOfHasPreservesReflectsGSplitEqualizers [HasEqualizerOfIsCosplitPair F] + [PreservesLimitOfIsCosplitPair F] [ReflectsLimitOfIsCosplitPair F] : + ComonadicLeftAdjoint F where adj := adj eqv := by - have : ∀ (X : Algebra adj.toMonad), IsIso ((comparisonAdjunction adj).unit.app X) := by + have : ∀ (X : Coalgebra adj.toComonad), IsIso ((comparisonAdjunction adj).counit.app X) := by intro X - apply @isIso_of_reflects_iso _ _ _ _ _ _ _ (Monad.forget adj.toMonad) ?_ _ - · change IsIso ((comparisonAdjunction adj).unit.app X).f - rw [comparisonAdjunction_unit_f] + apply @isIso_of_reflects_iso _ _ _ _ _ _ _ (Comonad.forget adj.toComonad) ?_ _ + · change IsIso ((comparisonAdjunction adj).counit.app X).f + rw [comparisonAdjunction_counit_f] change IsIso - (IsColimit.coconePointUniqueUpToIso (beckCoequalizer X) - (unitColimitOfPreservesCoequalizer X)).hom - exact (IsColimit.coconePointUniqueUpToIso _ _).isIso_hom - have : ∀ (Y : D), IsIso ((comparisonAdjunction adj).counit.app Y) := by + (IsLimit.conePointUniqueUpToIso (beckEqualizer X) + (counitLimitOfPreservesEqualizer X)).inv + exact (IsLimit.conePointUniqueUpToIso _ _).isIso_inv + have : ∀ (Y : C), IsIso ((comparisonAdjunction adj).unit.app Y) := by intro Y - rw [comparisonAdjunction_counit_app] + rw [comparisonAdjunction_unit_app] -- Porting note: passing instances through - change IsIso (IsColimit.coconePointUniqueUpToIso _ ?_).hom + change IsIso (IsLimit.conePointUniqueUpToIso _ ?_).inv infer_instance -- Porting note: passing instances through - apply @counitCoequalizerOfReflectsCoequalizer _ _ _ _ _ _ _ _ ?_ + apply @unitEqualizerOfCoreflectsEqualizer _ _ _ _ _ _ _ _ ?_ letI _ : - G.IsSplitPair (F.map (G.map (adj.counit.app Y))) - (adj.counit.app (F.obj (G.obj Y))) := - MonadicityInternal.main_pair_G_split _ ((comparison adj).obj Y) + F.IsCosplitPair (G.map (F.map (adj.unit.app Y))) + (adj.unit.app (G.obj (F.obj Y))) := + ComonadicityInternal.main_pair_F_cosplit _ ((comparison adj).obj Y) infer_instance - exact (comparisonAdjunction adj).toEquivalence.isEquivalence_inverse -set_option linter.uppercaseLean3 false in -#align category_theory.monad.monadic_of_has_preserves_reflects_G_split_coequalizers CategoryTheory.Monad.monadicOfHasPreservesReflectsGSplitCoequalizers + exact (comparisonAdjunction adj).toEquivalence.symm.isEquivalence_inverse -- Porting note: added these to replace parametric instances lean4#2311 --- [∀ ⦃A B⦄ (f g : A ⟶ B) [G.IsSplitPair f g], CreatesColimit (parallelPair f g) G] : -class CreatesColimitOfIsSplitPair (G : D ⥤ C) where - out : ∀ {A B} (f g : A ⟶ B) [G.IsSplitPair f g], CreatesColimit (parallelPair f g) G +-- [∀ ⦃A B⦄ (f g : A ⟶ B) [G.IsCosplitPair f g], CreatesLimit (parallelPair f g) G] : +class CreatesLimitOfIsCosplitPair (G : D ⥤ C) where + out : ∀ {A B} (f g : A ⟶ B) [G.IsCosplitPair f g], CreatesLimit (parallelPair f g) G -instance {A B} (f g : A ⟶ B) [G.IsSplitPair f g] [CreatesColimitOfIsSplitPair G] : - CreatesColimit (parallelPair f g) G := CreatesColimitOfIsSplitPair.out f g +instance {A B} (f g : A ⟶ B) [G.IsCosplitPair f g] [CreatesLimitOfIsCosplitPair G] : + CreatesLimit (parallelPair f g) G := CreatesLimitOfIsCosplitPair.out f g -instance [CreatesColimitOfIsSplitPair G] : ∀ (A : Algebra adj.toMonad), - CreatesColimit (parallelPair (F.map A.a) - (NatTrans.app adj.counit (F.obj A.A))) G := - fun _ => CreatesColimitOfIsSplitPair.out _ _ +instance [CreatesLimitOfIsCosplitPair F] : ∀ (A : Coalgebra adj.toComonad), + CreatesLimit (parallelPair (G.map A.a) + (NatTrans.app adj.unit (G.obj A.A))) F := + fun _ => CreatesLimitOfIsCosplitPair.out _ _ /-- -Beck's monadicity theorem. If `G` has a right adjoint and creates coequalizers of `G`-split pairs, -then it is monadic. -This is the converse of `createsGSplitOfMonadic`. +Beck's comonadicity theorem. If `F` has a right adjoint and creates equalizers of `F`-cosplit pairs, +then it is comonadic. +This is the converse of `createsGSplitOfComonadic`. -/ -def monadicOfCreatesGSplitCoequalizers [CreatesColimitOfIsSplitPair G] : - MonadicRightAdjoint G := by - let I {A B} (f g : A ⟶ B) [G.IsSplitPair f g] : HasColimit (parallelPair f g ⋙ G) := by - apply @hasColimitOfIso _ _ _ _ _ _ ?_ (diagramIsoParallelPair.{v₁} _) - exact inferInstanceAs <| HasCoequalizer (G.map f) (G.map g) - have : HasCoequalizerOfIsSplitPair G := ⟨fun _ _ => hasColimit_of_created (parallelPair _ _) G⟩ - have : PreservesColimitOfIsSplitPair G := ⟨by intros; infer_instance⟩ - have : ReflectsColimitOfIsSplitPair G := ⟨by intros; infer_instance⟩ - exact monadicOfHasPreservesReflectsGSplitCoequalizers adj -set_option linter.uppercaseLean3 false in -#align category_theory.monad.monadic_of_creates_G_split_coequalizers CategoryTheory.Monad.monadicOfCreatesGSplitCoequalizers - -/-- An alternate version of Beck's monadicity theorem. If `G` reflects isomorphisms, preserves -coequalizers of `G`-split pairs and `C` has coequalizers of `G`-split pairs, then it is monadic. +def comonadicOfCreatesGSplitEqualizers [CreatesLimitOfIsCosplitPair F] : + ComonadicLeftAdjoint F := by + let I {A B} (f g : A ⟶ B) [F.IsCosplitPair f g] : HasLimit (parallelPair f g ⋙ F) := by + apply @hasLimitOfIso _ _ _ _ _ _ ?_ (diagramIsoParallelPair.{v₁} _).symm + exact inferInstanceAs <| HasEqualizer (F.map f) (F.map g) + have : HasEqualizerOfIsCosplitPair F := ⟨fun _ _ => hasLimit_of_created (parallelPair _ _) F⟩ + have : PreservesLimitOfIsCosplitPair F := ⟨by intros; infer_instance⟩ + have : ReflectsLimitOfIsCosplitPair F := ⟨by intros; infer_instance⟩ + exact comonadicOfHasPreservesReflectsGSplitEqualizers adj + +/-- An alternate version of Beck's comonadicity theorem. If `F` reflects isomorphisms, preserves +equalizers of `F`-cosplit pairs and `C` has equalizers of `F`-cosplit pairs, then it is comonadic. -/ -def monadicOfHasPreservesGSplitCoequalizersOfReflectsIsomorphisms [G.ReflectsIsomorphisms] - [HasCoequalizerOfIsSplitPair G] [PreservesColimitOfIsSplitPair G] : - MonadicRightAdjoint G := by - have : ReflectsColimitOfIsSplitPair G := ⟨fun f g _ => by - have := HasCoequalizerOfIsSplitPair.out G f g - apply reflectsColimitOfReflectsIsomorphisms⟩ - apply monadicOfHasPreservesReflectsGSplitCoequalizers adj -set_option linter.uppercaseLean3 false in -#align category_theory.monad.monadic_of_has_preserves_G_split_coequalizers_of_reflects_isomorphisms CategoryTheory.Monad.monadicOfHasPreservesGSplitCoequalizersOfReflectsIsomorphisms +def monadicOfHasPreservesGSplitCoequalizersOfReflectsIsomorphisms [F.ReflectsIsomorphisms] + [HasEqualizerOfIsCosplitPair F] [PreservesLimitOfIsCosplitPair F] : + ComonadicLeftAdjoint F := by + have : ReflectsLimitOfIsCosplitPair F := ⟨fun f g _ => by + have := HasEqualizerOfIsCosplitPair.out F f g + apply reflectsLimitOfReflectsIsomorphisms⟩ + apply comonadicOfHasPreservesReflectsGSplitEqualizers adj -end BeckMonadicity +end BeckComonadicity -section ReflexiveMonadicity +section CoreflexiveComonadicity -variable [HasReflexiveCoequalizers D] [G.ReflectsIsomorphisms] +variable [HasCoreflexiveEqualizers C] [F.ReflectsIsomorphisms] -- Porting note: added these to replace parametric instances lean4#2311 --- [∀ ⦃A B⦄ (f g : A ⟶ B) [G.IsReflexivePair f g], PreservesColimit (parallelPair f g) G] : -class PreservesColimitOfIsReflexivePair (G : C ⥤ D) where - out : ∀ ⦃A B⦄ (f g : A ⟶ B) [IsReflexivePair f g], PreservesColimit (parallelPair f g) G +-- [∀ ⦃A B⦄ (f g : A ⟶ B) [F.IsCoreflexivePair f g], PreservesLimit (parallelPair f g) F] : +class PreservesLimitOfIsCoreflexivePair (F : C ⥤ D) where + out : ∀ ⦃A B⦄ (f g : A ⟶ B) [IsCoreflexivePair f g], PreservesLimit (parallelPair f g) F -instance {A B} (f g : A ⟶ B) [IsReflexivePair f g] [PreservesColimitOfIsReflexivePair G] : - PreservesColimit (parallelPair f g) G := PreservesColimitOfIsReflexivePair.out f g +instance temp {A B} (f g : A ⟶ B) [IsCoreflexivePair f g] [PreservesLimitOfIsCoreflexivePair F] : + PreservesLimit (parallelPair f g) F := PreservesLimitOfIsCoreflexivePair.out f g -instance [PreservesColimitOfIsReflexivePair G] : ∀ X : Algebra adj.toMonad, - PreservesColimit (parallelPair (F.map X.a) - (NatTrans.app adj.counit (F.obj X.A))) G := - fun _ => PreservesColimitOfIsReflexivePair.out _ _ +instance [PreservesLimitOfIsCoreflexivePair F] : ∀ X : Coalgebra adj.toComonad, + PreservesLimit (parallelPair (G.map X.a) + (NatTrans.app adj.unit (G.obj X.A))) F := + fun _ => PreservesLimitOfIsCoreflexivePair.out _ _ -variable [PreservesColimitOfIsReflexivePair G] +variable [PreservesLimitOfIsCoreflexivePair F] -/-- Reflexive (crude) monadicity theorem. If `G` has a right adjoint, `D` has and `G` preserves -reflexive coequalizers and `G` reflects isomorphisms, then `G` is monadic. +/-- Reflexive (crude) monadicity theorem. If `F` has a right adjoint, `C` has and `F` preserves +coreflexive equalizers and `F` reflects isomorphisms, then `F` is comonadic. -/ -def monadicOfHasPreservesReflexiveCoequalizersOfReflectsIsomorphisms : MonadicRightAdjoint G where +def comonadicOfHasPreservesCoreflexiveEqualizersOfReflectsIsomorphisms : ComonadicLeftAdjoint F where adj := adj eqv := by - have : ∀ (X : Algebra adj.toMonad), IsIso ((comparisonAdjunction adj).unit.app X) := by + have : ∀ (X : adj.toComonad.Coalgebra), IsIso ((comparisonAdjunction adj).counit.app X) := by intro X apply - @isIso_of_reflects_iso _ _ _ _ _ _ _ (Monad.forget adj.toMonad) ?_ _ - · change IsIso ((comparisonAdjunction adj).unit.app X).f - rw [comparisonAdjunction_unit_f] - exact (IsColimit.coconePointUniqueUpToIso (beckCoequalizer X) - (unitColimitOfPreservesCoequalizer X)).isIso_hom - have : ∀ (Y : D), IsIso ((comparisonAdjunction adj).counit.app Y) := by + @isIso_of_reflects_iso _ _ _ _ _ _ _ (Comonad.forget adj.toComonad) ?_ _ + · change IsIso ((comparisonAdjunction adj).counit.app X).f + rw [comparisonAdjunction_counit_f] + exact (IsLimit.conePointUniqueUpToIso (beckEqualizer X) + (counitLimitOfPreservesEqualizer X)).isIso_inv + have : ∀ (Y : C), IsIso ((comparisonAdjunction adj).unit.app Y) := by intro Y - rw [comparisonAdjunction_counit_app] + rw [comparisonAdjunction_unit_app] -- Porting note: passing instances through - change IsIso (IsColimit.coconePointUniqueUpToIso _ ?_).hom + change IsIso (IsLimit.conePointUniqueUpToIso _ ?_).inv infer_instance -- Porting note: passing instances through - apply @counitCoequalizerOfReflectsCoequalizer _ _ _ _ _ _ _ _ ?_ - apply reflectsColimitOfReflectsIsomorphisms - exact (comparisonAdjunction adj).toEquivalence.isEquivalence_inverse -#align category_theory.monad.monadic_of_has_preserves_reflexive_coequalizers_of_reflects_isomorphisms CategoryTheory.Monad.monadicOfHasPreservesReflexiveCoequalizersOfReflectsIsomorphisms - -end ReflexiveMonadicity + have : IsCoreflexivePair (G.map (F.map (adj.unit.app Y))) (adj.unit.app (G.obj (F.obj Y))) := by + apply IsCoreflexivePair.mk' (G.map (adj.counit.app _)) _ _ + · rw [← G.map_comp, ← G.map_id] + exact congr_arg G.map (adj.left_triangle_components Y) + · rw [← G.map_id] + simp + apply @unitEqualizerOfCoreflectsEqualizer _ _ _ _ _ _ _ _ ?_ + apply reflectsLimitOfReflectsIsomorphisms + exact (comparisonAdjunction adj).toEquivalence.symm.isEquivalence_inverse +--PreservesLimit (parallelPair (G.map (F.map (adj.unit.app Y))) (adj.unit.app (G.obj (F.obj Y)))) F +end CoreflexiveComonadicity end -end Monad +end Comonad end CategoryTheory diff --git a/Mathlib/CategoryTheory/Monad/Limits.lean b/Mathlib/CategoryTheory/Monad/Limits.lean index b793f6e64826db..93d89e8243042c 100644 --- a/Mathlib/CategoryTheory/Monad/Limits.lean +++ b/Mathlib/CategoryTheory/Monad/Limits.lean @@ -406,4 +406,288 @@ noncomputable def leftAdjointPreservesTerminalOfReflective (R : D ⥤ C) [Reflec end +---------------------------------------------------------------------------------------------------- +---------------------------------------------------------------------------------------------------- + +namespace Comonad + +variable {C : Type u₁} [Category.{v₁} C] +variable {T : Comonad C} +variable {J : Type u} [Category.{v} J] + +namespace ForgetCreatesColimits' + +variable (D : J ⥤ Coalgebra T) (c : Cocone (D ⋙ T.forget)) (t : IsColimit c) + +/-- (Impl) The natural transformation used to define the new cocone -/ +@[simps] +def γ : D ⋙ T.forget ⟶ D ⋙ T.forget ⋙ ↑T where app j := (D.obj j).a + +/-- (Impl) This new cocone is used to construct the algebra structure -/ +@[simps! ι_app] +def newCocone : Cocone (D ⋙ T.forget) where + pt := T.obj c.pt + ι := γ D ≫ whiskerRight c.ι (T : C ⥤ C) ≫ (Functor.constComp J _ (T : C ⥤ C)).hom + +/-- The coalgebra structure which will be the apex of the new limit cone for `D`. -/ +@[simps] +def coconePoint : Coalgebra T where + A := c.pt + a := t.desc (newCocone D c) + counit := t.hom_ext fun j ↦ by + simp + rw [← Category.assoc, (D.obj j).counit, Category.id_comp] + coassoc := t.hom_ext fun j ↦ by + simp + rw [← Category.assoc, (D.obj j).coassoc, ← Functor.map_comp, t.fac (newCocone D c) j, + newCocone_ι_app, Functor.map_comp, assoc] + +/-- (Impl) Construct the lifted cocone in `Coalgebra T` which will be colimiting. -/ +@[simps] +def liftedCocone : Cocone D where + pt := coconePoint D c t + ι := + { app := fun j => { f := c.ι.app j } + naturality := fun X Y f => by + ext1 + dsimp + erw [c.w f] + simp } + +/-- (Impl) Prove that the lifted cocone is colimiting. -/ +@[simps] +def liftedCoconeIsColimit : IsColimit (liftedCocone D c t) where + desc s := + { f := t.desc ((forget T).mapCocone s) + h := + t.hom_ext fun j => by + dsimp + rw [← Category.assoc, ← Category.assoc, t.fac, newCocone_ι_app, t.fac, + Functor.mapCocone_ι_app, Category.assoc, ← Functor.map_comp, t.fac] + apply (s.ι.app j).h } + uniq s m J := by + ext1 + apply t.hom_ext + intro j + simpa [t.fac ((forget T).mapCocone s) j] using congr_arg Coalgebra.Hom.f (J j) + +end ForgetCreatesColimits' + +-- Theorem 5.6.5 from [Riehl][riehl2017] +/-- The forgetful functor from the Eilenberg-Moore category creates colimits. -/ +noncomputable instance forgetCreatesColimit : CreatesColimitsOfSize (forget T) where + CreatesColimitsOfShape := { + CreatesColimit := fun {D} => + createsColimitOfReflectsIso fun c t => + { liftedCocone := ForgetCreatesColimits'.liftedCocone D c t + validLift := Cocones.ext (Iso.refl _) fun _ => (comp_id _) + makesColimit := ForgetCreatesColimits'.liftedCoconeIsColimit _ _ _ } } + +/-- If `D ⋙ forget T` has a colimit, then `D` has a colimit. -/ +theorem hasColimit_of_comp_forget_hasColimit (D : J ⥤ Coalgebra T) [HasColimit (D ⋙ forget T)] : + HasColimit D := + hasColimit_of_created D (forget T) + +namespace ForgetCreatesLimits' + +-- Let's hide the implementation details in a namespace +variable {D : J ⥤ Coalgebra T} (c : Cone (D ⋙ forget T)) (t : IsLimit c) + +-- We have a diagram D of shape J in the category of coalgebras, and we assume that we are given a +-- limit for its image D ⋙ forget T under the forgetful functor, say its apex is L. +-- We'll construct a limiting algebra for D, whose carrier will also be L. +-- To do this, we must find a map L ⟶ TL. Since T preserves limits, TL is also a limit. +-- In particular, it is a limit for the diagram `(D ⋙ forget T) ⋙ T` +-- so to construct a map L ⟶ TL it suffices to show that L is the apex of a cone for this diagram. +-- In other words, we need a natural transformation from const L to `(D ⋙ forget T) ⋙ T`. +-- But we already know that L is the apex of a cone for the diagram `D ⋙ forget T`, so it +-- suffices to give a natural transformation `((D ⋙ forget T) ⋙ T) ⟶ (D ⋙ forget T)`: +/-- (Impl) +The natural transformation given by the coalgebra structure maps, used to construct a cone `c` with +apex `limit (D ⋙ forget T)`. + -/ +@[simps] +def γ : D ⋙ forget T ⟶ (D ⋙ forget T) ⋙ ↑T where app j := (D.obj j).a + +/-- (Impl) +A cone for the diagram `(D ⋙ forget T) ⋙ T` found by composing the natural transformation `γ` +with the limiting cone for `D ⋙ forget T`. +-/ +@[simps] +def newCone : Cone ((D ⋙ forget T) ⋙ (T : C ⥤ C)) where + pt := c.pt + π := c.π ≫ γ + +variable [PreservesLimit (D ⋙ forget T) (T : C ⥤ C)] + +/-- (Impl) +Define the map `λ : TL ⟶ L`, which will serve as the structure of the algebra on `L`, and +we will show is the limiting object. We use the cone constructed by `c` and the fact that +`T` preserves limits to produce this morphism. +-/ +abbrev lambda : c.pt ⟶ ((T : C ⥤ C).mapCone c).pt := + (isLimitOfPreserves _ t).lift (newCone c) + +/-- (Impl) The key property defining the map `λ : TL ⟶ L`. -/ +theorem commuting (j : J) : lambda c t ≫ (T : C ⥤ C).map (c.π.app j) = c.π.app j ≫ (D.obj j).a := + (isLimitOfPreserves _ t).fac (newCone c) j + +variable [PreservesColimit ((D ⋙ forget T) ⋙ ↑T) (T : C ⥤ C)] + +/-- (Impl) +Construct the limiting algebra from the map `λ : TL ⟶ L` given by `lambda`. We are required to +show it satisfies the two coalgebra laws, which follow from the coalgebra laws for the image of `D` +and our `commuting` lemma. +-/ +@[simps] +def conePoint : Coalgebra T where + A := c.pt + a := lambda c t + counit := t.hom_ext fun j ↦ by + sorry + coassoc := by + have : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor := sorry + apply (isLimitOfPreserves _ (isLimitOfPreserves _ t)).hom_ext + intro j + simp + rw [← Functor.map_comp, commuting, Functor.map_comp] + erw [← T.δ.naturality (c.π.app j)] + congr 1 + -- (D.obj j).coassoc + simp + sorry + +/-- (Impl) Construct the lifted cocone in `Coalgebra T` which will be colimiting. -/ +@[simps] +def liftedCone : Cone D where + pt := conePoint c t + π := + { app := fun j => + { f := c.π.app j + h := commuting _ _ _ } + naturality := fun A B f => by + ext1 + dsimp + rw [id_comp, ← c.w] + rfl } + +/-- (Impl) Prove that the lifted cocone is colimiting. -/ +@[simps] +def liftedConeIsLimit : IsLimit (liftedCone c t) where + lift s := + { f := t.lift ((forget T).mapCone s) + h := + (isLimitOfPreserves (T : C ⥤ C) t).hom_ext fun j => by + dsimp + rw [Category.assoc, ← t.fac, Category.assoc, t.fac, commuting] + sorry } --apply Coalgebra.Hom.h } + uniq s m J := by + ext1 + apply t.hom_ext + intro j + simpa using congr_arg Coalgebra.Hom.f (J j) + +end ForgetCreatesLimits' + +open ForgetCreatesLimits' + +-- TODO: the converse of this is true as well +/-- The forgetful functor from the Eilenberg-Moore category for a comonad creates any limit +which the comonad itself preserves. +-/ +noncomputable instance forgetCreatesLimit (D : J ⥤ Coalgebra T) + [PreservesLimit (D ⋙ forget T) (T : C ⥤ C)] + [PreservesLimit ((D ⋙ forget T) ⋙ ↑T) (T : C ⥤ C)] : CreatesLimit D (forget T) := + createsLimitOfReflectsIso fun c t => + { liftedCone := + { pt := conePoint c t + π := + { app := fun j => + { f := c.π.app j + h := commuting _ _ _ } + naturality := fun A B f => by + ext1 + dsimp + erw [id_comp, c.w] } } + validLift := Cones.ext (Iso.refl _) + makesLimit := liftedConeIsLimit _ _ } + +noncomputable instance forgetCreatesLimitsOfShape [PreservesLimitsOfShape J (T : C ⥤ C)] : + CreatesLimitsOfShape J (forget T) where CreatesLimit := by infer_instance + +noncomputable instance forgetCreatesLimits [PreservesLimitsOfSize.{v, u} (T : C ⥤ C)] : + CreatesLimitsOfSize.{v, u} (forget T) where CreatesLimitsOfShape := by infer_instance + +/-- For `D : J ⥤ Coalgebra T`, `D ⋙ forget T` has a limit, then `D` has a limit provided colimits +of shape `J` are preserved by `T`. +-/ +theorem forget_creates_limits_of_comonad_preserves [PreservesLimitsOfShape J (T : C ⥤ C)] + (D : J ⥤ Coalgebra T) [HasLimit (D ⋙ forget T)] : HasLimit D := + hasLimit_of_created D (forget T) + +end Comonad + +variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D] +variable {J : Type u} [Category.{v} J] + +instance comp_comparison_forget_hasColimit (F : J ⥤ D) (R : D ⥤ C) [ComonadicLeftAdjoint R] + [HasColimit (F ⋙ R)] : + HasColimit ((F ⋙ Comonad.comparison (comonadicAdjunction R)) ⋙ Comonad.forget _) := + @hasColimitOfIso _ _ _ _ (F ⋙ R) _ _ + (isoWhiskerLeft F (Comonad.comparisonForget (comonadicAdjunction R)).symm) + +instance comp_comparison_hasColimit (F : J ⥤ D) (R : D ⥤ C) [ComonadicLeftAdjoint R] + [HasColimit (F ⋙ R)] : HasColimit (F ⋙ Comonad.comparison (comonadicAdjunction R)) := + Comonad.hasColimit_of_comp_forget_hasColimit (F ⋙ Comonad.comparison (comonadicAdjunction R)) + +/-- Any monadic functor creates limits. -/ +noncomputable def monadicCreatesColimits (R : D ⥤ C) [ComonadicLeftAdjoint R] : + CreatesColimitsOfSize.{v, u} R := + createsColimitsOfNatIso (Comonad.comparisonForget (comonadicAdjunction R)) + +/-- The forgetful functor from the Eilenberg-Moore category for a comonad creates any limit +which the comonad itself preserves. +-/ +noncomputable def comonadicCreatesLimitOfPreservesLimit (R : D ⥤ C) (K : J ⥤ D) + [ComonadicLeftAdjoint R] [PreservesLimit (K ⋙ R) (comonadicRightAdjoint R ⋙ R)] + [PreservesLimit ((K ⋙ R) ⋙ comonadicRightAdjoint R ⋙ R) (comonadicRightAdjoint R ⋙ R)] : + CreatesLimit K R := by + -- Porting note: It would be nice to have a variant of apply which introduces goals for missing + -- instances. + letI A := Comonad.comparison (comonadicAdjunction R) + letI B := Comonad.forget (Adjunction.toComonad (comonadicAdjunction R)) + let i : (K ⋙ Comonad.comparison (comonadicAdjunction R)) ⋙ Comonad.forget _ ≅ K ⋙ R := + Functor.associator _ _ _ ≪≫ + isoWhiskerLeft K (Comonad.comparisonForget (comonadicAdjunction R)) + letI : PreservesLimit ((K ⋙ A) ⋙ Comonad.forget + (Adjunction.toComonad (comonadicAdjunction R))) + (Adjunction.toComonad (comonadicAdjunction R)).toFunctor := by + dsimp + exact preservesLimitOfIsoDiagram _ i.symm + letI : PreservesLimit + (((K ⋙ A) ⋙ Comonad.forget (Adjunction.toComonad (comonadicAdjunction R))) ⋙ + (Adjunction.toComonad (comonadicAdjunction R)).toFunctor) + (Adjunction.toComonad (comonadicAdjunction R)).toFunctor := by + dsimp + exact preservesLimitOfIsoDiagram _ (isoWhiskerRight i (comonadicRightAdjoint R ⋙ R)).symm + letI : CreatesLimit (K ⋙ A) B := CategoryTheory.Comonad.forgetCreatesLimit _ + letI : CreatesLimit K (A ⋙ B) := CategoryTheory.compCreatesLimit _ _ + let e := Comonad.comparisonForget (comonadicAdjunction R) + apply createsLimitOfNatIso e + +/-- A comonadic functor creates any limits of shapes it preserves. -/ +noncomputable def comonadicCreatesLimitsOfShapeOfPreservesLimitsOfShape (R : D ⥤ C) + [ComonadicLeftAdjoint R] [PreservesLimitsOfShape J R] : CreatesLimitsOfShape J R := + letI : PreservesLimitsOfShape J (comonadicRightAdjoint R) := by + apply (Adjunction.rightAdjointPreservesLimits (comonadicAdjunction R)).1 + letI : PreservesLimitsOfShape J (comonadicRightAdjoint R ⋙ R) := by + apply CategoryTheory.Limits.compPreservesLimitsOfShape _ _ + ⟨comonadicCreatesLimitOfPreservesLimit _ _⟩ + +/-- A comonadic functor creates limits if it preserves limits. -/ +noncomputable def comonadicCreatesLimitsOfPreservesLimits (R : D ⥤ C) [ComonadicLeftAdjoint R] + [PreservesLimitsOfSize.{v, u} R] : CreatesLimitsOfSize.{v, u} R where + CreatesLimitsOfShape := + comonadicCreatesLimitsOfShapeOfPreservesLimitsOfShape _ + end CategoryTheory From c95407d5718297d405ff3683acf52dafe5c6f7fb Mon Sep 17 00:00:00 2001 From: dagurtomas Date: Thu, 27 Jun 2024 17:46:32 +0000 Subject: [PATCH 05/29] close a sorry --- Mathlib/CategoryTheory/Monad/Limits.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Mathlib/CategoryTheory/Monad/Limits.lean b/Mathlib/CategoryTheory/Monad/Limits.lean index 93d89e8243042c..f8d511a1662187 100644 --- a/Mathlib/CategoryTheory/Monad/Limits.lean +++ b/Mathlib/CategoryTheory/Monad/Limits.lean @@ -544,7 +544,8 @@ def conePoint : Coalgebra T where A := c.pt a := lambda c t counit := t.hom_ext fun j ↦ by - sorry + rw [assoc, ← show _ = _ ≫ c.π.app j from T.ε.naturality _, ← assoc, commuting, assoc] + simp [Coalgebra.counit (D.obj j)] coassoc := by have : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor := sorry apply (isLimitOfPreserves _ (isLimitOfPreserves _ t)).hom_ext From b5b9d0f0aebaec6e259151bb8b51d7122958cb79 Mon Sep 17 00:00:00 2001 From: dagurtomas Date: Thu, 27 Jun 2024 18:03:49 +0000 Subject: [PATCH 06/29] close a sorry --- Mathlib/CategoryTheory/Monad/Limits.lean | 17 +++++++---------- 1 file changed, 7 insertions(+), 10 deletions(-) diff --git a/Mathlib/CategoryTheory/Monad/Limits.lean b/Mathlib/CategoryTheory/Monad/Limits.lean index f8d511a1662187..a13fbf80c99115 100644 --- a/Mathlib/CategoryTheory/Monad/Limits.lean +++ b/Mathlib/CategoryTheory/Monad/Limits.lean @@ -519,6 +519,7 @@ def newCone : Cone ((D ⋙ forget T) ⋙ (T : C ⥤ C)) where π := c.π ≫ γ variable [PreservesLimit (D ⋙ forget T) (T : C ⥤ C)] + [PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor] /-- (Impl) Define the map `λ : TL ⟶ L`, which will serve as the structure of the algebra on `L`, and @@ -547,16 +548,12 @@ def conePoint : Coalgebra T where rw [assoc, ← show _ = _ ≫ c.π.app j from T.ε.naturality _, ← assoc, commuting, assoc] simp [Coalgebra.counit (D.obj j)] coassoc := by - have : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor := sorry - apply (isLimitOfPreserves _ (isLimitOfPreserves _ t)).hom_ext - intro j - simp - rw [← Functor.map_comp, commuting, Functor.map_comp] - erw [← T.δ.naturality (c.π.app j)] - congr 1 - -- (D.obj j).coassoc - simp - sorry + refine (isLimitOfPreserves _ (isLimitOfPreserves _ t)).hom_ext fun j => ?_ + rw [Functor.mapCone_π_app, Functor.mapCone_π_app, assoc, + ← show _ = _ ≫ T.map (T.map _) from T.δ.naturality _, assoc, ← Functor.map_comp, commuting, + Functor.map_comp, ← assoc, commuting] + simp only [Functor.comp_obj, forget_obj, Functor.const_obj_obj, assoc] + rw [(D.obj j).coassoc, ← assoc, ← assoc, commuting] /-- (Impl) Construct the lifted cocone in `Coalgebra T` which will be colimiting. -/ @[simps] From 7e54a6fbcbca62b984e081949e5b691f58f4987a Mon Sep 17 00:00:00 2001 From: dagurtomas Date: Thu, 27 Jun 2024 18:16:33 +0000 Subject: [PATCH 07/29] last sorry in limits file --- Mathlib/CategoryTheory/Monad/Limits.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/Mathlib/CategoryTheory/Monad/Limits.lean b/Mathlib/CategoryTheory/Monad/Limits.lean index a13fbf80c99115..3d110d7d92634a 100644 --- a/Mathlib/CategoryTheory/Monad/Limits.lean +++ b/Mathlib/CategoryTheory/Monad/Limits.lean @@ -577,8 +577,9 @@ def liftedConeIsLimit : IsLimit (liftedCone c t) where h := (isLimitOfPreserves (T : C ⥤ C) t).hom_ext fun j => by dsimp - rw [Category.assoc, ← t.fac, Category.assoc, t.fac, commuting] - sorry } --apply Coalgebra.Hom.h } + rw [Category.assoc, ← t.fac, Category.assoc, t.fac, commuting, ← assoc, ← assoc, t.fac, + assoc, ← Functor.map_comp, t.fac] + exact (s.π.app j).h } uniq s m J := by ext1 apply t.hom_ext From a2a8f01e2974bf9d8a7950fe74e75ddd524a41b6 Mon Sep 17 00:00:00 2001 From: adamtopaz Date: Thu, 27 Jun 2024 12:26:38 -0600 Subject: [PATCH 08/29] wip --- .../Limits/Preserves/Shapes/Equalizers.lean | 10 ++++++++++ Mathlib/CategoryTheory/Monad/Comonadicity.lean | 4 ++-- 2 files changed, 12 insertions(+), 2 deletions(-) diff --git a/Mathlib/CategoryTheory/Limits/Preserves/Shapes/Equalizers.lean b/Mathlib/CategoryTheory/Limits/Preserves/Shapes/Equalizers.lean index ff5c65747da92f..bfa732dffeefb3 100644 --- a/Mathlib/CategoryTheory/Limits/Preserves/Shapes/Equalizers.lean +++ b/Mathlib/CategoryTheory/Limits/Preserves/Shapes/Equalizers.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Bhavik Mehta -/ import Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer +import Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer import Mathlib.CategoryTheory.Limits.Preserves.Basic #align_import category_theory.limits.preserves.shapes.equalizers from "leanprover-community/mathlib"@"4698e35ca56a0d4fa53aa5639c3364e0a77f4eba" @@ -252,6 +253,15 @@ instance (priority := 1) preservesSplitCoequalizers (f g : X ⟶ Y) [HasSplitCoe ((HasSplitCoequalizer.isSplitCoequalizer f g).map G).isCoequalizer #align category_theory.limits.preserves_split_coequalizers CategoryTheory.Limits.preservesSplitCoequalizers +instance (priority := 1) preservesSplitEqualizers (f g : X ⟶ Y) [HasSplitEqualizer f g] : + PreservesLimit (parallelPair f g) G := by + apply + preservesLimitOfPreservesLimitCone + (HasSplitEqualizer.isSplitEqualizer f g).isEqualizer + apply + (isLimitMapConeForkEquiv G _).symm + ((HasSplitEqualizer.isSplitEqualizer f g).map G).isEqualizer + end Coequalizers end CategoryTheory.Limits diff --git a/Mathlib/CategoryTheory/Monad/Comonadicity.lean b/Mathlib/CategoryTheory/Monad/Comonadicity.lean index 24a55621609b23..aa9019c250a97f 100644 --- a/Mathlib/CategoryTheory/Monad/Comonadicity.lean +++ b/Mathlib/CategoryTheory/Monad/Comonadicity.lean @@ -227,10 +227,10 @@ def createsGSplitEqualizersOfComonadic [ComonadicLeftAdjoint F] ⦃A B⦄ (f g : -- Porting note: oddly (config := {allowSynthFailures := true}) had no effect here and below · apply @preservesLimitOfIsoDiagram _ _ _ _ _ _ _ _ _ (diagramIsoParallelPair.{v₁} _).symm ?_ dsimp - sorry --infer_instance + infer_instance · apply @preservesLimitOfIsoDiagram _ _ _ _ _ _ _ _ _ (diagramIsoParallelPair.{v₁} _).symm ?_ dsimp - sorry --infer_instance + infer_instance section BeckComonadicity From 8e8e7d745c37d2360fc0343ccc4c41c49ba9d0c4 Mon Sep 17 00:00:00 2001 From: adamtopaz Date: Thu, 27 Jun 2024 12:40:35 -0600 Subject: [PATCH 09/29] kill two sorries --- Mathlib/CategoryTheory/Monad/Comonadicity.lean | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) diff --git a/Mathlib/CategoryTheory/Monad/Comonadicity.lean b/Mathlib/CategoryTheory/Monad/Comonadicity.lean index aa9019c250a97f..a81a46e5e2b09c 100644 --- a/Mathlib/CategoryTheory/Monad/Comonadicity.lean +++ b/Mathlib/CategoryTheory/Monad/Comonadicity.lean @@ -86,12 +86,19 @@ def comparisonRightAdjointHomEquiv (A : adj.toComonad.Coalgebra) (B : C) ((comparison adj).obj B ⟶ A) ≃ (B ⟶ comparisonRightAdjointObj adj A) where toFun f := by refine equalizer.lift (adj.homEquiv _ _ f.f) ?_ - congr - sorry + simp only [Adjunction.toComonad_coe, Functor.comp_obj, Adjunction.homEquiv_unit, + Functor.id_obj, Category.assoc, ← G.map_comp, ← f.h] + simp invFun f := by refine ⟨(adj.homEquiv _ _).symm (f ≫ (equalizer.ι _ _)), ?_⟩ - simp - sorry + apply (adj.homEquiv _ _).injective + simp only [Adjunction.toComonad_coe, Functor.comp_obj, comparison_obj_A, comparison_obj_a, + Adjunction.homEquiv_counit, Functor.id_obj, Functor.map_comp, Category.assoc, + Functor.comp_map, Adjunction.homEquiv_unit, Adjunction.unit_naturality_assoc, + Adjunction.unit_naturality, Adjunction.right_triangle_components_assoc] + congr 1 + symm + apply equalizer.condition left_inv f := by aesop right_inv f := by apply equalizer.hom_ext; simp From 01023036a880c976567232b88ebe7219216f7873 Mon Sep 17 00:00:00 2001 From: adamtopaz Date: Thu, 27 Jun 2024 12:44:34 -0600 Subject: [PATCH 10/29] kill last sorry --- Mathlib/CategoryTheory/Monad/Comonadicity.lean | 10 +--------- 1 file changed, 1 insertion(+), 9 deletions(-) diff --git a/Mathlib/CategoryTheory/Monad/Comonadicity.lean b/Mathlib/CategoryTheory/Monad/Comonadicity.lean index a81a46e5e2b09c..9561918e55840c 100644 --- a/Mathlib/CategoryTheory/Monad/Comonadicity.lean +++ b/Mathlib/CategoryTheory/Monad/Comonadicity.lean @@ -76,6 +76,7 @@ def comparisonRightAdjointObj (A : adj.toComonad.Coalgebra) [HasEqualizer (G.map A.a) (adj.unit.app _)] : C := equalizer (G.map A.a) (adj.unit.app _) +--TODO: CLEAN THIS UP! /-- We have a bijection of homsets which will be used to construct the right adjoint to the comparison functor. @@ -158,16 +159,7 @@ theorem comparisonAdjunction_counit_f (adj.unit.app (G.obj A.A))] (A : adj.toComonad.Coalgebra) : ((comparisonAdjunction adj).counit.app A).f = (beckEqualizer A).lift (counitFork A) := by - apply Limits.Fork.IsLimit.hom_ext (beckEqualizer A) - rw [Fork.IsLimit.lift_ι] - dsimp only [beckFork_ι, unitFork_ι] - rw [comparisonAdjunction_counit_f_aux] simp - suffices h : adj.counit.app A.A ≫ A.a = 𝟙 _ by { - rw [h] - simp only [Functor.comp_obj, Category.comp_id] - } - sorry variable (adj) From 3236a7a49b9dd39926a1bd2ea95f2dc49467c852 Mon Sep 17 00:00:00 2001 From: dagurtomas Date: Thu, 27 Jun 2024 19:34:40 +0000 Subject: [PATCH 11/29] feat(Algebra/ModuleCat): faitfully flat descent --- .../Algebra/Category/ModuleCat/Descent.lean | 46 +++++++++++++++++++ 1 file changed, 46 insertions(+) create mode 100644 Mathlib/Algebra/Category/ModuleCat/Descent.lean diff --git a/Mathlib/Algebra/Category/ModuleCat/Descent.lean b/Mathlib/Algebra/Category/ModuleCat/Descent.lean new file mode 100644 index 00000000000000..544938e295a872 --- /dev/null +++ b/Mathlib/Algebra/Category/ModuleCat/Descent.lean @@ -0,0 +1,46 @@ +import Mathlib.CategoryTheory.Monad.Comonadicity +import Mathlib.CategoryTheory.Preadditive.LeftExact +import Mathlib.Algebra.Category.ModuleCat.Abelian +import Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic +import Mathlib.Algebra.Category.ModuleCat.ChangeOfRings +import Mathlib.RingTheory.Flat.Algebra +import Mathlib.RingTheory.Flat.Basic + +noncomputable section + +open CategoryTheory Comonad ModuleCat Limits MonoidalCategory + +variable {A B : Type} [CommRing.{0} A] [CommRing.{0} B] (f : A →+* B) [f.Flat] + [(extendScalars f).ReflectsIsomorphisms] -- `f` is faithfully flat. + +example : ModuleCat A ⥤ ModuleCat B := ModuleCat.extendScalars f + +instance : Module A B := f.toAlgebra.toModule + +example : extendScalars f ⋙ restrictScalars f ≅ + tensorLeft ((restrictScalars f).obj (ModuleCat.of B B)) := + Iso.refl _ + +instance : PreservesFiniteLimits <| tensorLeft ((restrictScalars f).obj (ModuleCat.of B B)) := + sorry -- This is in a PR + +instance : PreservesFiniteLimits (extendScalars f) := by + have : PreservesFiniteLimits (extendScalars f ⋙ restrictScalars f) := + inferInstanceAs + (PreservesFiniteLimits <| tensorLeft ((restrictScalars f).obj (ModuleCat.of B B))) + apply preservesFiniteLimitsOfReflectsOfPreserves (extendScalars f) (restrictScalars f) + +def extendScalarsComonadic : ComonadicLeftAdjoint (extendScalars f) := by + apply (config := {allowSynthFailures := true}) + monadicOfHasPreservesGSplitCoequalizersOfReflectsIsomorphisms (G := restrictScalars f) + · exact (extendRestrictScalarsAdj f) + · constructor + intros + infer_instance + · suffices ∀ {M N : ModuleCat A} (g : M ⟶ N), + PreservesLimit (parallelPair g (0 : M ⟶ N)) (extendScalars f) by + constructor + intros + apply CategoryTheory.Functor.preservesEqualizerOfPreservesKernels + intro M N g + infer_instance From 02abe6a9fc9b265f05f23e108b310bd7994aacc2 Mon Sep 17 00:00:00 2001 From: dagurtomas Date: Thu, 27 Jun 2024 19:40:44 +0000 Subject: [PATCH 12/29] add examples --- Mathlib/Algebra/Category/ModuleCat/Descent.lean | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/Mathlib/Algebra/Category/ModuleCat/Descent.lean b/Mathlib/Algebra/Category/ModuleCat/Descent.lean index 544938e295a872..b1e41e5227871e 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Descent.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Descent.lean @@ -11,7 +11,7 @@ noncomputable section open CategoryTheory Comonad ModuleCat Limits MonoidalCategory variable {A B : Type} [CommRing.{0} A] [CommRing.{0} B] (f : A →+* B) [f.Flat] - [(extendScalars f).ReflectsIsomorphisms] -- `f` is faithfully flat. + -- [(extendScalars f).ReflectsIsomorphisms] -- `f` is faithfully flat. example : ModuleCat A ⥤ ModuleCat B := ModuleCat.extendScalars f @@ -34,6 +34,7 @@ def extendScalarsComonadic : ComonadicLeftAdjoint (extendScalars f) := by apply (config := {allowSynthFailures := true}) monadicOfHasPreservesGSplitCoequalizersOfReflectsIsomorphisms (G := restrictScalars f) · exact (extendRestrictScalarsAdj f) + · sorry -- This follows from `f` being faithfully flat. · constructor intros infer_instance @@ -44,3 +45,8 @@ def extendScalarsComonadic : ComonadicLeftAdjoint (extendScalars f) := by apply CategoryTheory.Functor.preservesEqualizerOfPreservesKernels intro M N g infer_instance + +example : Comonad (ModuleCat B) := (extendRestrictScalarsAdj f).toComonad + +example (Q : Coalgebra (extendRestrictScalarsAdj f).toComonad) : ModuleCat A := + (comparison (extendScalarsComonadic f).adj).asEquivalence.inverse.obj Q From 20bcedd971c0497087fb4f522f21994a75def574 Mon Sep 17 00:00:00 2001 From: Jack McKoen Date: Thu, 27 Jun 2024 13:50:31 -0600 Subject: [PATCH 13/29] rename --- Mathlib/CategoryTheory/Monad/Comonadicity.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/CategoryTheory/Monad/Comonadicity.lean b/Mathlib/CategoryTheory/Monad/Comonadicity.lean index 9561918e55840c..bd6d2147a73690 100644 --- a/Mathlib/CategoryTheory/Monad/Comonadicity.lean +++ b/Mathlib/CategoryTheory/Monad/Comonadicity.lean @@ -336,7 +336,7 @@ def comonadicOfCreatesGSplitEqualizers [CreatesLimitOfIsCosplitPair F] : /-- An alternate version of Beck's comonadicity theorem. If `F` reflects isomorphisms, preserves equalizers of `F`-cosplit pairs and `C` has equalizers of `F`-cosplit pairs, then it is comonadic. -/ -def monadicOfHasPreservesGSplitCoequalizersOfReflectsIsomorphisms [F.ReflectsIsomorphisms] +def comonadicOfHasPreservesGSplitCoequalizersOfReflectsIsomorphisms [F.ReflectsIsomorphisms] [HasEqualizerOfIsCosplitPair F] [PreservesLimitOfIsCosplitPair F] : ComonadicLeftAdjoint F := by have : ReflectsLimitOfIsCosplitPair F := ⟨fun f g _ => by From 862abbb7eb18f117673234f815225d5c2dc83df3 Mon Sep 17 00:00:00 2001 From: dagurtomas Date: Thu, 27 Jun 2024 20:01:42 +0000 Subject: [PATCH 14/29] add flatness --- Mathlib/Algebra/Category/ModuleCat/Descent.lean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/Mathlib/Algebra/Category/ModuleCat/Descent.lean b/Mathlib/Algebra/Category/ModuleCat/Descent.lean index b1e41e5227871e..d01601e30d791b 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Descent.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Descent.lean @@ -21,6 +21,11 @@ example : extendScalars f ⋙ restrictScalars f ≅ tensorLeft ((restrictScalars f).obj (ModuleCat.of B B)) := Iso.refl _ +instance : Module.Flat A ((restrictScalars f).obj (ModuleCat.of B B)) := + -- algebraize f + let _ : Algebra A B := f.toAlgebra + (inferInstance : f.Flat).1.1 + instance : PreservesFiniteLimits <| tensorLeft ((restrictScalars f).obj (ModuleCat.of B B)) := sorry -- This is in a PR From 40861093b54f6041fbbeb587ec79750433af1029 Mon Sep 17 00:00:00 2001 From: Jack McKoen Date: Thu, 27 Jun 2024 15:01:41 -0600 Subject: [PATCH 15/29] finish Limits.lean, dualise some of Adjunction.lean --- Mathlib/CategoryTheory/Monad/Adjunction.lean | 42 +++++++++ Mathlib/CategoryTheory/Monad/Limits.lean | 97 ++++++++++++++------ 2 files changed, 110 insertions(+), 29 deletions(-) diff --git a/Mathlib/CategoryTheory/Monad/Adjunction.lean b/Mathlib/CategoryTheory/Monad/Adjunction.lean index 51a2e92e27f17e..dc2df87bd6a4ab 100644 --- a/Mathlib/CategoryTheory/Monad/Adjunction.lean +++ b/Mathlib/CategoryTheory/Monad/Adjunction.lean @@ -294,6 +294,43 @@ lemma comparison_full [R.Full] {L : C ⥤ D} (adj : L ⊣ R): end Reflective +namespace Coreflective + +instance [Coreflective R] (X : (coreflectorAdjunction R).toComonad.Coalgebra) : + IsIso ((coreflectorAdjunction R).counit.app X.A) := + ⟨⟨X.a, + ⟨by + dsimp only [Functor.id_obj] + rw [← (coreflectorAdjunction R).counit_naturality] + dsimp only [Functor.comp_obj, Adjunction.toMonad_coe] + rw [counit_obj_eq_map_counit, ← Functor.map_comp, ← Functor.map_comp] + erw [X.counit] + simp, X.counit⟩⟩⟩ + +instance comparison_essSurj [Coreflective R] : + (Comonad.comparison (coreflectorAdjunction R)).EssSurj := by + refine ⟨fun X => ⟨(coreflector R).obj X.A, ⟨?_⟩⟩⟩ + symm + refine Comonad.Coalgebra.isoMk ?_ ?_ + · exact (asIso ((coreflectorAdjunction R).counit.app X.A)).symm + dsimp only [Functor.comp_map, Comonad.comparison_obj_a, asIso_hom, Functor.comp_obj, + Comonad.comparison_obj_A, Adjunction.toComonad_coe] + rw [← cancel_epi ((coreflectorAdjunction R).counit.app X.A)] + dsimp only [Functor.id_obj, Functor.comp_obj] + simp + have := Adjunction.counit_naturality (coreflectorAdjunction R) X.a + rw [← Category.assoc] + let adj := (coreflectorAdjunction R) + change (adj.counit.app X.A ≫ X.a) ≫ R.map (adj.unit.app ((coreflector R).obj X.A)) = + R.map (adj.unit.app ((coreflector R).obj X.A)) + sorry + +lemma comparison_full [R.Full] {L : C ⥤ D} (adj : R ⊣ L): + (Comonad.comparison adj).Full where + map_surjective f := ⟨R.preimage f.f, by aesop_cat⟩ + +end Coreflective + -- It is possible to do this computably since the construction gives the data of the inverse, not -- just the existence of an inverse on each object. -- see Note [lower instance priority] @@ -305,4 +342,9 @@ instance (priority := 100) monadicOfReflective [Reflective R] : eqv := { full := Reflective.comparison_full _ } #align category_theory.monadic_of_reflective CategoryTheory.monadicOfReflective +instance (priority := 100) comonadicOfReflective [Coreflective R] : + ComonadicLeftAdjoint R where + adj := coreflectorAdjunction R + eqv := { full := Coreflective.comparison_full _ } + end CategoryTheory diff --git a/Mathlib/CategoryTheory/Monad/Limits.lean b/Mathlib/CategoryTheory/Monad/Limits.lean index 3d110d7d92634a..30749811c5778c 100644 --- a/Mathlib/CategoryTheory/Monad/Limits.lean +++ b/Mathlib/CategoryTheory/Monad/Limits.lean @@ -18,9 +18,6 @@ This is used to show that `Algebra T` has any limits which `C` has, and any coli 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. -/ @@ -406,9 +403,6 @@ noncomputable def leftAdjointPreservesTerminalOfReflective (R : D ⥤ C) [Reflec end ----------------------------------------------------------------------------------------------------- ----------------------------------------------------------------------------------------------------- - namespace Comonad variable {C : Type u₁} [Category.{v₁} C] @@ -423,13 +417,13 @@ variable (D : J ⥤ Coalgebra T) (c : Cocone (D ⋙ T.forget)) (t : IsColimit c) @[simps] def γ : D ⋙ T.forget ⟶ D ⋙ T.forget ⋙ ↑T where app j := (D.obj j).a -/-- (Impl) This new cocone is used to construct the algebra structure -/ +/-- (Impl) This new cocone is used to construct the coalgebra structure -/ @[simps! ι_app] -def newCocone : Cocone (D ⋙ T.forget) where +def newCocone : Cocone (D ⋙ forget T) where pt := T.obj c.pt ι := γ D ≫ whiskerRight c.ι (T : C ⥤ C) ≫ (Functor.constComp J _ (T : C ⥤ C)).hom -/-- The coalgebra structure which will be the apex of the new limit cone for `D`. -/ +/-- The coalgebra structure which will be the apex of the new colimit cone for `D`. -/ @[simps] def coconePoint : Coalgebra T where A := c.pt @@ -493,15 +487,6 @@ namespace ForgetCreatesLimits' -- Let's hide the implementation details in a namespace variable {D : J ⥤ Coalgebra T} (c : Cone (D ⋙ forget T)) (t : IsLimit c) --- We have a diagram D of shape J in the category of coalgebras, and we assume that we are given a --- limit for its image D ⋙ forget T under the forgetful functor, say its apex is L. --- We'll construct a limiting algebra for D, whose carrier will also be L. --- To do this, we must find a map L ⟶ TL. Since T preserves limits, TL is also a limit. --- In particular, it is a limit for the diagram `(D ⋙ forget T) ⋙ T` --- so to construct a map L ⟶ TL it suffices to show that L is the apex of a cone for this diagram. --- In other words, we need a natural transformation from const L to `(D ⋙ forget T) ⋙ T`. --- But we already know that L is the apex of a cone for the diagram `D ⋙ forget T`, so it --- suffices to give a natural transformation `((D ⋙ forget T) ⋙ T) ⟶ (D ⋙ forget T)`: /-- (Impl) The natural transformation given by the coalgebra structure maps, used to construct a cone `c` with apex `limit (D ⋙ forget T)`. @@ -519,24 +504,24 @@ def newCone : Cone ((D ⋙ forget T) ⋙ (T : C ⥤ C)) where π := c.π ≫ γ variable [PreservesLimit (D ⋙ forget T) (T : C ⥤ C)] - [PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor] + [PreservesLimit ((D ⋙ forget T) ⋙ T.toFunctor) T.toFunctor] /-- (Impl) -Define the map `λ : TL ⟶ L`, which will serve as the structure of the algebra on `L`, and +Define the map `λ : L ⟶ TL`, which will serve as the structure of the algebra on `L`, and we will show is the limiting object. We use the cone constructed by `c` and the fact that `T` preserves limits to produce this morphism. -/ abbrev lambda : c.pt ⟶ ((T : C ⥤ C).mapCone c).pt := (isLimitOfPreserves _ t).lift (newCone c) -/-- (Impl) The key property defining the map `λ : TL ⟶ L`. -/ +/-- (Impl) The key property defining the map `λ : L ⟶ TL`. -/ theorem commuting (j : J) : lambda c t ≫ (T : C ⥤ C).map (c.π.app j) = c.π.app j ≫ (D.obj j).a := (isLimitOfPreserves _ t).fac (newCone c) j variable [PreservesColimit ((D ⋙ forget T) ⋙ ↑T) (T : C ⥤ C)] /-- (Impl) -Construct the limiting algebra from the map `λ : TL ⟶ L` given by `lambda`. We are required to +Construct the limiting coalgebra from the map `λ : L ⟶ TL` given by `lambda`. We are required to show it satisfies the two coalgebra laws, which follow from the coalgebra laws for the image of `D` and our `commuting` lemma. -/ @@ -555,7 +540,7 @@ def conePoint : Coalgebra T where simp only [Functor.comp_obj, forget_obj, Functor.const_obj_obj, assoc] rw [(D.obj j).coassoc, ← assoc, ← assoc, commuting] -/-- (Impl) Construct the lifted cocone in `Coalgebra T` which will be colimiting. -/ +/-- (Impl) Construct the lifted cone in `Coalgebra T` which will be limiting. -/ @[simps] def liftedCone : Cone D where pt := conePoint c t @@ -569,7 +554,7 @@ def liftedCone : Cone D where rw [id_comp, ← c.w] rfl } -/-- (Impl) Prove that the lifted cocone is colimiting. -/ +/-- (Impl) Prove that the lifted cone is limiting. -/ @[simps] def liftedConeIsLimit : IsLimit (liftedCone c t) where lift s := @@ -617,7 +602,7 @@ noncomputable instance forgetCreatesLimitsOfShape [PreservesLimitsOfShape J (T : noncomputable instance forgetCreatesLimits [PreservesLimitsOfSize.{v, u} (T : C ⥤ C)] : CreatesLimitsOfSize.{v, u} (forget T) where CreatesLimitsOfShape := by infer_instance -/-- For `D : J ⥤ Coalgebra T`, `D ⋙ forget T` has a limit, then `D` has a limit provided colimits +/-- For `D : J ⥤ Coalgebra T`, `D ⋙ forget T` has a limit, then `D` has a limit provided limits of shape `J` are preserved by `T`. -/ theorem forget_creates_limits_of_comonad_preserves [PreservesLimitsOfShape J (T : C ⥤ C)] @@ -639,8 +624,8 @@ instance comp_comparison_hasColimit (F : J ⥤ D) (R : D ⥤ C) [ComonadicLeftAd [HasColimit (F ⋙ R)] : HasColimit (F ⋙ Comonad.comparison (comonadicAdjunction R)) := Comonad.hasColimit_of_comp_forget_hasColimit (F ⋙ Comonad.comparison (comonadicAdjunction R)) -/-- Any monadic functor creates limits. -/ -noncomputable def monadicCreatesColimits (R : D ⥤ C) [ComonadicLeftAdjoint R] : +/-- Any comonadic functor creates colimits. -/ +noncomputable def comonadicCreatesColimits (R : D ⥤ C) [ComonadicLeftAdjoint R] : CreatesColimitsOfSize.{v, u} R := createsColimitsOfNatIso (Comonad.comparisonForget (comonadicAdjunction R)) @@ -651,8 +636,6 @@ noncomputable def comonadicCreatesLimitOfPreservesLimit (R : D ⥤ C) (K : J ⥤ [ComonadicLeftAdjoint R] [PreservesLimit (K ⋙ R) (comonadicRightAdjoint R ⋙ R)] [PreservesLimit ((K ⋙ R) ⋙ comonadicRightAdjoint R ⋙ R) (comonadicRightAdjoint R ⋙ R)] : CreatesLimit K R := by - -- Porting note: It would be nice to have a variant of apply which introduces goals for missing - -- instances. letI A := Comonad.comparison (comonadicAdjunction R) letI B := Comonad.forget (Adjunction.toComonad (comonadicAdjunction R)) let i : (K ⋙ Comonad.comparison (comonadicAdjunction R)) ⋙ Comonad.forget _ ≅ K ⋙ R := @@ -689,4 +672,60 @@ noncomputable def comonadicCreatesLimitsOfPreservesLimits (R : D ⥤ C) [Comonad CreatesLimitsOfShape := comonadicCreatesLimitsOfShapeOfPreservesLimitsOfShape _ +section + +theorem hasColimit_of_coreflective (F : J ⥤ D) (R : D ⥤ C) [HasColimit (F ⋙ R)] [Coreflective R] : + HasColimit F := + haveI := comonadicCreatesColimits.{v, u} R + hasColimit_of_created F R + +/-- If `C` has colimits of shape `J` then any coreflective subcategory has colimits of shape `J`. -/ +theorem hasColimitsOfShape_of_coreflective [HasColimitsOfShape J C] (R : D ⥤ C) [Coreflective R] : + HasColimitsOfShape J D := + ⟨fun F => hasColimit_of_coreflective F R⟩ + +/-- If `C` has colimits then any coreflective subcategory has colimits. -/ +theorem hasColimits_of_coreflective (R : D ⥤ C) [HasColimitsOfSize.{v, u} C] [Coreflective R] : + HasColimitsOfSize.{v, u} D := + ⟨fun _ => hasColimitsOfShape_of_coreflective R⟩ + +/-- If `C` has limits of shape `J` then any coreflective subcategory has limits of shape `J`. -/ +theorem hasLimitsOfShape_of_coreflective (R : D ⥤ C) [Coreflective R] [HasLimitsOfShape J C] : + HasLimitsOfShape J D where + has_limit := fun F => by + let c := (comonadicRightAdjoint R).mapCone (limit.cone (F ⋙ R)) + letI : PreservesLimitsOfShape J _ := + (comonadicAdjunction R).rightAdjointPreservesLimits.1 + let t : IsLimit c := isLimitOfPreserves (comonadicRightAdjoint R) (limit.isLimit _) + apply HasLimit.mk ⟨_, (IsLimit.postcomposeHomEquiv _ _).symm t⟩ + apply + (F.rightUnitor ≪≫ (isoWhiskerLeft F ((asIso (comonadicAdjunction R).unit) : _) )).symm + +/-- If `C` has limits then any coreflective subcategory has limits. -/ +theorem hasLimits_of_coreflective (R : D ⥤ C) [Coreflective R] [HasLimitsOfSize.{v, u} C] : + HasLimitsOfSize.{v, u} D := + ⟨fun _ => hasLimitsOfShape_of_coreflective R⟩ + +/-- The coreflector always preserves terminal objects. Note this in general doesn't apply to any +other colimit. +-/ +noncomputable def rightAdjointPreservesTerminalOfCoreflective (R : D ⥤ C) [Coreflective R] : + PreservesColimitsOfShape (Discrete.{v} PEmpty) (comonadicRightAdjoint R) where + preservesColimit {K} := by + let F := Functor.empty.{v} D + letI : PreservesColimit (F ⋙ R) (comonadicRightAdjoint R) := by + constructor + intro c h + haveI : HasColimit (F ⋙ R) := ⟨⟨⟨c, h⟩⟩⟩ + haveI : HasColimit F := hasColimit_of_coreflective F R + apply isColimitChangeEmptyCocone D (colimit.isColimit F) + apply (asIso ((comonadicAdjunction R).unit.app _)).trans + apply (comonadicRightAdjoint R).mapIso + letI := comonadicCreatesColimits.{v, v} R + let A := CategoryTheory.preservesColimitOfCreatesColimitAndHasColimit F R + apply (A.preserves (colimit.isColimit F)).coconePointUniqueUpToIso h + apply preservesColimitOfIsoDiagram _ (Functor.emptyExt (F ⋙ R) _) + +end + end CategoryTheory From 8517ca830ec0a894b2d02bccd7e73e9e3947ff53 Mon Sep 17 00:00:00 2001 From: Dagur Asgeirsson Date: Tue, 27 Aug 2024 12:46:43 +0000 Subject: [PATCH 16/29] Update Adjunction.lean --- Mathlib/CategoryTheory/Monad/Adjunction.lean | 387 +++++++++++++++++++ 1 file changed, 387 insertions(+) diff --git a/Mathlib/CategoryTheory/Monad/Adjunction.lean b/Mathlib/CategoryTheory/Monad/Adjunction.lean index e69de29bb2d1d6..30ed3a870df5fd 100644 --- a/Mathlib/CategoryTheory/Monad/Adjunction.lean +++ b/Mathlib/CategoryTheory/Monad/Adjunction.lean @@ -0,0 +1,387 @@ +/- +Copyright (c) 2019 Scott Morrison. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Scott Morrison, Bhavik Mehta +-/ +import Mathlib.CategoryTheory.Adjunction.Reflective +import Mathlib.CategoryTheory.Monad.Algebra + +/-! +# Adjunctions and (co)monads + +We develop the basic relationship between adjunctions and (co)monads. + +Given an adjunction `h : L ⊣ R`, we have `h.toMonad : Monad C` and `h.toComonad : Comonad D`. +We then have +`Monad.comparison (h : L ⊣ R) : D ⥤ h.toMonad.algebra` +sending `Y : D` to the Eilenberg-Moore algebra for `L ⋙ R` with underlying object `R.obj X`, +and dually `Comonad.comparison`. + +We say `R : D ⥤ C` is `MonadicRightAdjoint`, if it is a right adjoint and its `Monad.comparison` +is an equivalence of categories. (Similarly for `ComonadicLeftAdjoint`.) + +Finally we prove that reflective functors are `MonadicRightAdjoint` and coreflective functors are +`ComonadicLeftAdjoint`. +-/ + + +namespace CategoryTheory + +open Category + +universe v₁ v₂ u₁ u₂ + +-- morphism levels before object levels. See note [category_theory universes]. +variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D] +variable {L : C ⥤ D} {R : D ⥤ C} + +namespace Adjunction + +/-- For a pair of functors `L : C ⥤ D`, `R : D ⥤ C`, an adjunction `h : L ⊣ R` induces a monad on +the category `C`. +-/ +-- Porting note: Specifying simps projections manually to match mathlib3 behavior. +@[simps! coe η μ] +def toMonad (h : L ⊣ R) : Monad C where + toFunctor := L ⋙ R + η := h.unit + μ := whiskerRight (whiskerLeft L h.counit) R + assoc X := by + dsimp + rw [← R.map_comp] + simp + right_unit X := by + dsimp + rw [← R.map_comp] + simp + +/-- For a pair of functors `L : C ⥤ D`, `R : D ⥤ C`, an adjunction `h : L ⊣ R` induces a comonad on +the category `D`. +-/ +-- Porting note: Specifying simps projections manually to match mathlib3 behavior. +@[simps coe ε δ] +def toComonad (h : L ⊣ R) : Comonad D where + toFunctor := R ⋙ L + ε := h.counit + δ := whiskerRight (whiskerLeft R h.unit) L + coassoc X := by + dsimp + rw [← L.map_comp] + simp + right_counit X := by + dsimp + rw [← L.map_comp] + simp + +/-- The monad induced by the Eilenberg-Moore adjunction is the original monad. -/ +@[simps!] +def adjToMonadIso (T : Monad C) : T.adj.toMonad ≅ T := + MonadIso.mk (NatIso.ofComponents fun X => Iso.refl _) + +/-- The comonad induced by the Eilenberg-Moore adjunction is the original comonad. -/ +@[simps!] +def adjToComonadIso (G : Comonad C) : G.adj.toComonad ≅ G := + ComonadIso.mk (NatIso.ofComponents fun X => Iso.refl _) + +/-- +Given an adjunction `L ⊣ R`, if `L ⋙ R` is abstractly isomorphic to the identity functor, then the +unit is an isomorphism. +-/ +def unitAsIsoOfIso (adj : L ⊣ R) (i : L ⋙ R ≅ 𝟭 C) : 𝟭 C ≅ L ⋙ R where + hom := adj.unit + inv := i.hom ≫ (adj.toMonad.transport i).μ + hom_inv_id := by + rw [← assoc] + ext X + exact (adj.toMonad.transport i).right_unit X + inv_hom_id := by + rw [assoc, ← Iso.eq_inv_comp, comp_id, ← id_comp i.inv, Iso.eq_comp_inv, assoc, + NatTrans.id_comm] + ext X + exact (adj.toMonad.transport i).right_unit X + +lemma isIso_unit_of_iso (adj : L ⊣ R) (i : L ⋙ R ≅ 𝟭 C) : IsIso adj.unit := + (inferInstanceAs (IsIso (unitAsIsoOfIso adj i).hom)) + +/-- +Given an adjunction `L ⊣ R`, if `L ⋙ R` is isomorphic to the identity functor, then `L` is +fully faithful. +-/ +noncomputable def fullyFaithfulLOfCompIsoId (adj : L ⊣ R) (i : L ⋙ R ≅ 𝟭 C) : L.FullyFaithful := + haveI := adj.isIso_unit_of_iso i + adj.fullyFaithfulLOfIsIsoUnit + +/-- +Given an adjunction `L ⊣ R`, if `R ⋙ L` is abstractly isomorphic to the identity functor, then the +counit is an isomorphism. +-/ +def counitAsIsoOfIso (adj : L ⊣ R) (j : R ⋙ L ≅ 𝟭 D) : R ⋙ L ≅ 𝟭 D where + hom := adj.counit + inv := (adj.toComonad.transport j).δ ≫ j.inv + hom_inv_id := by + rw [← assoc, Iso.comp_inv_eq, id_comp, ← comp_id j.hom, ← Iso.inv_comp_eq, ← assoc, + NatTrans.id_comm] + ext X + exact (adj.toComonad.transport j).right_counit X + inv_hom_id := by + rw [assoc] + ext X + exact (adj.toComonad.transport j).right_counit X + +lemma isIso_counit_of_iso (adj : L ⊣ R) (j : R ⋙ L ≅ 𝟭 D) : IsIso adj.counit := + inferInstanceAs (IsIso (counitAsIsoOfIso adj j).hom) + +/-- +Given an adjunction `L ⊣ R`, if `R ⋙ L` is isomorphic to the identity functor, then `R` is +fully faithful. +-/ +noncomputable def fullyFaithfulROfCompIsoId (adj : L ⊣ R) (j : R ⋙ L ≅ 𝟭 D) : R.FullyFaithful := + haveI := adj.isIso_counit_of_iso j + adj.fullyFaithfulROfIsIsoCounit + +end Adjunction + +/-- Given any adjunction `L ⊣ R`, there is a comparison functor `CategoryTheory.Monad.comparison R` +sending objects `Y : D` to Eilenberg-Moore algebras for `L ⋙ R` with underlying object `R.obj X`. + +We later show that this is full when `R` is full, faithful when `R` is faithful, +and essentially surjective when `R` is reflective. +-/ +@[simps] +def Monad.comparison (h : L ⊣ R) : D ⥤ h.toMonad.Algebra where + obj X := + { A := R.obj X + a := R.map (h.counit.app X) + assoc := by + dsimp + rw [← R.map_comp, ← Adjunction.counit_naturality, R.map_comp] } + map f := + { f := R.map f + h := by + dsimp + rw [← R.map_comp, Adjunction.counit_naturality, R.map_comp] } + +/-- The underlying object of `(Monad.comparison R).obj X` is just `R.obj X`. +-/ +@[simps] +def Monad.comparisonForget (h : L ⊣ R) : Monad.comparison h ⋙ h.toMonad.forget ≅ R where + hom := { app := fun X => 𝟙 _ } + inv := { app := fun X => 𝟙 _ } + +theorem Monad.left_comparison (h : L ⊣ R) : L ⋙ Monad.comparison h = h.toMonad.free := + rfl + +instance [R.Faithful] (h : L ⊣ R) : (Monad.comparison h).Faithful where + map_injective {_ _} _ _ w := R.map_injective (congr_arg Monad.Algebra.Hom.f w : _) + +instance (T : Monad C) : (Monad.comparison T.adj).Full where + map_surjective {_ _} f := ⟨⟨f.f, by simpa using f.h⟩, rfl⟩ + +instance (T : Monad C) : (Monad.comparison T.adj).EssSurj where + mem_essImage X := + ⟨{ A := X.A + a := X.a + unit := by simpa using X.unit + assoc := by simpa using X.assoc }, + ⟨Monad.Algebra.isoMk (Iso.refl _)⟩⟩ + +/-- +Given any adjunction `L ⊣ R`, there is a comparison functor `CategoryTheory.Comonad.comparison L` +sending objects `X : C` to Eilenberg-Moore coalgebras for `L ⋙ R` with underlying object +`L.obj X`. +-/ +@[simps] +def Comonad.comparison (h : L ⊣ R) : C ⥤ h.toComonad.Coalgebra where + obj X := + { A := L.obj X + a := L.map (h.unit.app X) + coassoc := by + dsimp + rw [← L.map_comp, ← Adjunction.unit_naturality, L.map_comp] } + map f := + { f := L.map f + h := by + dsimp + rw [← L.map_comp] + simp } + +/-- The underlying object of `(Comonad.comparison L).obj X` is just `L.obj X`. +-/ +@[simps] +def Comonad.comparisonForget {L : C ⥤ D} {R : D ⥤ C} (h : L ⊣ R) : + Comonad.comparison h ⋙ h.toComonad.forget ≅ L where + hom := { app := fun X => 𝟙 _ } + inv := { app := fun X => 𝟙 _ } + +theorem Comonad.left_comparison (h : L ⊣ R) : R ⋙ Comonad.comparison h = h.toComonad.cofree := + rfl + +instance Comonad.comparison_faithful_of_faithful [L.Faithful] (h : L ⊣ R) : + (Comonad.comparison h).Faithful where + map_injective {_ _} _ _ w := L.map_injective (congr_arg Comonad.Coalgebra.Hom.f w : _) + +instance (G : Comonad C) : (Comonad.comparison G.adj).Full where + map_surjective f := ⟨⟨f.f, by simpa using f.h⟩, rfl⟩ + +instance (G : Comonad C) : (Comonad.comparison G.adj).EssSurj where + mem_essImage X := + ⟨{ A := X.A + a := X.a + counit := by simpa using X.counit + coassoc := by simpa using X.coassoc }, + ⟨Comonad.Coalgebra.isoMk (Iso.refl _)⟩⟩ + +/-- A right adjoint functor `R : D ⥤ C` is *monadic* if the comparison functor `Monad.comparison R` +from `D` to the category of Eilenberg-Moore algebras for the adjunction is an equivalence. +-/ +class MonadicRightAdjoint (R : D ⥤ C) where + /-- a choice of left adjoint for `R` -/ + L : C ⥤ D + /-- `R` is a right adjoint -/ + adj : L ⊣ R + eqv : (Monad.comparison adj).IsEquivalence + +/-- The left adjoint functor to `R` given by `[MonadicRightAdjoint R]`. -/ +def monadicLeftAdjoint (R : D ⥤ C) [MonadicRightAdjoint R] : C ⥤ D := + MonadicRightAdjoint.L (R := R) + +/-- The adjunction `monadicLeftAdjoint R ⊣ R` given by `[MonadicRightAdjoint R]`. -/ +def monadicAdjunction (R : D ⥤ C) [MonadicRightAdjoint R] : + monadicLeftAdjoint R ⊣ R := + MonadicRightAdjoint.adj + +instance (R : D ⥤ C) [MonadicRightAdjoint R] : + (Monad.comparison (monadicAdjunction R)).IsEquivalence := + MonadicRightAdjoint.eqv + +instance (R : D ⥤ C) [MonadicRightAdjoint R] : R.IsRightAdjoint := + (monadicAdjunction R).isRightAdjoint + +noncomputable instance (T : Monad C) : MonadicRightAdjoint T.forget where + adj := T.adj + eqv := { } + +/-- +A left adjoint functor `L : C ⥤ D` is *comonadic* if the comparison functor `Comonad.comparison L` +from `C` to the category of Eilenberg-Moore algebras for the adjunction is an equivalence. +-/ +class ComonadicLeftAdjoint (L : C ⥤ D) where + /-- a choice of right adjoint for `L` -/ + R : D ⥤ C + /-- `L` is a left adjoint -/ + adj : L ⊣ R + eqv : (Comonad.comparison adj).IsEquivalence + +/-- The right adjoint functor to `L` given by `[ComonadicLeftAdjoint L]`. -/ +def comonadicRightAdjoint (L : C ⥤ D) [ComonadicLeftAdjoint L] : D ⥤ C := + ComonadicLeftAdjoint.R (L := L) + +/-- The adjunction `L ⊣ comonadicRightAdjoint L` given by `[ComonadicLeftAdjoint L]`. -/ +def comonadicAdjunction (L : C ⥤ D) [ComonadicLeftAdjoint L] : + L ⊣ comonadicRightAdjoint L := + ComonadicLeftAdjoint.adj + +instance (L : C ⥤ D) [ComonadicLeftAdjoint L] : + (Comonad.comparison (comonadicAdjunction L)).IsEquivalence := + ComonadicLeftAdjoint.eqv + +instance (L : C ⥤ D) [ComonadicLeftAdjoint L] : L.IsLeftAdjoint := + (comonadicAdjunction L).isLeftAdjoint + +noncomputable instance (G : Comonad C) : ComonadicLeftAdjoint G.forget where + adj := G.adj + eqv := { } + +-- TODO: This holds more generally for idempotent adjunctions, not just reflective adjunctions. +instance μ_iso_of_reflective [Reflective R] : IsIso (reflectorAdjunction R).toMonad.μ := by + dsimp + infer_instance + +instance δ_iso_of_coreflective [Coreflective R] : IsIso (coreflectorAdjunction R).toComonad.δ := by + dsimp + infer_instance + +attribute [instance] MonadicRightAdjoint.eqv +attribute [instance] ComonadicLeftAdjoint.eqv + +namespace Reflective + +instance [Reflective R] (X : (reflectorAdjunction R).toMonad.Algebra) : + IsIso ((reflectorAdjunction R).unit.app X.A) := + ⟨⟨X.a, + ⟨X.unit, by + dsimp only [Functor.id_obj] + rw [← (reflectorAdjunction R).unit_naturality] + dsimp only [Functor.comp_obj, Adjunction.toMonad_coe] + rw [unit_obj_eq_map_unit, ← Functor.map_comp, ← Functor.map_comp] + erw [X.unit] + simp⟩⟩⟩ + +instance comparison_essSurj [Reflective R] : + (Monad.comparison (reflectorAdjunction R)).EssSurj := by + refine ⟨fun X => ⟨(reflector R).obj X.A, ⟨?_⟩⟩⟩ + symm + refine Monad.Algebra.isoMk ?_ ?_ + · exact asIso ((reflectorAdjunction R).unit.app X.A) + dsimp only [Functor.comp_map, Monad.comparison_obj_a, asIso_hom, Functor.comp_obj, + Monad.comparison_obj_A, Adjunction.toMonad_coe] + rw [← cancel_epi ((reflectorAdjunction R).unit.app X.A)] + dsimp only [Functor.id_obj, Functor.comp_obj] + rw [Adjunction.unit_naturality_assoc, + Adjunction.right_triangle_components, comp_id] + apply (X.unit_assoc _).symm + +lemma comparison_full [R.Full] {L : C ⥤ D} (adj : L ⊣ R) : + (Monad.comparison adj).Full where + map_surjective f := ⟨R.preimage f.f, by aesop_cat⟩ + +end Reflective + +namespace Coreflective + +instance [Coreflective R] (X : (coreflectorAdjunction R).toComonad.Coalgebra) : + IsIso ((coreflectorAdjunction R).counit.app X.A) := + ⟨⟨X.a, + ⟨by + dsimp only [Functor.id_obj] + rw [← (coreflectorAdjunction R).counit_naturality] + dsimp only [Functor.comp_obj, Adjunction.toMonad_coe] + rw [counit_obj_eq_map_counit, ← Functor.map_comp, ← Functor.map_comp] + erw [X.counit] + simp, X.counit⟩⟩⟩ + +instance comparison_essSurj [Coreflective R] : + (Comonad.comparison (coreflectorAdjunction R)).EssSurj := by + refine ⟨fun X => ⟨(coreflector R).obj X.A, ⟨?_⟩⟩⟩ + refine Comonad.Coalgebra.isoMk ?_ ?_ + · exact (asIso ((coreflectorAdjunction R).counit.app X.A)) + rw [← cancel_mono ((coreflectorAdjunction R).counit.app X.A)] + simp only [Adjunction.counit_naturality, Functor.comp_obj, Functor.id_obj, + Adjunction.left_triangle_components_assoc, assoc] + erw [X.counit] + simp + +lemma comparison_full [R.Full] {L : C ⥤ D} (adj : R ⊣ L) : + (Comonad.comparison adj).Full where + map_surjective f := ⟨R.preimage f.f, by aesop_cat⟩ + +end Coreflective + +-- It is possible to do this computably since the construction gives the data of the inverse, not +-- just the existence of an inverse on each object. +-- see Note [lower instance priority] +/-- Any reflective inclusion has a monadic right adjoint. + cf Prop 5.3.3 of [Riehl][riehl2017] -/ +instance (priority := 100) monadicOfReflective [Reflective R] : + MonadicRightAdjoint R where + adj := reflectorAdjunction R + eqv := { full := Reflective.comparison_full _ } + +/-- Any coreflective inclusion has a comonadic left adjoint. + cf Dual statement of Prop 5.3.3 of [Riehl][riehl2017] -/ +instance (priority := 100) comonadicOfCoreflective [Coreflective R] : + ComonadicLeftAdjoint R where + adj := coreflectorAdjunction R + eqv := { full := Coreflective.comparison_full _ } + +end CategoryTheory From 8943aa3f6516d3ae0c3f040203e3fdf634ef7a4f Mon Sep 17 00:00:00 2001 From: Dagur Asgeirsson Date: Tue, 27 Aug 2024 12:48:10 +0000 Subject: [PATCH 17/29] Update Limits.lean --- Mathlib/CategoryTheory/Monad/Limits.lean | 324 ++++++++++++++++++++++- 1 file changed, 323 insertions(+), 1 deletion(-) diff --git a/Mathlib/CategoryTheory/Monad/Limits.lean b/Mathlib/CategoryTheory/Monad/Limits.lean index 3ae6bdd0044faf..f447048e82490b 100644 --- a/Mathlib/CategoryTheory/Monad/Limits.lean +++ b/Mathlib/CategoryTheory/Monad/Limits.lean @@ -373,7 +373,329 @@ noncomputable def leftAdjointPreservesTerminalOfReflective (R : D ⥤ C) [Reflec let A := CategoryTheory.preservesLimitOfCreatesLimitAndHasLimit F R apply (A.preserves (limit.isLimit F)).conePointUniqueUpToIso h apply preservesLimitOfIsoDiagram _ (Functor.emptyExt (F ⋙ R) _) -#align category_theory.left_adjoint_preserves_terminal_of_reflective CategoryTheory.leftAdjointPreservesTerminalOfReflective + +end + +-- We dualise all of the above for comonads. +namespace Comonad + +variable {T : Comonad C} + +namespace ForgetCreatesColimits' + +variable (D : J ⥤ Coalgebra T) (c : Cocone (D ⋙ T.forget)) (t : IsColimit c) + +/-- (Impl) The natural transformation used to define the new cocone -/ +@[simps] +def γ : D ⋙ T.forget ⟶ D ⋙ T.forget ⋙ ↑T where app j := (D.obj j).a + +/-- (Impl) This new cocone is used to construct the coalgebra structure -/ +@[simps! ι_app] +def newCocone : Cocone (D ⋙ forget T) where + pt := T.obj c.pt + ι := γ D ≫ whiskerRight c.ι (T : C ⥤ C) ≫ (Functor.constComp J _ (T : C ⥤ C)).hom + +/-- The coalgebra structure which will be the point of the new colimit cone for `D`. -/ +@[simps] +def coconePoint : Coalgebra T where + A := c.pt + a := t.desc (newCocone D c) + counit := t.hom_ext fun j ↦ by + simp only [Functor.comp_obj, forget_obj, Functor.id_obj, Functor.const_obj_obj, + IsColimit.fac_assoc, newCocone_ι_app, assoc, NatTrans.naturality, Functor.id_map, comp_id] + rw [← Category.assoc, (D.obj j).counit, Category.id_comp] + coassoc := t.hom_ext fun j ↦ by + simp only [Functor.comp_obj, forget_obj, Functor.const_obj_obj, IsColimit.fac_assoc, + newCocone_ι_app, assoc, NatTrans.naturality, Functor.comp_map] + rw [← Category.assoc, (D.obj j).coassoc, ← Functor.map_comp, t.fac (newCocone D c) j, + newCocone_ι_app, Functor.map_comp, assoc] + +/-- (Impl) Construct the lifted cocone in `Coalgebra T` which will be colimiting. -/ +@[simps] +def liftedCocone : Cocone D where + pt := coconePoint D c t + ι := + { app := fun j => { f := c.ι.app j } + naturality := fun X Y f => by + ext1 + dsimp + erw [c.w f] + simp } + +/-- (Impl) Prove that the lifted cocone is colimiting. -/ +@[simps] +def liftedCoconeIsColimit : IsColimit (liftedCocone D c t) where + desc s := + { f := t.desc ((forget T).mapCocone s) + h := + t.hom_ext fun j => by + dsimp + rw [← Category.assoc, ← Category.assoc, t.fac, newCocone_ι_app, t.fac, + Functor.mapCocone_ι_app, Category.assoc, ← Functor.map_comp, t.fac] + apply (s.ι.app j).h } + uniq s m J := by + ext1 + apply t.hom_ext + intro j + simpa [t.fac ((forget T).mapCocone s) j] using congr_arg Coalgebra.Hom.f (J j) + +end ForgetCreatesColimits' + +-- Dual to theorem 5.6.5 from [Riehl][riehl2017] +/-- The forgetful functor from the Eilenberg-Moore category creates colimits. -/ +noncomputable instance forgetCreatesColimit : CreatesColimitsOfSize (forget T) where + CreatesColimitsOfShape := { + CreatesColimit := fun {D} => + createsColimitOfReflectsIso fun c t => + { liftedCocone := ForgetCreatesColimits'.liftedCocone D c t + validLift := Cocones.ext (Iso.refl _) fun _ => (comp_id _) + makesColimit := ForgetCreatesColimits'.liftedCoconeIsColimit _ _ _ } } + +/-- If `D ⋙ forget T` has a colimit, then `D` has a colimit. -/ +theorem hasColimit_of_comp_forget_hasColimit (D : J ⥤ Coalgebra T) [HasColimit (D ⋙ forget T)] : + HasColimit D := + hasColimit_of_created D (forget T) + +namespace ForgetCreatesLimits' + +-- Let's hide the implementation details in a namespace +variable {D : J ⥤ Coalgebra T} (c : Cone (D ⋙ forget T)) (t : IsLimit c) + +/-- (Impl) +The natural transformation given by the coalgebra structure maps, used to construct a cone `c` with +point `limit (D ⋙ forget T)`. + -/ +@[simps] +def γ : D ⋙ forget T ⟶ (D ⋙ forget T) ⋙ ↑T where app j := (D.obj j).a + +/-- (Impl) +A cone for the diagram `(D ⋙ forget T) ⋙ T` found by composing the natural transformation `γ` +with the limiting cone for `D ⋙ forget T`. +-/ +@[simps] +def newCone : Cone ((D ⋙ forget T) ⋙ (T : C ⥤ C)) where + pt := c.pt + π := c.π ≫ γ + +variable [PreservesLimit (D ⋙ forget T) (T : C ⥤ C)] + +/-- (Impl) +Define the map `λ : L ⟶ TL`, which will serve as the structure of the algebra on `L`, and +we will show is the limiting object. We use the cone constructed by `c` and the fact that +`T` preserves limits to produce this morphism. +-/ +abbrev lambda : c.pt ⟶ ((T : C ⥤ C).mapCone c).pt := + (isLimitOfPreserves _ t).lift (newCone c) + +/-- (Impl) The key property defining the map `λ : L ⟶ TL`. -/ +theorem commuting (j : J) : lambda c t ≫ (T : C ⥤ C).map (c.π.app j) = c.π.app j ≫ (D.obj j).a := + (isLimitOfPreserves _ t).fac (newCone c) j + +variable [PreservesLimit ((D ⋙ forget T) ⋙ T.toFunctor) T.toFunctor] +variable [PreservesColimit ((D ⋙ forget T) ⋙ ↑T) (T : C ⥤ C)] + +/-- (Impl) +Construct the limiting coalgebra from the map `λ : L ⟶ TL` given by `lambda`. We are required to +show it satisfies the two coalgebra laws, which follow from the coalgebra laws for the image of `D` +and our `commuting` lemma. +-/ +@[simps] +def conePoint : Coalgebra T where + A := c.pt + a := lambda c t + counit := t.hom_ext fun j ↦ by + rw [assoc, ← show _ = _ ≫ c.π.app j from T.ε.naturality _, ← assoc, commuting, assoc] + simp [Coalgebra.counit (D.obj j)] + coassoc := by + refine (isLimitOfPreserves _ (isLimitOfPreserves _ t)).hom_ext fun j => ?_ + rw [Functor.mapCone_π_app, Functor.mapCone_π_app, assoc, + ← show _ = _ ≫ T.map (T.map _) from T.δ.naturality _, assoc, ← Functor.map_comp, commuting, + Functor.map_comp, ← assoc, commuting] + simp only [Functor.comp_obj, forget_obj, Functor.const_obj_obj, assoc] + rw [(D.obj j).coassoc, ← assoc, ← assoc, commuting] + +/-- (Impl) Construct the lifted cone in `Coalgebra T` which will be limiting. -/ +@[simps] +def liftedCone : Cone D where + pt := conePoint c t + π := + { app := fun j => + { f := c.π.app j + h := commuting _ _ _ } + naturality := fun A B f => by + ext1 + dsimp + rw [id_comp, ← c.w] + rfl } + +/-- (Impl) Prove that the lifted cone is limiting. -/ +@[simps] +def liftedConeIsLimit : IsLimit (liftedCone c t) where + lift s := + { f := t.lift ((forget T).mapCone s) + h := + (isLimitOfPreserves (T : C ⥤ C) t).hom_ext fun j => by + dsimp + rw [Category.assoc, ← t.fac, Category.assoc, t.fac, commuting, ← assoc, ← assoc, t.fac, + assoc, ← Functor.map_comp, t.fac] + exact (s.π.app j).h } + uniq s m J := by + ext1 + apply t.hom_ext + intro j + simpa using congr_arg Coalgebra.Hom.f (J j) + +end ForgetCreatesLimits' + +open ForgetCreatesLimits' + +-- TODO: the converse of this is true as well +/-- The forgetful functor from the Eilenberg-Moore category for a comonad creates any limit +which the comonad itself preserves. +-/ +noncomputable instance forgetCreatesLimit (D : J ⥤ Coalgebra T) + [PreservesLimit (D ⋙ forget T) (T : C ⥤ C)] + [PreservesLimit ((D ⋙ forget T) ⋙ ↑T) (T : C ⥤ C)] : CreatesLimit D (forget T) := + createsLimitOfReflectsIso fun c t => + { liftedCone := + { pt := conePoint c t + π := + { app := fun j => + { f := c.π.app j + h := commuting _ _ _ } + naturality := fun A B f => by + ext1 + dsimp + erw [id_comp, c.w] } } + validLift := Cones.ext (Iso.refl _) + makesLimit := liftedConeIsLimit _ _ } + +noncomputable instance forgetCreatesLimitsOfShape [PreservesLimitsOfShape J (T : C ⥤ C)] : + CreatesLimitsOfShape J (forget T) where CreatesLimit := by infer_instance + +noncomputable instance forgetCreatesLimits [PreservesLimitsOfSize.{v, u} (T : C ⥤ C)] : + CreatesLimitsOfSize.{v, u} (forget T) where CreatesLimitsOfShape := by infer_instance + +/-- For `D : J ⥤ Coalgebra T`, `D ⋙ forget T` has a limit, then `D` has a limit provided limits +of shape `J` are preserved by `T`. +-/ +theorem forget_creates_limits_of_comonad_preserves [PreservesLimitsOfShape J (T : C ⥤ C)] + (D : J ⥤ Coalgebra T) [HasLimit (D ⋙ forget T)] : HasLimit D := + hasLimit_of_created D (forget T) + +end Comonad + +instance comp_comparison_forget_hasColimit (F : J ⥤ D) (R : D ⥤ C) [ComonadicLeftAdjoint R] + [HasColimit (F ⋙ R)] : + HasColimit ((F ⋙ Comonad.comparison (comonadicAdjunction R)) ⋙ Comonad.forget _) := + @hasColimitOfIso _ _ _ _ (F ⋙ R) _ _ + (isoWhiskerLeft F (Comonad.comparisonForget (comonadicAdjunction R)).symm) + +instance comp_comparison_hasColimit (F : J ⥤ D) (R : D ⥤ C) [ComonadicLeftAdjoint R] + [HasColimit (F ⋙ R)] : HasColimit (F ⋙ Comonad.comparison (comonadicAdjunction R)) := + Comonad.hasColimit_of_comp_forget_hasColimit (F ⋙ Comonad.comparison (comonadicAdjunction R)) + +/-- Any comonadic functor creates colimits. -/ +noncomputable def comonadicCreatesColimits (R : D ⥤ C) [ComonadicLeftAdjoint R] : + CreatesColimitsOfSize.{v, u} R := + createsColimitsOfNatIso (Comonad.comparisonForget (comonadicAdjunction R)) + +/-- The forgetful functor from the Eilenberg-Moore category for a comonad creates any limit +which the comonad itself preserves. +-/ +noncomputable def comonadicCreatesLimitOfPreservesLimit (R : D ⥤ C) (K : J ⥤ D) + [ComonadicLeftAdjoint R] [PreservesLimit (K ⋙ R) (comonadicRightAdjoint R ⋙ R)] + [PreservesLimit ((K ⋙ R) ⋙ comonadicRightAdjoint R ⋙ R) (comonadicRightAdjoint R ⋙ R)] : + CreatesLimit K R := by + letI A := Comonad.comparison (comonadicAdjunction R) + letI B := Comonad.forget (Adjunction.toComonad (comonadicAdjunction R)) + let i : (K ⋙ Comonad.comparison (comonadicAdjunction R)) ⋙ Comonad.forget _ ≅ K ⋙ R := + Functor.associator _ _ _ ≪≫ + isoWhiskerLeft K (Comonad.comparisonForget (comonadicAdjunction R)) + letI : PreservesLimit ((K ⋙ A) ⋙ Comonad.forget + (Adjunction.toComonad (comonadicAdjunction R))) + (Adjunction.toComonad (comonadicAdjunction R)).toFunctor := by + dsimp + exact preservesLimitOfIsoDiagram _ i.symm + letI : PreservesLimit + (((K ⋙ A) ⋙ Comonad.forget (Adjunction.toComonad (comonadicAdjunction R))) ⋙ + (Adjunction.toComonad (comonadicAdjunction R)).toFunctor) + (Adjunction.toComonad (comonadicAdjunction R)).toFunctor := by + dsimp + exact preservesLimitOfIsoDiagram _ (isoWhiskerRight i (comonadicRightAdjoint R ⋙ R)).symm + letI : CreatesLimit (K ⋙ A) B := CategoryTheory.Comonad.forgetCreatesLimit _ + letI : CreatesLimit K (A ⋙ B) := CategoryTheory.compCreatesLimit _ _ + let e := Comonad.comparisonForget (comonadicAdjunction R) + apply createsLimitOfNatIso e + +/-- A comonadic functor creates any limits of shapes it preserves. -/ +noncomputable def comonadicCreatesLimitsOfShapeOfPreservesLimitsOfShape (R : D ⥤ C) + [ComonadicLeftAdjoint R] [PreservesLimitsOfShape J R] : CreatesLimitsOfShape J R := + letI : PreservesLimitsOfShape J (comonadicRightAdjoint R) := by + apply (Adjunction.rightAdjointPreservesLimits (comonadicAdjunction R)).1 + letI : PreservesLimitsOfShape J (comonadicRightAdjoint R ⋙ R) := by + apply CategoryTheory.Limits.compPreservesLimitsOfShape _ _ + ⟨comonadicCreatesLimitOfPreservesLimit _ _⟩ + +/-- A comonadic functor creates limits if it preserves limits. -/ +noncomputable def comonadicCreatesLimitsOfPreservesLimits (R : D ⥤ C) [ComonadicLeftAdjoint R] + [PreservesLimitsOfSize.{v, u} R] : CreatesLimitsOfSize.{v, u} R where + CreatesLimitsOfShape := + comonadicCreatesLimitsOfShapeOfPreservesLimitsOfShape _ + +section + +theorem hasColimit_of_coreflective (F : J ⥤ D) (R : D ⥤ C) [HasColimit (F ⋙ R)] [Coreflective R] : + HasColimit F := + haveI := comonadicCreatesColimits.{v, u} R + hasColimit_of_created F R + +/-- If `C` has colimits of shape `J` then any coreflective subcategory has colimits of shape `J`. -/ +theorem hasColimitsOfShape_of_coreflective [HasColimitsOfShape J C] (R : D ⥤ C) [Coreflective R] : + HasColimitsOfShape J D := + ⟨fun F => hasColimit_of_coreflective F R⟩ + +/-- If `C` has colimits then any coreflective subcategory has colimits. -/ +theorem hasColimits_of_coreflective (R : D ⥤ C) [HasColimitsOfSize.{v, u} C] [Coreflective R] : + HasColimitsOfSize.{v, u} D := + ⟨fun _ => hasColimitsOfShape_of_coreflective R⟩ + +/-- If `C` has limits of shape `J` then any coreflective subcategory has limits of shape `J`. -/ +theorem hasLimitsOfShape_of_coreflective (R : D ⥤ C) [Coreflective R] [HasLimitsOfShape J C] : + HasLimitsOfShape J D where + has_limit := fun F => by + let c := (comonadicRightAdjoint R).mapCone (limit.cone (F ⋙ R)) + letI : PreservesLimitsOfShape J _ := + (comonadicAdjunction R).rightAdjointPreservesLimits.1 + let t : IsLimit c := isLimitOfPreserves (comonadicRightAdjoint R) (limit.isLimit _) + apply HasLimit.mk ⟨_, (IsLimit.postcomposeHomEquiv _ _).symm t⟩ + apply + (F.rightUnitor ≪≫ (isoWhiskerLeft F ((asIso (comonadicAdjunction R).unit) : _) )).symm + +/-- If `C` has limits then any coreflective subcategory has limits. -/ +theorem hasLimits_of_coreflective (R : D ⥤ C) [Coreflective R] [HasLimitsOfSize.{v, u} C] : + HasLimitsOfSize.{v, u} D := + ⟨fun _ => hasLimitsOfShape_of_coreflective R⟩ + +/-- The coreflector always preserves initial objects. Note this in general doesn't apply to any +other colimit. +-/ +noncomputable def rightAdjointPreservesInitialOfCoreflective (R : D ⥤ C) [Coreflective R] : + PreservesColimitsOfShape (Discrete.{v} PEmpty) (comonadicRightAdjoint R) where + preservesColimit {K} := by + let F := Functor.empty.{v} D + letI : PreservesColimit (F ⋙ R) (comonadicRightAdjoint R) := by + constructor + intro c h + haveI : HasColimit (F ⋙ R) := ⟨⟨⟨c, h⟩⟩⟩ + haveI : HasColimit F := hasColimit_of_coreflective F R + apply isColimitChangeEmptyCocone D (colimit.isColimit F) + apply (asIso ((comonadicAdjunction R).unit.app _)).trans + apply (comonadicRightAdjoint R).mapIso + letI := comonadicCreatesColimits.{v, v} R + let A := CategoryTheory.preservesColimitOfCreatesColimitAndHasColimit F R + apply (A.preserves (colimit.isColimit F)).coconePointUniqueUpToIso h + apply preservesColimitOfIsoDiagram _ (Functor.emptyExt (F ⋙ R) _) end From 6173d2362c2919a6ce276825e07cb8587a255c58 Mon Sep 17 00:00:00 2001 From: dagurtomas Date: Tue, 27 Aug 2024 12:51:27 +0000 Subject: [PATCH 18/29] try fixing diff --- Mathlib/CategoryTheory/Monad/Adjunction.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/CategoryTheory/Monad/Adjunction.lean b/Mathlib/CategoryTheory/Monad/Adjunction.lean index 30ed3a870df5fd..94a38e039c6c3e 100644 --- a/Mathlib/CategoryTheory/Monad/Adjunction.lean +++ b/Mathlib/CategoryTheory/Monad/Adjunction.lean @@ -24,7 +24,7 @@ Finally we prove that reflective functors are `MonadicRightAdjoint` and coreflec `ComonadicLeftAdjoint`. -/ - +-- test namespace CategoryTheory open Category From c98bde4a040956da9fbe678bafa99eb4a3d13e02 Mon Sep 17 00:00:00 2001 From: dagurtomas Date: Tue, 27 Aug 2024 12:52:02 +0000 Subject: [PATCH 19/29] again --- Mathlib/CategoryTheory/Monad/Adjunction.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/CategoryTheory/Monad/Adjunction.lean b/Mathlib/CategoryTheory/Monad/Adjunction.lean index 94a38e039c6c3e..30ed3a870df5fd 100644 --- a/Mathlib/CategoryTheory/Monad/Adjunction.lean +++ b/Mathlib/CategoryTheory/Monad/Adjunction.lean @@ -24,7 +24,7 @@ Finally we prove that reflective functors are `MonadicRightAdjoint` and coreflec `ComonadicLeftAdjoint`. -/ --- test + namespace CategoryTheory open Category From 41480364d603aa47f0ac19a34c86cce42614c13b Mon Sep 17 00:00:00 2001 From: Christian Merten Date: Wed, 23 Apr 2025 17:33:13 +0200 Subject: [PATCH 20/29] fix --- .../Algebra/Category/ModuleCat/Descent.lean | 89 +++++++++++++++---- .../Limits/Preserves/Shapes/Equalizers.lean | 9 -- 2 files changed, 70 insertions(+), 28 deletions(-) diff --git a/Mathlib/Algebra/Category/ModuleCat/Descent.lean b/Mathlib/Algebra/Category/ModuleCat/Descent.lean index d01601e30d791b..1d281912d46e35 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Descent.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Descent.lean @@ -1,16 +1,19 @@ import Mathlib.CategoryTheory.Monad.Comonadicity +import Mathlib.CategoryTheory.Monad.Monadicity import Mathlib.CategoryTheory.Preadditive.LeftExact import Mathlib.Algebra.Category.ModuleCat.Abelian import Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic import Mathlib.Algebra.Category.ModuleCat.ChangeOfRings -import Mathlib.RingTheory.Flat.Algebra +import Mathlib.Algebra.Homology.ShortComplex.ExactFunctor +import Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed import Mathlib.RingTheory.Flat.Basic +import Mathlib.RingTheory.RingHom.Flat noncomputable section open CategoryTheory Comonad ModuleCat Limits MonoidalCategory -variable {A B : Type} [CommRing.{0} A] [CommRing.{0} B] (f : A →+* B) [f.Flat] +variable {A B : Type} [CommRing.{0} A] [CommRing.{0} B] (f : A →+* B) (hf : f.Flat) -- [(extendScalars f).ReflectsIsomorphisms] -- `f` is faithfully flat. example : ModuleCat A ⥤ ModuleCat B := ModuleCat.extendScalars f @@ -21,25 +24,70 @@ example : extendScalars f ⋙ restrictScalars f ≅ tensorLeft ((restrictScalars f).obj (ModuleCat.of B B)) := Iso.refl _ -instance : Module.Flat A ((restrictScalars f).obj (ModuleCat.of B B)) := - -- algebraize f - let _ : Algebra A B := f.toAlgebra - (inferInstance : f.Flat).1.1 +instance : Module.Flat A ((restrictScalars f).obj (ModuleCat.of B B)) := hf -instance : PreservesFiniteLimits <| tensorLeft ((restrictScalars f).obj (ModuleCat.of B B)) := - sorry -- This is in a PR +instance (M : ModuleCat.{0} A) [Module.Flat A M] : + PreservesFiniteLimits <| tensorLeft M := by + have h1 := (Functor.preservesFiniteLimits_tfae (tensorLeft M)).out 0 3 + have h2 := ((Functor.preservesFiniteColimits_tfae (tensorLeft M)).out 0 3).mpr + (inferInstanceAs <| PreservesFiniteColimits (tensorLeft M)) + rw [← h1] + intro S hS + refine ⟨(h2 S hS).1, ?_⟩ + have := hS.mono_f + rw [ModuleCat.mono_iff_injective] at this ⊢ + apply Module.Flat.lTensor_preserves_injective_linearMap + exact this -instance : PreservesFiniteLimits (extendScalars f) := by - have : PreservesFiniteLimits (extendScalars f ⋙ restrictScalars f) := - inferInstanceAs - (PreservesFiniteLimits <| tensorLeft ((restrictScalars f).obj (ModuleCat.of B B))) - apply preservesFiniteLimitsOfReflectsOfPreserves (extendScalars f) (restrictScalars f) +include hf in +lemma ModuleCat.preservesFiniteLimits_tensorLeft_of_flat : + PreservesFiniteLimits <| tensorLeft ((restrictScalars f).obj (ModuleCat.of B B)) := by + algebraize [f] + change PreservesFiniteLimits <| tensorLeft (ModuleCat.of A B) + infer_instance -def extendScalarsComonadic : ComonadicLeftAdjoint (extendScalars f) := by +instance : (restrictScalars f).ReflectsIsomorphisms := + have : (restrictScalars f ⋙ CategoryTheory.forget (ModuleCat A)).ReflectsIsomorphisms := + inferInstanceAs (CategoryTheory.forget _).ReflectsIsomorphisms + reflectsIsomorphisms_of_comp _ (CategoryTheory.forget _) + +include hf in +lemma ModuleCat.preservesFiniteLimits_extendScalars_of_flat : + PreservesFiniteLimits (extendScalars.{_, _, 0} f) := by + have : PreservesFiniteLimits (extendScalars.{0} f ⋙ restrictScalars f) := by + apply ModuleCat.preservesFiniteLimits_tensorLeft_of_flat + exact hf + exact preservesFiniteLimits_of_reflects_of_preserves (extendScalars f) (restrictScalars f) + +@[simp] +lemma Module.FaithfullyFlat.lTensor_bijective_iff_bijective {R M : Type*} + [CommRing R] [AddCommGroup M] [Module R M] {N N' : Type*} + [AddCommGroup N] [AddCommGroup N'] [Module R N] [Module R N'] + (f : N →ₗ[R] N') + [Module.FaithfullyFlat R M] : + Function.Bijective (f.lTensor M) ↔ Function.Bijective f := by + simp [Function.Bijective] + +include hf in +lemma ModuleCat.reflectsIsomorphisms_extendScalars_of_flat + (hs : Function.Surjective f.specComap) : + (extendScalars.{_, _, 0} f).ReflectsIsomorphisms := by + constructor + intro M N g h + rw [ConcreteCategory.isIso_iff_bijective] at h ⊢ + algebraize [f] + have : Module.Flat A B := hf + have : Module.FaithfullyFlat A B := + Module.FaithfullyFlat.of_specComap_surjective hs + replace h : Function.Bijective (LinearMap.lTensor B g.hom) := h + rwa [Module.FaithfullyFlat.lTensor_bijective_iff_bijective] at h + +def extendScalarsComonadic (hs : Function.Surjective f.specComap) : + ComonadicLeftAdjoint (extendScalars f) := by apply (config := {allowSynthFailures := true}) - monadicOfHasPreservesGSplitCoequalizersOfReflectsIsomorphisms (G := restrictScalars f) + Comonad.comonadicOfHasPreservesFSplitEqualizersOfReflectsIsomorphisms (G := restrictScalars f) · exact (extendRestrictScalarsAdj f) - · sorry -- This follows from `f` being faithfully flat. + · exact reflectsIsomorphisms_extendScalars_of_flat f hf hs · constructor intros infer_instance @@ -47,11 +95,14 @@ def extendScalarsComonadic : ComonadicLeftAdjoint (extendScalars f) := by PreservesLimit (parallelPair g (0 : M ⟶ N)) (extendScalars f) by constructor intros - apply CategoryTheory.Functor.preservesEqualizerOfPreservesKernels + apply CategoryTheory.Functor.preservesEqualizer_of_preservesKernels + have : PreservesFiniteLimits (extendScalars f) := + preservesFiniteLimits_extendScalars_of_flat f hf intro M N g infer_instance example : Comonad (ModuleCat B) := (extendRestrictScalarsAdj f).toComonad -example (Q : Coalgebra (extendRestrictScalarsAdj f).toComonad) : ModuleCat A := - (comparison (extendScalarsComonadic f).adj).asEquivalence.inverse.obj Q +example (hs : Function.Surjective f.specComap) + (Q : Coalgebra (extendRestrictScalarsAdj f).toComonad) : ModuleCat A := + (comparison (extendScalarsComonadic f hf hs).adj).asEquivalence.inverse.obj Q diff --git a/Mathlib/CategoryTheory/Limits/Preserves/Shapes/Equalizers.lean b/Mathlib/CategoryTheory/Limits/Preserves/Shapes/Equalizers.lean index e620182fbccafc..3e3b781aeb0d85 100644 --- a/Mathlib/CategoryTheory/Limits/Preserves/Shapes/Equalizers.lean +++ b/Mathlib/CategoryTheory/Limits/Preserves/Shapes/Equalizers.lean @@ -240,15 +240,6 @@ instance (priority := 1) preservesSplitEqualizers (f g : X ⟶ Y) [HasSplitEqual (isLimitMapConeForkEquiv G _).symm ((HasSplitEqualizer.isSplitEqualizer f g).map G).isEqualizer -instance (priority := 1) preservesSplitEqualizers (f g : X ⟶ Y) [HasSplitEqualizer f g] : - PreservesLimit (parallelPair f g) G := by - apply - preservesLimitOfPreservesLimitCone - (HasSplitEqualizer.isSplitEqualizer f g).isEqualizer - apply - (isLimitMapConeForkEquiv G _).symm - ((HasSplitEqualizer.isSplitEqualizer f g).map G).isEqualizer - end Coequalizers end CategoryTheory.Limits From 86496f29f5ebc9d19e407a2043d9963a227f2dc6 Mon Sep 17 00:00:00 2001 From: Christian Merten Date: Sat, 26 Apr 2025 01:05:19 +0200 Subject: [PATCH 21/29] and properties --- Mathlib/RingTheory/LocalProperties/Basic.lean | 39 +++++++++++++++++++ Mathlib/RingTheory/RingHomProperties.lean | 21 +++++++++- 2 files changed, 59 insertions(+), 1 deletion(-) diff --git a/Mathlib/RingTheory/LocalProperties/Basic.lean b/Mathlib/RingTheory/LocalProperties/Basic.lean index 6cfd1fc4831360..b0749f7956f8d8 100644 --- a/Mathlib/RingTheory/LocalProperties/Basic.lean +++ b/Mathlib/RingTheory/LocalProperties/Basic.lean @@ -355,6 +355,45 @@ lemma RingHom.OfLocalizationSpanTarget.ofIsLocalization section +variable {Q : ∀ {R S : Type u} [CommRing R] [CommRing S], (R →+* S) → Prop} + +lemma RingHom.OfLocalizationSpanTarget.and (hP : OfLocalizationSpanTarget P) + (hQ : OfLocalizationSpanTarget Q) : + OfLocalizationSpanTarget (fun f ↦ P f ∧ Q f) := by + introv R hs hf + exact ⟨hP f s hs fun r ↦ (hf r).1, hQ f s hs fun r ↦ (hf r).2⟩ + +lemma RingHom.OfLocalizationSpan.and (hP : OfLocalizationSpan P) (hQ : OfLocalizationSpan Q) : + OfLocalizationSpan (fun f ↦ P f ∧ Q f) := by + introv R hs hf + exact ⟨hP f s hs fun r ↦ (hf r).1, hQ f s hs fun r ↦ (hf r).2⟩ + +lemma RingHom.LocalizationAwayPreserves.and (hP : LocalizationAwayPreserves P) + (hQ : LocalizationAwayPreserves Q) : + LocalizationAwayPreserves (fun f ↦ P f ∧ Q f) := by + introv R h + exact ⟨hP f r R' S' h.1, hQ f r R' S' h.2⟩ + +lemma RingHom.StableUnderCompositionWithLocalizationAwayTarget.and + (hP : StableUnderCompositionWithLocalizationAwayTarget P) + (hQ : StableUnderCompositionWithLocalizationAwayTarget Q) : + StableUnderCompositionWithLocalizationAwayTarget (fun f ↦ P f ∧ Q f) := by + introv R h hf + exact ⟨hP T s f hf.1, hQ T s f hf.2⟩ + +lemma RingHom.PropertyIsLocal.and (hP : PropertyIsLocal P) (hQ : PropertyIsLocal Q) : + PropertyIsLocal (fun f ↦ P f ∧ Q f) where + localizationAwayPreserves := hP.localizationAwayPreserves.and hQ.localizationAwayPreserves + ofLocalizationSpanTarget := hP.ofLocalizationSpanTarget.and hQ.ofLocalizationSpanTarget + ofLocalizationSpan := hP.ofLocalizationSpan.and hQ.ofLocalizationSpan + StableUnderCompositionWithLocalizationAwayTarget := + hP.StableUnderCompositionWithLocalizationAwayTarget.and + hQ.StableUnderCompositionWithLocalizationAwayTarget + +end + +section + variable (hP : RingHom.IsStableUnderBaseChange @P) variable {R S Rᵣ Sᵣ : Type u} [CommRing R] [CommRing S] [CommRing Rᵣ] [CommRing Sᵣ] [Algebra R Rᵣ] [Algebra S Sᵣ] diff --git a/Mathlib/RingTheory/RingHomProperties.lean b/Mathlib/RingTheory/RingHomProperties.lean index dc7809bdc84400..3f1f054981e766 100644 --- a/Mathlib/RingTheory/RingHomProperties.lean +++ b/Mathlib/RingTheory/RingHomProperties.lean @@ -30,7 +30,7 @@ open CategoryTheory Opposite CategoryTheory.Limits namespace RingHom -variable (P : ∀ {R S : Type u} [CommRing R] [CommRing S] (_ : R →+* S), Prop) +variable (P Q : ∀ {R S : Type u} [CommRing R] [CommRing S] (_ : R →+* S), Prop) {Q} section RespectsIso @@ -87,6 +87,14 @@ theorem RespectsIso.isLocalization_away_iff (hP : RingHom.RespectsIso @P) {R S : @[deprecated (since := "2025-03-01")] alias RespectsIso.is_localization_away_iff := RespectsIso.isLocalization_away_iff +lemma RespectsIso.and (hP : RespectsIso P) (hQ : RespectsIso Q) : + RespectsIso (fun f ↦ P f ∧ Q f) := by + refine ⟨?_, ?_⟩ + · introv hf + exact ⟨hP.1 f e hf.1, hQ.1 f e hf.2⟩ + · introv hf + exact ⟨hP.2 f e hf.1, hQ.2 f e hf.2⟩ + end RespectsIso section StableUnderComposition @@ -110,6 +118,11 @@ theorem StableUnderComposition.respectsIso (hP : RingHom.StableUnderComposition apply hP exacts [hP' e, H] +lemma StableUnderComposition.and (hP : StableUnderComposition P) (hQ : StableUnderComposition Q) : + StableUnderComposition (fun f ↦ P f ∧ Q f) := by + introv R hf hg + exact ⟨hP f g hf.1 hg.1, hQ f g hf.2 hg.2⟩ + end StableUnderComposition section IsStableUnderBaseChange @@ -169,6 +182,12 @@ theorem IsStableUnderBaseChange.pushout_inl (hP : RingHom.IsStableUnderBaseChang apply hP R T S (TensorProduct R S T) exact H +lemma IsStableUnderBaseChange.and (hP : IsStableUnderBaseChange P) + (hQ : IsStableUnderBaseChange Q) : + IsStableUnderBaseChange (fun f ↦ P f ∧ Q f) := by + introv R _ h + exact ⟨hP R S R' S' h.1, hQ R S R' S' h.2⟩ + end IsStableUnderBaseChange section ToMorphismProperty From 0c2a9ef505eb2f0fb3de0c1fc2fe3c302abe032a Mon Sep 17 00:00:00 2001 From: Christian Merten <136261474+chrisflav@users.noreply.github.com> Date: Thu, 1 May 2025 14:08:16 +0200 Subject: [PATCH 22/29] Update Mathlib/RingTheory/RingHomProperties.lean Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com> --- Mathlib/RingTheory/RingHomProperties.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/RingTheory/RingHomProperties.lean b/Mathlib/RingTheory/RingHomProperties.lean index 3f1f054981e766..62f27e217b774b 100644 --- a/Mathlib/RingTheory/RingHomProperties.lean +++ b/Mathlib/RingTheory/RingHomProperties.lean @@ -30,7 +30,7 @@ open CategoryTheory Opposite CategoryTheory.Limits namespace RingHom -variable (P Q : ∀ {R S : Type u} [CommRing R] [CommRing S] (_ : R →+* S), Prop) {Q} +variable {P Q : ∀ {R S : Type u} [CommRing R] [CommRing S] (_ : R →+* S), Prop} section RespectsIso From bcf51bf7d56d265a9e8d2df1e0fb4ae91169c236 Mon Sep 17 00:00:00 2001 From: Christian Merten Date: Thu, 1 May 2025 14:10:06 +0200 Subject: [PATCH 23/29] fix --- Mathlib/RingTheory/RingHomProperties.lean | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/Mathlib/RingTheory/RingHomProperties.lean b/Mathlib/RingTheory/RingHomProperties.lean index 62f27e217b774b..ae7717b5ea7daa 100644 --- a/Mathlib/RingTheory/RingHomProperties.lean +++ b/Mathlib/RingTheory/RingHomProperties.lean @@ -34,6 +34,7 @@ variable {P Q : ∀ {R S : Type u} [CommRing R] [CommRing S] (_ : R →+* S), Pr section RespectsIso +variable (P) in /-- A property `RespectsIso` if it still holds when composed with an isomorphism -/ def RespectsIso : Prop := (∀ {R S T : Type u} [CommRing R] [CommRing S] [CommRing T], @@ -41,8 +42,6 @@ def RespectsIso : Prop := ∀ {R S T : Type u} [CommRing R] [CommRing S] [CommRing T], ∀ (f : S →+* T) (e : R ≃+* S) (_ : P f), P (f.comp e.toRingHom) -variable {P} - theorem RespectsIso.cancel_left_isIso (hP : RespectsIso @P) {R S T : CommRingCat} (f : R ⟶ S) (g : S ⟶ T) [IsIso f] : P (g.hom.comp f.hom) ↔ P g.hom := ⟨fun H => by @@ -99,14 +98,13 @@ end RespectsIso section StableUnderComposition +variable (P) in /-- A property is `StableUnderComposition` if the composition of two such morphisms still falls in the class. -/ def StableUnderComposition : Prop := ∀ ⦃R S T⦄ [CommRing R] [CommRing S] [CommRing T], ∀ (f : R →+* S) (g : S →+* T) (_ : P f) (_ : P g), P (g.comp f) -variable {P} - theorem StableUnderComposition.respectsIso (hP : RingHom.StableUnderComposition @P) (hP' : ∀ {R S : Type u} [CommRing R] [CommRing S] (e : R ≃+* S), P e.toRingHom) : RingHom.RespectsIso @P := by @@ -127,6 +125,7 @@ end StableUnderComposition section IsStableUnderBaseChange +variable (P) in /-- A morphism property `P` is `IsStableUnderBaseChange` if `P(S →+* A)` implies `P(B →+* A ⊗[S] B)`. -/ def IsStableUnderBaseChange : Prop := @@ -192,12 +191,11 @@ end IsStableUnderBaseChange section ToMorphismProperty +variable (P) in /-- The categorical `MorphismProperty` associated to a property of ring homs expressed non-categorical terms. -/ def toMorphismProperty : MorphismProperty CommRingCat := fun _ _ f ↦ P f.hom -variable {P} - lemma toMorphismProperty_respectsIso_iff : RespectsIso P ↔ (toMorphismProperty P).RespectsIso := by refine ⟨fun h ↦ MorphismProperty.RespectsIso.mk _ ?_ ?_, fun h ↦ ⟨?_, ?_⟩⟩ From f48aef20ec163ee6d56512fbb9d26099e856c596 Mon Sep 17 00:00:00 2001 From: Christian Merten Date: Thu, 1 May 2025 14:26:36 +0200 Subject: [PATCH 24/29] fix --- Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean | 2 +- Mathlib/RingTheory/RingHom/Finite.lean | 2 +- Mathlib/RingTheory/RingHom/Flat.lean | 2 +- Mathlib/RingTheory/RingHom/Integral.lean | 2 +- Mathlib/RingTheory/RingHom/Locally.lean | 2 +- Mathlib/RingTheory/RingHom/Surjective.lean | 2 +- Mathlib/RingTheory/RingHom/Unramified.lean | 2 +- 7 files changed, 7 insertions(+), 7 deletions(-) diff --git a/Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean b/Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean index 0cb356bd847ca4..e0585bd799331b 100644 --- a/Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean +++ b/Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean @@ -83,7 +83,7 @@ theorem IsStableUnderBaseChange.pullback_fst_appTop Functor.op_map, Quiver.Hom.unop_op, AffineScheme.forgetToScheme_map, Scheme.Γ_map] at this rw [← this, CommRingCat.hom_comp, hP'.cancel_right_isIso, ← pushoutIsoUnopPullback_inl_hom, CommRingCat.hom_comp, hP'.cancel_right_isIso] - exact hP.pushout_inl _ hP' _ _ H + exact hP.pushout_inl hP' _ _ H @[deprecated (since := "2024-11-23")] alias IsStableUnderBaseChange.pullback_fst_app_top := diff --git a/Mathlib/RingTheory/RingHom/Finite.lean b/Mathlib/RingTheory/RingHom/Finite.lean index 3286a56d35bb24..c47a16a49c844b 100644 --- a/Mathlib/RingTheory/RingHom/Finite.lean +++ b/Mathlib/RingTheory/RingHom/Finite.lean @@ -41,7 +41,7 @@ theorem finite_respectsIso : RespectsIso @Finite := by lemma finite_containsIdentities : ContainsIdentities @Finite := Finite.id theorem finite_isStableUnderBaseChange : IsStableUnderBaseChange @Finite := by - refine IsStableUnderBaseChange.mk _ finite_respectsIso ?_ + refine IsStableUnderBaseChange.mk finite_respectsIso ?_ classical introv h replace h : Module.Finite R T := by diff --git a/Mathlib/RingTheory/RingHom/Flat.lean b/Mathlib/RingTheory/RingHom/Flat.lean index ae742aa4674fc8..210e13e1274c61 100644 --- a/Mathlib/RingTheory/RingHom/Flat.lean +++ b/Mathlib/RingTheory/RingHom/Flat.lean @@ -61,7 +61,7 @@ lemma respectsIso : RespectsIso Flat := by exact of_bijective e.bijective lemma isStableUnderBaseChange : IsStableUnderBaseChange Flat := by - apply IsStableUnderBaseChange.mk _ respectsIso + apply IsStableUnderBaseChange.mk respectsIso introv h replace h : Module.Flat R T := by rw [RingHom.Flat] at h; convert h; ext; simp_rw [Algebra.smul_def]; rfl diff --git a/Mathlib/RingTheory/RingHom/Integral.lean b/Mathlib/RingTheory/RingHom/Integral.lean index a938ac44a00cbf..0822781dc03f4c 100644 --- a/Mathlib/RingTheory/RingHom/Integral.lean +++ b/Mathlib/RingTheory/RingHom/Integral.lean @@ -29,7 +29,7 @@ theorem isIntegral_respectsIso : RespectsIso fun f => f.IsIntegral := by apply RingHom.isIntegralElem_map theorem isIntegral_isStableUnderBaseChange : IsStableUnderBaseChange fun f => f.IsIntegral := by - refine IsStableUnderBaseChange.mk _ isIntegral_respectsIso ?_ + refine IsStableUnderBaseChange.mk isIntegral_respectsIso ?_ introv h x refine TensorProduct.induction_on x ?_ ?_ ?_ · apply isIntegral_zero diff --git a/Mathlib/RingTheory/RingHom/Locally.lean b/Mathlib/RingTheory/RingHom/Locally.lean index f84f17bcf4d46f..f1edbe094e293a 100644 --- a/Mathlib/RingTheory/RingHom/Locally.lean +++ b/Mathlib/RingTheory/RingHom/Locally.lean @@ -272,7 +272,7 @@ attribute [local instance] Algebra.TensorProduct.rightAlgebra in /-- If `P` is stable under base change, then so is `Locally P`. -/ lemma locally_isStableUnderBaseChange (hPi : RespectsIso P) (hPb : IsStableUnderBaseChange P) : IsStableUnderBaseChange (Locally P) := by - apply IsStableUnderBaseChange.mk _ (locally_respectsIso hPi) + apply IsStableUnderBaseChange.mk (locally_respectsIso hPi) introv hf obtain ⟨s, hsone, hs⟩ := hf rw [locally_iff_exists hPi] diff --git a/Mathlib/RingTheory/RingHom/Surjective.lean b/Mathlib/RingTheory/RingHom/Surjective.lean index f81c8c1d9032bd..6158b94c50ed03 100644 --- a/Mathlib/RingTheory/RingHom/Surjective.lean +++ b/Mathlib/RingTheory/RingHom/Surjective.lean @@ -42,7 +42,7 @@ theorem surjective_respectsIso : RespectsIso surjective := by exact e.surjective theorem surjective_isStableUnderBaseChange : IsStableUnderBaseChange surjective := by - refine IsStableUnderBaseChange.mk _ surjective_respectsIso ?_ + refine IsStableUnderBaseChange.mk surjective_respectsIso ?_ classical introv h x induction x with diff --git a/Mathlib/RingTheory/RingHom/Unramified.lean b/Mathlib/RingTheory/RingHom/Unramified.lean index 1016996901edb0..5f0952a47462eb 100644 --- a/Mathlib/RingTheory/RingHom/Unramified.lean +++ b/Mathlib/RingTheory/RingHom/Unramified.lean @@ -48,7 +48,7 @@ lemma respectsIso : lemma isStableUnderBaseChange : IsStableUnderBaseChange FormallyUnramified := by - refine .mk _ respectsIso ?_ + refine .mk respectsIso ?_ intros R S T _ _ _ _ _ h show (algebraMap _ _).FormallyUnramified rw [formallyUnramified_algebraMap] at h ⊢ From ee76441014216019867d6f9f6f5a300afb404f5d Mon Sep 17 00:00:00 2001 From: Christian Merten Date: Fri, 2 May 2025 00:04:14 +0200 Subject: [PATCH 25/29] cleanup --- .../Algebra/Category/ModuleCat/Descent.lean | 30 +++++-------------- 1 file changed, 7 insertions(+), 23 deletions(-) diff --git a/Mathlib/Algebra/Category/ModuleCat/Descent.lean b/Mathlib/Algebra/Category/ModuleCat/Descent.lean index 1d281912d46e35..62e66b22dd0129 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Descent.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Descent.lean @@ -9,24 +9,15 @@ import Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed import Mathlib.RingTheory.Flat.Basic import Mathlib.RingTheory.RingHom.Flat +universe u + noncomputable section open CategoryTheory Comonad ModuleCat Limits MonoidalCategory -variable {A B : Type} [CommRing.{0} A] [CommRing.{0} B] (f : A →+* B) (hf : f.Flat) - -- [(extendScalars f).ReflectsIsomorphisms] -- `f` is faithfully flat. - -example : ModuleCat A ⥤ ModuleCat B := ModuleCat.extendScalars f - -instance : Module A B := f.toAlgebra.toModule - -example : extendScalars f ⋙ restrictScalars f ≅ - tensorLeft ((restrictScalars f).obj (ModuleCat.of B B)) := - Iso.refl _ +variable {A B : Type u} [CommRing A] [CommRing B] (f : A →+* B) (hf : f.Flat) -instance : Module.Flat A ((restrictScalars f).obj (ModuleCat.of B B)) := hf - -instance (M : ModuleCat.{0} A) [Module.Flat A M] : +instance (M : ModuleCat.{u} A) [Module.Flat A M] : PreservesFiniteLimits <| tensorLeft M := by have h1 := (Functor.preservesFiniteLimits_tfae (tensorLeft M)).out 0 3 have h2 := ((Functor.preservesFiniteColimits_tfae (tensorLeft M)).out 0 3).mpr @@ -53,8 +44,8 @@ instance : (restrictScalars f).ReflectsIsomorphisms := include hf in lemma ModuleCat.preservesFiniteLimits_extendScalars_of_flat : - PreservesFiniteLimits (extendScalars.{_, _, 0} f) := by - have : PreservesFiniteLimits (extendScalars.{0} f ⋙ restrictScalars f) := by + PreservesFiniteLimits (extendScalars.{_, _, u} f) := by + have : PreservesFiniteLimits (extendScalars.{_, _, u} f ⋙ restrictScalars.{_, _, u} f) := by apply ModuleCat.preservesFiniteLimits_tensorLeft_of_flat exact hf exact preservesFiniteLimits_of_reflects_of_preserves (extendScalars f) (restrictScalars f) @@ -71,12 +62,11 @@ lemma Module.FaithfullyFlat.lTensor_bijective_iff_bijective {R M : Type*} include hf in lemma ModuleCat.reflectsIsomorphisms_extendScalars_of_flat (hs : Function.Surjective f.specComap) : - (extendScalars.{_, _, 0} f).ReflectsIsomorphisms := by + (extendScalars.{_, _, u} f).ReflectsIsomorphisms := by constructor intro M N g h rw [ConcreteCategory.isIso_iff_bijective] at h ⊢ algebraize [f] - have : Module.Flat A B := hf have : Module.FaithfullyFlat A B := Module.FaithfullyFlat.of_specComap_surjective hs replace h : Function.Bijective (LinearMap.lTensor B g.hom) := h @@ -100,9 +90,3 @@ def extendScalarsComonadic (hs : Function.Surjective f.specComap) : preservesFiniteLimits_extendScalars_of_flat f hf intro M N g infer_instance - -example : Comonad (ModuleCat B) := (extendRestrictScalarsAdj f).toComonad - -example (hs : Function.Surjective f.specComap) - (Q : Coalgebra (extendRestrictScalarsAdj f).toComonad) : ModuleCat A := - (comparison (extendScalarsComonadic f hf hs).adj).asEquivalence.inverse.obj Q From 18b05ae102226c63ced3e43b09c53699e066c494 Mon Sep 17 00:00:00 2001 From: Christian Merten Date: Fri, 2 May 2025 00:24:09 +0200 Subject: [PATCH 26/29] faithfully flat ring homs --- Mathlib.lean | 1 + Mathlib/Algebra/Ring/Equiv.lean | 12 +++ .../RingTheory/RingHom/FaithfullyFlat.lean | 75 +++++++++++++++++++ Mathlib/RingTheory/RingHom/Flat.lean | 2 +- 4 files changed, 89 insertions(+), 1 deletion(-) create mode 100644 Mathlib/RingTheory/RingHom/FaithfullyFlat.lean diff --git a/Mathlib.lean b/Mathlib.lean index 7da2ef28a9dbbf..b965ae00755846 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -5275,6 +5275,7 @@ import Mathlib.RingTheory.Radical import Mathlib.RingTheory.ReesAlgebra import Mathlib.RingTheory.Regular.IsSMulRegular import Mathlib.RingTheory.Regular.RegularSequence +import Mathlib.RingTheory.RingHom.FaithfullyFlat import Mathlib.RingTheory.RingHom.Finite import Mathlib.RingTheory.RingHom.FinitePresentation import Mathlib.RingTheory.RingHom.FiniteType diff --git a/Mathlib/Algebra/Ring/Equiv.lean b/Mathlib/Algebra/Ring/Equiv.lean index cab85052362661..ac7fd9b16fda86 100644 --- a/Mathlib/Algebra/Ring/Equiv.lean +++ b/Mathlib/Algebra/Ring/Equiv.lean @@ -454,6 +454,18 @@ theorem ofBijective_apply [NonUnitalRingHomClass F R S] (f : F) (hf : Function.B (x : R) : ofBijective f hf x = f x := rfl +@[simp] +lemma ofBijective_symm_comp (f : R →ₙ+* S) (hf : Function.Bijective f) : + ((RingEquiv.ofBijective f hf).symm : _ →ₙ+* _).comp f = NonUnitalRingHom.id R := by + ext + exact (RingEquiv.ofBijective f hf).injective <| RingEquiv.apply_symm_apply .. + +@[simp] +lemma comp_ofBijective_symm (f : R →ₙ+* S) (hf : Function.Bijective f) : + f.comp ((RingEquiv.ofBijective f hf).symm : _ →ₙ+* _) = NonUnitalRingHom.id S := by + ext + exact (RingEquiv.ofBijective f hf).symm.injective <| RingEquiv.apply_symm_apply .. + /-- Product of a singleton family of (non-unital non-associative semi)rings is isomorphic to the only member of this family. -/ @[simps! -fullyApplied] diff --git a/Mathlib/RingTheory/RingHom/FaithfullyFlat.lean b/Mathlib/RingTheory/RingHom/FaithfullyFlat.lean new file mode 100644 index 00000000000000..6340f943b3a559 --- /dev/null +++ b/Mathlib/RingTheory/RingHom/FaithfullyFlat.lean @@ -0,0 +1,75 @@ +/- +Copyright (c) 2025 Christian Merten. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Merten, Joël Riou +-/ +import Mathlib.RingTheory.RingHom.Flat + +/-! +# Faithfully flat ring maps + +A ring map `f : R →+* S` is faithfully flat if `S` is faithfully flat as an `R`-algebra. This is +the same as being flat and a surjection on prime spectra. +-/ + +namespace RingHom + +variable {R S : Type*} [CommRing R] [CommRing S] {f : R →+* S} + +/-- A ring map `f : R →+* S` is faithfully flat if `S` is faithfully flat as an `R`-algebra. -/ +@[algebraize Module.FaithfullyFlat] +def FaithfullyFlat {R S : Type*} [CommRing R] [CommRing S] (f : R →+* S) : Prop := + letI : Algebra R S := f.toAlgebra + Module.FaithfullyFlat R S + +lemma faithfullyFlat_algebraMap_iff [Algebra R S] : + (algebraMap R S).FaithfullyFlat ↔ Module.FaithfullyFlat R S := by + simp only [RingHom.FaithfullyFlat] + congr! + exact Algebra.algebra_ext _ _ fun _ ↦ rfl + +namespace FaithfullyFlat + +lemma flat (hf : f.FaithfullyFlat) : f.Flat := by + algebraize [f] + exact inferInstanceAs <| Module.Flat R S + +lemma iff_flat_and_comap_surjective : + f.FaithfullyFlat ↔ f.Flat ∧ Function.Surjective f.specComap := by + algebraize [f] + show (algebraMap R S).FaithfullyFlat ↔ (algebraMap R S).Flat ∧ + Function.Surjective (algebraMap R S).specComap + rw [RingHom.faithfullyFlat_algebraMap_iff, RingHom.flat_algebraMap_iff] + exact ⟨fun h ↦ ⟨inferInstance, PrimeSpectrum.specComap_surjective_of_faithfullyFlat⟩, + fun ⟨h, hf⟩ ↦ .of_specComap_surjective hf⟩ + +lemma eq_and : @FaithfullyFlat = + fun R S (_ : CommRing R) (_ : CommRing S) f ↦ f.Flat ∧ Function.Surjective f.specComap := by + ext + rw [iff_flat_and_comap_surjective] + +lemma stableUnderComposition : StableUnderComposition FaithfullyFlat := by + rw [eq_and] + refine Flat.stableUnderComposition.and ?_ + introv R hf hg + rw [PrimeSpectrum.specComap_comp] + exact hf.comp hg + +lemma of_bijective (hf : Function.Bijective f) : f.FaithfullyFlat := by + rw [iff_flat_and_comap_surjective] + refine ⟨.of_bijective hf, fun p ↦ ?_⟩ + use ((RingEquiv.ofBijective f hf).symm : _ →+* _).specComap p + have : ((RingEquiv.ofBijective f hf).symm : _ →+* _).comp f = RingHom.id R := by + ext + exact (RingEquiv.ofBijective f hf).injective (by simp) + rw [← PrimeSpectrum.specComap_comp_apply, this, PrimeSpectrum.specComap_id] + +lemma respectsIso : RespectsIso FaithfullyFlat := + stableUnderComposition.respectsIso (fun e ↦ .of_bijective e.bijective) + +lemma isStableUnderBaseChange : IsStableUnderBaseChange FaithfullyFlat := by + refine .mk respectsIso (fun R S T _ _ _ _ _ _ ↦ show (algebraMap _ _).FaithfullyFlat from ?_) + rw [faithfullyFlat_algebraMap_iff] at * + infer_instance + +end RingHom.FaithfullyFlat diff --git a/Mathlib/RingTheory/RingHom/Flat.lean b/Mathlib/RingTheory/RingHom/Flat.lean index 210e13e1274c61..b4f888074c9b2a 100644 --- a/Mathlib/RingTheory/RingHom/Flat.lean +++ b/Mathlib/RingTheory/RingHom/Flat.lean @@ -24,7 +24,7 @@ def RingHom.Flat {R : Type u} {S : Type v} [CommRing R] [CommRing S] (f : R →+ letI : Algebra R S := f.toAlgebra Module.Flat R S -lemma flat_algebraMap_iff {R S : Type*} [CommRing R] [CommRing S] [Algebra R S] : +lemma RingHom.flat_algebraMap_iff {R S : Type*} [CommRing R] [CommRing S] [Algebra R S] : (algebraMap R S).Flat ↔ Module.Flat R S := by simp only [RingHom.Flat] congr! From 43aa480ba9b85beff7a2e87d551944b44066638f Mon Sep 17 00:00:00 2001 From: Christian Merten Date: Fri, 2 May 2025 01:23:35 +0200 Subject: [PATCH 27/29] cleanup --- .../Category/ModuleCat/ChangeOfRings.lean | 6 + .../Algebra/Category/ModuleCat/Descent.lean | 103 +++++++----------- .../Homology/ShortComplex/ExactFunctor.lean | 10 ++ .../RingTheory/Flat/FaithfullyFlat/Basic.lean | 5 + 4 files changed, 60 insertions(+), 64 deletions(-) diff --git a/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean b/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean index d0bf4dd5bae4ab..a8e53362943179 100644 --- a/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean +++ b/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean @@ -92,6 +92,12 @@ instance {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) : (restrictScalars.{v} f).PreservesMonomorphisms where preserves _ h := by rwa [mono_iff_injective] at h ⊢ +instance {R S : Type*} [Ring R] [Ring S] (f : R →+* S) : + (restrictScalars f).ReflectsIsomorphisms := + have : (restrictScalars f ⋙ CategoryTheory.forget (ModuleCat R)).ReflectsIsomorphisms := + inferInstanceAs (CategoryTheory.forget _).ReflectsIsomorphisms + reflectsIsomorphisms_of_comp _ (CategoryTheory.forget _) + -- Porting note: this should be automatic -- TODO: this instance gives diamonds if `f : S →+* S`, see `PresheafOfModules.pushforward₀`. -- The correct solution is probably to define explicit maps between `M` and diff --git a/Mathlib/Algebra/Category/ModuleCat/Descent.lean b/Mathlib/Algebra/Category/ModuleCat/Descent.lean index 62e66b22dd0129..2e9874f9398616 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Descent.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Descent.lean @@ -1,13 +1,22 @@ -import Mathlib.CategoryTheory.Monad.Comonadicity -import Mathlib.CategoryTheory.Monad.Monadicity -import Mathlib.CategoryTheory.Preadditive.LeftExact +/- +Copyright (c) 2025 Dagur Asgeirsson. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Dagur Asgeirsson, Jack McKoen, Christian Merten, Joël Riou, Adam Topaz +-/ import Mathlib.Algebra.Category.ModuleCat.Abelian -import Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic import Mathlib.Algebra.Category.ModuleCat.ChangeOfRings -import Mathlib.Algebra.Homology.ShortComplex.ExactFunctor import Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed -import Mathlib.RingTheory.Flat.Basic -import Mathlib.RingTheory.RingHom.Flat +import Mathlib.Algebra.Homology.ShortComplex.ExactFunctor +import Mathlib.CategoryTheory.Monad.Comonadicity +import Mathlib.RingTheory.RingHom.FaithfullyFlat + +/-! +# Faithfully flat descent for modules + +In this file we show that extension of scalars by a faithfully flat ring homomorphism is comonadic. +Then the general theory of descent implies that the pseudofunctor to `Cat` given by extension +of scalars has effective descent relative to faithfully flat maps (TODO). +-/ universe u @@ -15,78 +24,44 @@ noncomputable section open CategoryTheory Comonad ModuleCat Limits MonoidalCategory -variable {A B : Type u} [CommRing A] [CommRing B] (f : A →+* B) (hf : f.Flat) +variable {A B : Type u} [CommRing A] [CommRing B] {f : A →+* B} -instance (M : ModuleCat.{u} A) [Module.Flat A M] : - PreservesFiniteLimits <| tensorLeft M := by - have h1 := (Functor.preservesFiniteLimits_tfae (tensorLeft M)).out 0 3 - have h2 := ((Functor.preservesFiniteColimits_tfae (tensorLeft M)).out 0 3).mpr +instance (M : ModuleCat.{u} A) [Module.Flat A M] : PreservesFiniteLimits <| tensorLeft M := by + have h2 := (Functor.preservesFiniteColimits_iff_forall_exact_map_and_epi (tensorLeft M)).mp (inferInstanceAs <| PreservesFiniteColimits (tensorLeft M)) - rw [← h1] - intro S hS - refine ⟨(h2 S hS).1, ?_⟩ + rw [Functor.preservesFiniteLimits_iff_forall_exact_map_and_mono] + refine fun S hS ↦ ⟨(h2 S hS).1, ?_⟩ have := hS.mono_f rw [ModuleCat.mono_iff_injective] at this ⊢ - apply Module.Flat.lTensor_preserves_injective_linearMap - exact this + exact Module.Flat.lTensor_preserves_injective_linearMap _ this -include hf in -lemma ModuleCat.preservesFiniteLimits_tensorLeft_of_flat : +lemma ModuleCat.preservesFiniteLimits_tensorLeft_of_flat (hf : f.Flat) : PreservesFiniteLimits <| tensorLeft ((restrictScalars f).obj (ModuleCat.of B B)) := by algebraize [f] change PreservesFiniteLimits <| tensorLeft (ModuleCat.of A B) infer_instance -instance : (restrictScalars f).ReflectsIsomorphisms := - have : (restrictScalars f ⋙ CategoryTheory.forget (ModuleCat A)).ReflectsIsomorphisms := - inferInstanceAs (CategoryTheory.forget _).ReflectsIsomorphisms - reflectsIsomorphisms_of_comp _ (CategoryTheory.forget _) - -include hf in -lemma ModuleCat.preservesFiniteLimits_extendScalars_of_flat : +lemma ModuleCat.preservesFiniteLimits_extendScalars_of_flat (hf : f.Flat) : PreservesFiniteLimits (extendScalars.{_, _, u} f) := by - have : PreservesFiniteLimits (extendScalars.{_, _, u} f ⋙ restrictScalars.{_, _, u} f) := by - apply ModuleCat.preservesFiniteLimits_tensorLeft_of_flat - exact hf + have : PreservesFiniteLimits (extendScalars.{_, _, u} f ⋙ restrictScalars.{_, _, u} f) := + ModuleCat.preservesFiniteLimits_tensorLeft_of_flat hf exact preservesFiniteLimits_of_reflects_of_preserves (extendScalars f) (restrictScalars f) -@[simp] -lemma Module.FaithfullyFlat.lTensor_bijective_iff_bijective {R M : Type*} - [CommRing R] [AddCommGroup M] [Module R M] {N N' : Type*} - [AddCommGroup N] [AddCommGroup N'] [Module R N] [Module R N'] - (f : N →ₗ[R] N') - [Module.FaithfullyFlat R M] : - Function.Bijective (f.lTensor M) ↔ Function.Bijective f := by - simp [Function.Bijective] - -include hf in -lemma ModuleCat.reflectsIsomorphisms_extendScalars_of_flat - (hs : Function.Surjective f.specComap) : - (extendScalars.{_, _, u} f).ReflectsIsomorphisms := by - constructor - intro M N g h - rw [ConcreteCategory.isIso_iff_bijective] at h ⊢ +/-- Extension of scalars along faithfully flat ring maps reflects isomorphisms. -/ +lemma ModuleCat.reflectsIsomorphisms_extendScalars_of_faithfullyFlat + (hf : f.FaithfullyFlat) : (extendScalars.{_, _, u} f).ReflectsIsomorphisms := by + refine ⟨fun {M N} g h ↦ ?_⟩ algebraize [f] - have : Module.FaithfullyFlat A B := - Module.FaithfullyFlat.of_specComap_surjective hs + rw [ConcreteCategory.isIso_iff_bijective] at h ⊢ replace h : Function.Bijective (LinearMap.lTensor B g.hom) := h rwa [Module.FaithfullyFlat.lTensor_bijective_iff_bijective] at h -def extendScalarsComonadic (hs : Function.Surjective f.specComap) : +/-- Extension of scalars by a faithfully flat ring map is comonadic. -/ +def comonadicExtendScalars (hf : f.FaithfullyFlat) : ComonadicLeftAdjoint (extendScalars f) := by - apply (config := {allowSynthFailures := true}) - Comonad.comonadicOfHasPreservesFSplitEqualizersOfReflectsIsomorphisms (G := restrictScalars f) - · exact (extendRestrictScalarsAdj f) - · exact reflectsIsomorphisms_extendScalars_of_flat f hf hs - · constructor - intros - infer_instance - · suffices ∀ {M N : ModuleCat A} (g : M ⟶ N), - PreservesLimit (parallelPair g (0 : M ⟶ N)) (extendScalars f) by - constructor - intros - apply CategoryTheory.Functor.preservesEqualizer_of_preservesKernels - have : PreservesFiniteLimits (extendScalars f) := - preservesFiniteLimits_extendScalars_of_flat f hf - intro M N g - infer_instance + have := preservesFiniteLimits_extendScalars_of_flat hf.flat + have := reflectsIsomorphisms_extendScalars_of_faithfullyFlat hf + convert Comonad.comonadicOfHasPreservesFSplitEqualizersOfReflectsIsomorphisms + (extendRestrictScalarsAdj f) + · exact ⟨inferInstance⟩ + · exact ⟨inferInstance⟩ diff --git a/Mathlib/Algebra/Homology/ShortComplex/ExactFunctor.lean b/Mathlib/Algebra/Homology/ShortComplex/ExactFunctor.lean index 06141d6538e482..8c7c167112388c 100644 --- a/Mathlib/Algebra/Homology/ShortComplex/ExactFunctor.lean +++ b/Mathlib/Algebra/Homology/ShortComplex/ExactFunctor.lean @@ -147,6 +147,11 @@ lemma preservesFiniteLimits_tfae : List.TFAE tfae_finish +lemma preservesFiniteLimits_iff_forall_exact_map_and_mono : + PreservesFiniteLimits F ↔ + ∀ (S : ShortComplex C), S.ShortExact → (S.map F).Exact ∧ Mono (F.map S.f) := + ((Functor.preservesFiniteLimits_tfae F).out 0 3).symm + /-- If a functor `F : C ⥤ D` preserves exact sequences on the right hand side (i.e. if `0 ⟶ A ⟶ B ⟶ C ⟶ 0` is exact then `F(A) ⟶ F(B) ⟶ F(C) ⟶ 0` is exact), @@ -247,6 +252,11 @@ lemma exact_tfae : List.TFAE tfae_finish +lemma preservesFiniteColimits_iff_forall_exact_map_and_epi : + PreservesFiniteColimits F ↔ + ∀ (S : ShortComplex C), S.ShortExact → (S.map F).Exact ∧ Epi (F.map S.g) := + ((Functor.preservesFiniteColimits_tfae F).out 0 3).symm + end end Functor diff --git a/Mathlib/RingTheory/Flat/FaithfullyFlat/Basic.lean b/Mathlib/RingTheory/Flat/FaithfullyFlat/Basic.lean index 74a56aadc38d4c..966c677be6ed26 100644 --- a/Mathlib/RingTheory/Flat/FaithfullyFlat/Basic.lean +++ b/Mathlib/RingTheory/Flat/FaithfullyFlat/Basic.lean @@ -374,6 +374,11 @@ lemma lTensor_surjective_iff_surjective [Module.FaithfullyFlat R M] : conv_rhs => rw [← lTensor_exact_iff_exact R M] simp +@[simp] +lemma lTensor_bijective_iff_bijective [Module.FaithfullyFlat R M] : + Function.Bijective (f.lTensor M) ↔ Function.Bijective f := by + simp [Function.Bijective] + end end arbitrary_universe From 67d8ab20e8462ad34fff210a1f067f3deefc7dac Mon Sep 17 00:00:00 2001 From: Christian Merten Date: Fri, 2 May 2025 01:25:30 +0200 Subject: [PATCH 28/29] add note --- Mathlib/Algebra/Category/ModuleCat/Descent.lean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/Mathlib/Algebra/Category/ModuleCat/Descent.lean b/Mathlib/Algebra/Category/ModuleCat/Descent.lean index 2e9874f9398616..67a4dae1dd40dd 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Descent.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Descent.lean @@ -16,6 +16,11 @@ import Mathlib.RingTheory.RingHom.FaithfullyFlat In this file we show that extension of scalars by a faithfully flat ring homomorphism is comonadic. Then the general theory of descent implies that the pseudofunctor to `Cat` given by extension of scalars has effective descent relative to faithfully flat maps (TODO). + +## Notes + +This contribution was created as part of the AIM workshop +"Formalizing algebraic geometry" in June 2024. -/ universe u From 75f43a0c35f0c1f563cc2cedea41d4171d4589c1 Mon Sep 17 00:00:00 2001 From: Christian Merten Date: Fri, 2 May 2025 01:26:30 +0200 Subject: [PATCH 29/29] update mathlib --- Mathlib.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib.lean b/Mathlib.lean index b965ae00755846..aef15fa9894685 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -128,6 +128,7 @@ import Mathlib.Algebra.Category.ModuleCat.Basic import Mathlib.Algebra.Category.ModuleCat.Biproducts import Mathlib.Algebra.Category.ModuleCat.ChangeOfRings import Mathlib.Algebra.Category.ModuleCat.Colimits +import Mathlib.Algebra.Category.ModuleCat.Descent import Mathlib.Algebra.Category.ModuleCat.Differentials.Basic import Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf import Mathlib.Algebra.Category.ModuleCat.EnoughInjectives