From b1caad96de9fedbef8dec022c46a8be940ddd5b2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Mon, 4 Sep 2023 16:01:21 +0000 Subject: [PATCH] refactor: colimits in ModuleCat (#6925) This PR refactors the construction of colimits of modules in order to prove that the forgetful functor to abelian groups preserves colimits. --- .../Algebra/Category/AlgebraCat/Limits.lean | 4 +- Mathlib/Algebra/Category/GroupCat/Basic.lean | 20 + .../Algebra/Category/GroupCat/Colimits.lean | 94 ++-- Mathlib/Algebra/Category/GroupCat/Limits.lean | 13 - Mathlib/Algebra/Category/ModuleCat/Basic.lean | 99 +++- .../Algebra/Category/ModuleCat/Colimits.lean | 431 +++++------------- Mathlib/Algebra/Homology/LocalCohomology.lean | 20 +- 7 files changed, 294 insertions(+), 387 deletions(-) diff --git a/Mathlib/Algebra/Category/AlgebraCat/Limits.lean b/Mathlib/Algebra/Category/AlgebraCat/Limits.lean index a1123d13a527e..7a1c5c0cc541f 100644 --- a/Mathlib/Algebra/Category/AlgebraCat/Limits.lean +++ b/Mathlib/Algebra/Category/AlgebraCat/Limits.lean @@ -159,12 +159,12 @@ instance forget₂RingPreservesLimits : PreservesLimits (forget₂ (AlgebraCat R /-- The forgetful functor from R-algebras to R-modules preserves all limits. -/ instance forget₂ModulePreservesLimitsOfSize : PreservesLimitsOfSize.{v, v} - (forget₂ (AlgebraCatMax.{v, w} R) (ModuleCat.ModuleCatMax.{v, w} R)) where + (forget₂ (AlgebraCatMax.{v, w} R) (ModuleCatMax.{v, w} R)) where preservesLimitsOfShape := { preservesLimit := preservesLimitOfPreservesLimitCone (limitConeIsLimit _) (ModuleCat.HasLimits.limitConeIsLimit - (_ ⋙ forget₂ (AlgebraCatMax.{v, w} R) (ModuleCat.ModuleCatMax.{v, w} R))) } + (_ ⋙ forget₂ (AlgebraCatMax.{v, w} R) (ModuleCatMax.{v, w} R))) } #align Algebra.forget₂_Module_preserves_limits_of_size AlgebraCat.forget₂ModulePreservesLimitsOfSize instance forget₂ModulePreservesLimits : diff --git a/Mathlib/Algebra/Category/GroupCat/Basic.lean b/Mathlib/Algebra/Category/GroupCat/Basic.lean index 5f2ce8cee8f8a..c8affa0a4c1df 100644 --- a/Mathlib/Algebra/Category/GroupCat/Basic.lean +++ b/Mathlib/Algebra/Category/GroupCat/Basic.lean @@ -512,3 +512,23 @@ set_option linter.uppercaseLean3 false in #align CommGroup.forget_reflects_isos CommGroupCat.forget_reflects_isos set_option linter.uppercaseLean3 false in #align AddCommGroup.forget_reflects_isos AddCommGroupCat.forget_reflects_isos + +-- note: in the following definitions, there is a problem with `@[to_additive]` +-- as the `Category` instance is not found on the additive variant +-- this variant is then renamed with a `Aux` suffix + +/-- An alias for `GroupCat.{max u v}`, to deal around unification issues. -/ +@[to_additive (attr := nolint checkUnivs) GroupCatMaxAux + "An alias for `AddGroupCat.{max u v}`, to deal around unification issues."] +abbrev GroupCatMax.{u1, u2} := GroupCat.{max u1 u2} +/-- An alias for `AddGroupCat.{max u v}`, to deal around unification issues. -/ +@[nolint checkUnivs] +abbrev AddGroupCatMax.{u1, u2} := AddGroupCat.{max u1 u2} + +/-- An alias for `CommGroupCat.{max u v}`, to deal around unification issues. -/ +@[to_additive (attr := nolint checkUnivs) AddCommGroupCatMaxAux + "An alias for `AddCommGroupCat.{max u v}`, to deal around unification issues."] +abbrev CommGroupCatMax.{u1, u2} := CommGroupCat.{max u1 u2} +/-- An alias for `AddCommGroupCat.{max u v}`, to deal around unification issues. -/ +@[nolint checkUnivs] +abbrev AddCommGroupCatMax.{u1, u2} := AddCommGroupCat.{max u1 u2} diff --git a/Mathlib/Algebra/Category/GroupCat/Colimits.lean b/Mathlib/Algebra/Category/GroupCat/Colimits.lean index 46b69c1eebebc..935cffa8b2ffc 100644 --- a/Mathlib/Algebra/Category/GroupCat/Colimits.lean +++ b/Mathlib/Algebra/Category/GroupCat/Colimits.lean @@ -6,6 +6,7 @@ Authors: Scott Morrison import Mathlib.Algebra.Category.GroupCat.Preadditive import Mathlib.GroupTheory.QuotientGroup import Mathlib.CategoryTheory.Limits.Shapes.Kernels +import Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits import Mathlib.CategoryTheory.ConcreteCategory.Elementwise #align_import algebra.category.Group.colimits from "leanprover-community/mathlib"@"70fd9563a21e7b963887c9360bd29b2393e6225a" @@ -25,16 +26,18 @@ of finitely supported functions, and we really should implement this as well (or -- porting note: `AddCommGroup` in all the names set_option linter.uppercaseLean3 false -universe u v +universe w u v -open CategoryTheory - -open CategoryTheory.Limits +open CategoryTheory Limits -- [ROBOT VOICE]: -- You should pretend for now that this file was automatically generated. -- It follows the same template as colimits in Mon. -namespace AddCommGroupCat.Colimits +namespace AddCommGroupCat + +variable {J : Type u} [Category.{v} J] (F : J ⥤ AddCommGroupCat.{max u v w}) + +namespace Colimits /-! We build the colimit of a diagram in `AddCommGroupCat` by constructing the @@ -43,9 +46,6 @@ then taking the quotient by the abelian group laws within each abelian group, and the identifications given by the morphisms in the diagram. -/ - -variable {J : Type v} [SmallCategory J] (F : J ⥤ AddCommGroupCat.{v}) - /-- An inductive type representing all group expressions (without relations) on a collection of types indexed by the objects of `J`. -/ @@ -58,7 +58,7 @@ inductive Prequotient | add : Prequotient → Prequotient → Prequotient #align AddCommGroup.colimits.prequotient AddCommGroupCat.Colimits.Prequotient -instance : Inhabited (Prequotient F) := +instance : Inhabited (Prequotient.{w} F) := ⟨Prequotient.zero⟩ open Prequotient @@ -67,7 +67,7 @@ open Prequotient because of the abelian group laws, or because one element is mapped to another by a morphism in the diagram. -/ -inductive Relation : Prequotient F → Prequotient F → Prop +inductive Relation : Prequotient.{w} F → Prequotient.{w} F → Prop -- Make it an equivalence relation: | refl : ∀ x, Relation x x | symm : ∀ (x y) (_ : Relation x y), Relation y x @@ -95,7 +95,7 @@ inductive Relation : Prequotient F → Prequotient F → Prop /-- The setoid corresponding to group expressions modulo abelian group relations and identifications. -/ -def colimitSetoid : Setoid (Prequotient F) where +def colimitSetoid : Setoid (Prequotient.{w} F) where r := Relation F iseqv := ⟨Relation.refl, fun r => Relation.symm _ _ r, fun r => Relation.trans _ _ _ r⟩ #align AddCommGroup.colimits.colimit_setoid AddCommGroupCat.Colimits.colimitSetoid @@ -104,11 +104,11 @@ attribute [instance] colimitSetoid /-- The underlying type of the colimit of a diagram in `AddCommGroupCat`. -/ -def ColimitType : Type v := - Quotient (colimitSetoid F) +def ColimitType : Type max u v w := + Quotient (colimitSetoid.{w} F) #align AddCommGroup.colimits.colimit_type AddCommGroupCat.Colimits.ColimitType -instance : AddCommGroup (ColimitType F) where +instance : AddCommGroup (ColimitType.{w} F) where zero := Quotient.mk _ zero neg := Quotient.map neg Relation.neg_1 add := Quotient.map₂ add <| fun x x' rx y y' ry => @@ -120,17 +120,17 @@ instance : AddCommGroup (ColimitType F) where add_assoc := Quotient.ind <| fun _ => Quotient.ind₂ <| fun _ _ => Quotient.sound <| Relation.add_assoc _ _ _ -instance ColimitTypeInhabited : Inhabited (ColimitType.{v} F) := ⟨0⟩ +instance ColimitTypeInhabited : Inhabited (ColimitType.{w} F) := ⟨0⟩ @[simp] -theorem quot_zero : Quot.mk Setoid.r zero = (0 : ColimitType F) := +theorem quot_zero : Quot.mk Setoid.r zero = (0 : ColimitType.{w} F) := rfl #align AddCommGroup.colimits.quot_zero AddCommGroupCat.Colimits.quot_zero @[simp] theorem quot_neg (x) : Quot.mk Setoid.r (neg x) = -- Porting note : force Lean to treat `ColimitType F` no as `Quot _` - Neg.neg (α := ColimitType.{v} F) (Quot.mk Setoid.r x : ColimitType.{v} F) := + Neg.neg (α := ColimitType.{w} F) (Quot.mk Setoid.r x : ColimitType.{w} F) := rfl #align AddCommGroup.colimits.quot_neg AddCommGroupCat.Colimits.quot_neg @@ -138,23 +138,23 @@ theorem quot_neg (x) : Quot.mk Setoid.r (neg x) = theorem quot_add (x y) : Quot.mk Setoid.r (add x y) = -- Porting note : force Lean to treat `ColimitType F` no as `Quot _` - Add.add (α := ColimitType.{v} F) (Quot.mk Setoid.r x) (Quot.mk Setoid.r y) := + Add.add (α := ColimitType.{w} F) (Quot.mk Setoid.r x) (Quot.mk Setoid.r y) := rfl #align AddCommGroup.colimits.quot_add AddCommGroupCat.Colimits.quot_add /-- The bundled abelian group giving the colimit of a diagram. -/ def colimit : AddCommGroupCat := - AddCommGroupCat.of (ColimitType F) + AddCommGroupCat.of (ColimitType.{w} F) #align AddCommGroup.colimits.colimit AddCommGroupCat.Colimits.colimit /-- The function from a given abelian group in the diagram to the colimit abelian group. -/ -def coconeFun (j : J) (x : F.obj j) : ColimitType F := +def coconeFun (j : J) (x : F.obj j) : ColimitType.{w} F := Quot.mk _ (Prequotient.of j x) #align AddCommGroup.colimits.cocone_fun AddCommGroupCat.Colimits.coconeFun /-- The group homomorphism from a given abelian group in the diagram to the colimit abelian group. -/ -def coconeMorphism (j : J) : F.obj j ⟶ colimit F where +def coconeMorphism (j : J) : F.obj j ⟶ colimit.{w} F where toFun := coconeFun F j map_zero' := by apply Quot.sound; apply Relation.zero map_add' := by intros; apply Quot.sound; apply Relation.add @@ -162,7 +162,7 @@ def coconeMorphism (j : J) : F.obj j ⟶ colimit F where @[simp] theorem cocone_naturality {j j' : J} (f : j ⟶ j') : - F.map f ≫ coconeMorphism F j' = coconeMorphism F j := by + F.map f ≫ coconeMorphism.{w} F j' = coconeMorphism F j := by ext apply Quot.sound apply Relation.map @@ -170,21 +170,21 @@ theorem cocone_naturality {j j' : J} (f : j ⟶ j') : @[simp] theorem cocone_naturality_components (j j' : J) (f : j ⟶ j') (x : F.obj j) : - (coconeMorphism F j') (F.map f x) = (coconeMorphism F j) x := by + (coconeMorphism.{w} F j') (F.map f x) = (coconeMorphism F j) x := by rw [← cocone_naturality F f] rfl #align AddCommGroup.colimits.cocone_naturality_components AddCommGroupCat.Colimits.cocone_naturality_components /-- The cocone over the proposed colimit abelian group. -/ def colimitCocone : Cocone F where - pt := colimit F + pt := colimit.{w} F ι := { app := coconeMorphism F } #align AddCommGroup.colimits.colimit_cocone AddCommGroupCat.Colimits.colimitCocone /-- The function from the free abelian group on the diagram to the cone point of any other cocone. -/ @[simp] -def descFunLift (s : Cocone F) : Prequotient F → s.pt +def descFunLift (s : Cocone F) : Prequotient.{w} F → s.pt | Prequotient.of j x => (s.ι.app j) x | zero => 0 | neg x => -descFunLift s x @@ -192,7 +192,7 @@ def descFunLift (s : Cocone F) : Prequotient F → s.pt #align AddCommGroup.colimits.desc_fun_lift AddCommGroupCat.Colimits.descFunLift /-- The function from the colimit abelian group to the cone point of any other cocone. -/ -def descFun (s : Cocone F) : ColimitType F → s.pt := by +def descFun (s : Cocone F) : ColimitType.{w} F → s.pt := by fapply Quot.lift · exact descFunLift F s · intro x y r @@ -216,7 +216,7 @@ def descFun (s : Cocone F) : ColimitType F → s.pt := by #align AddCommGroup.colimits.desc_fun AddCommGroupCat.Colimits.descFun /-- The group homomorphism from the colimit abelian group to the cone point of any other cocone. -/ -def descMorphism (s : Cocone F) : colimit.{v} F ⟶ s.pt where +def descMorphism (s : Cocone F) : colimit.{w} F ⟶ s.pt where toFun := descFun F s map_zero' := rfl -- Porting note : in `mathlib3`, nothing needs to be done after `induction` @@ -224,7 +224,7 @@ def descMorphism (s : Cocone F) : colimit.{v} F ⟶ s.pt where #align AddCommGroup.colimits.desc_morphism AddCommGroupCat.Colimits.descMorphism /-- Evidence that the proposed colimit is the colimit. -/ -def colimitCoconeIsColimit : IsColimit (colimitCocone.{v} F) where +def colimitCoconeIsColimit : IsColimit (colimitCocone.{w} F) where desc s := descMorphism F s uniq s m w := FunLike.ext _ _ <| fun x => Quot.inductionOn x fun x => by change (m : ColimitType F →+ s.pt) _ = (descMorphism F s : ColimitType F →+ s.pt) _ @@ -241,15 +241,37 @@ def colimitCoconeIsColimit : IsColimit (colimitCocone.{v} F) where erw [m.map_add, (descMorphism F s).map_add, ihx, ihy] #align AddCommGroup.colimits.colimit_cocone_is_colimit AddCommGroupCat.Colimits.colimitCoconeIsColimit -instance hasColimits_addCommGroupCat : HasColimits AddCommGroupCat - where has_colimits_of_shape {_ _} := - { has_colimit := fun F => - HasColimit.mk - { cocone := colimitCocone F - isColimit := colimitCoconeIsColimit F } } -#align AddCommGroup.colimits.has_colimits_AddCommGroup AddCommGroupCat.Colimits.hasColimits_addCommGroupCat +end Colimits + +lemma hasColimit : HasColimit F := ⟨_, Colimits.colimitCoconeIsColimit.{w} F⟩ + +variable (J) -end AddCommGroupCat.Colimits +lemma hasColimitsOfShape : HasColimitsOfShape J AddCommGroupCat.{max u v w} where + has_colimit F := hasColimit.{w} F + +lemma hasColimitsOfSize : HasColimitsOfSize.{v, u} AddCommGroupCat.{max u v w} := + ⟨fun _ => hasColimitsOfShape.{w} _⟩ + +instance hasColimits : HasColimits AddCommGroupCat.{w} := hasColimitsOfSize.{w} +#align AddCommGroup.colimits.has_colimits_AddCommGroup AddCommGroupCat.hasColimits + +instance : HasColimitsOfSize.{v, v} (AddCommGroupCatMax.{u, v}) := hasColimitsOfSize.{u} +instance : HasColimitsOfSize.{u, u} (AddCommGroupCatMax.{u, v}) := hasColimitsOfSize.{v} +instance : HasColimitsOfSize.{u, v} (AddCommGroupCatMax.{u, v}) := hasColimitsOfSize.{u} +instance : HasColimitsOfSize.{v, u} (AddCommGroupCatMax.{u, v}) := hasColimitsOfSize.{u} +instance : HasColimitsOfSize.{0, 0} (AddCommGroupCat.{u}) := hasColimitsOfSize.{u, 0, 0} + +example : HasColimits AddCommGroupCatMax.{v, u} := + inferInstance + +example : HasColimits AddCommGroupCatMax.{u, v} := + inferInstance + +example : HasColimits AddCommGroupCat.{u} := + inferInstance + +end AddCommGroupCat namespace AddCommGroupCat diff --git a/Mathlib/Algebra/Category/GroupCat/Limits.lean b/Mathlib/Algebra/Category/GroupCat/Limits.lean index 6cba23b08ba73..a28b9739913f5 100644 --- a/Mathlib/Algebra/Category/GroupCat/Limits.lean +++ b/Mathlib/Algebra/Category/GroupCat/Limits.lean @@ -29,13 +29,6 @@ noncomputable section variable {J : Type v} [SmallCategory J] --- Porting note: typemax hack to fix universe complaints -/-- An alias for `GroupCat.{max u v}`, to deal around unification issues. -/ -@[to_additive (attr := nolint checkUnivs) - "An alias for `AddGroupCat.{max u v}`, to deal around unification issues."] -abbrev GroupCatMax.{u1, u2} := GroupCat.{max u1 u2} - - namespace GroupCat @[to_additive] @@ -218,12 +211,6 @@ set_option linter.uppercaseLean3 false in end GroupCat --- Porting note: typemax hack to fix universe complaints -/-- An alias for `CommGroupCat.{max u v}`, to deal around unification issues. -/ -@[to_additive (attr := nolint checkUnivs) - "An alias for `AddCommGroupCat.{max u v}`, to deal around unification issues."] -abbrev CommGroupCatMax.{u1, u2} := CommGroupCat.{max u1 u2} - namespace CommGroupCat @[to_additive] diff --git a/Mathlib/Algebra/Category/ModuleCat/Basic.lean b/Mathlib/Algebra/Category/ModuleCat/Basic.lean index 2b2fac5801945..140284c626e1f 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Basic.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Basic.lean @@ -79,14 +79,13 @@ structure ModuleCat where attribute [instance] ModuleCat.isAddCommGroup ModuleCat.isModule -namespace ModuleCat - --- Porting note: typemax hack to fix universe complaints /-- An alias for `ModuleCat.{max u₁ u₂}`, to deal around unification issues. Since the universe the ring lives in can be inferred, we put that last. -/ @[nolint checkUnivs] abbrev ModuleCatMax.{v₁, v₂, u₁} (R : Type u₁) [Ring R] := ModuleCat.{max v₁ v₂, u₁} R +namespace ModuleCat + instance : CoeSort (ModuleCat.{v} R) (Type v) := ⟨ModuleCat.carrier⟩ @@ -378,4 +377,98 @@ theorem Iso.conj_eq_conj (i : X ≅ X') (f : End X) : end +variable (M N : ModuleCat.{v} R) + +/-- The scalar multiplication on an object of `ModuleCat R` considered as +a morphism of rings from `R` to the endomorphisms of the underlying abelian group. -/ +def smul : R →+* End ((forget₂ (ModuleCat R) AddCommGroupCat).obj M) where + toFun r := + { toFun := fun (m : M) => r • m + map_zero' := by dsimp; rw [smul_zero] + map_add' := fun x y => by dsimp; rw [smul_add] } + map_one' := AddMonoidHom.ext (fun x => by dsimp; rw [one_smul]) + map_zero' := AddMonoidHom.ext (fun x => by dsimp; rw [zero_smul]) + map_mul' r s := AddMonoidHom.ext (fun (x : M) => (smul_smul r s x).symm) + map_add' r s := AddMonoidHom.ext (fun (x : M) => add_smul r s x) + +lemma smul_naturality {M N : ModuleCat.{v} R} (f : M ⟶ N) (r : R) : + (forget₂ (ModuleCat R) AddCommGroupCat).map f ≫ N.smul r = + M.smul r ≫ (forget₂ (ModuleCat R) AddCommGroupCat).map f := by + ext x + exact (f.map_smul r x).symm + +variable (R) + +/-- The scalar multiplication on `ModuleCat R` considered as a morphism of rings +to the endomorphisms of the forgetful functor to `AddCommGroupCat)`. -/ +@[simps] +def smulNatTrans : R →+* End (forget₂ (ModuleCat R) AddCommGroupCat) where + toFun r := + { app := fun M => M.smul r + naturality := fun _ _ _ => smul_naturality _ r } + map_one' := NatTrans.ext _ _ (by aesop_cat) + map_zero' := NatTrans.ext _ _ (by aesop_cat) + map_mul' _ _ := NatTrans.ext _ _ (by aesop_cat) + map_add' _ _ := NatTrans.ext _ _ (by aesop_cat) + +variable {R} + +/-- Given `A : AddCommGroupCat` and a ring morphism `R →+* End A`, this is a type synonym +for `A`, on which we shall define a structure of `R`-module. -/ +@[nolint unusedArguments] +def mkOfSMul' {A : AddCommGroupCat} (_ : R →+* End A) := A + +section + +variable {A : AddCommGroupCat} (φ : R →+* End A) + +instance : AddCommGroup (mkOfSMul' φ) := by + dsimp only [mkOfSMul'] + infer_instance + +instance : SMul R (mkOfSMul' φ) := ⟨fun r (x : A) => (show A ⟶ A from φ r) x⟩ + +@[simp] +lemma mkOfSMul'_smul (r : R) (x : mkOfSMul' φ) : + r • x = (show A ⟶ A from φ r) x := rfl + +instance : Module R (mkOfSMul' φ) where + smul_zero _ := map_zero _ + smul_add _ _ _ := map_add _ _ _ + one_smul := by simp + mul_smul := by simp + add_smul _ _ _ := by simp; rfl + zero_smul := by simp + +/-- Given `A : AddCommGroupCat` and a ring morphism `R →+* End A`, this is an object in +`ModuleCat R`, whose underlying abelian group is `A` and whose scalar multiplication is +given by `R`. -/ +abbrev mkOfSMul := ModuleCat.of R (mkOfSMul' φ) + +@[simp] +lemma mkOfSMul_smul (r : R) : (mkOfSMul φ).smul r = φ r := rfl + +end + +section + +variable {M N} + (φ : (forget₂ (ModuleCat R) AddCommGroupCat).obj M ⟶ + (forget₂ (ModuleCat R) AddCommGroupCat).obj N) + (hφ : ∀ (r : R), φ ≫ N.smul r = M.smul r ≫ φ) + +/-- Constructor for morphisms in `ModuleCat R` which takes as inputs +a morphism between the underlying objects in `AddCommGroupCat` and the compatibility +with the scalar multiplication. -/ +@[simps] +def homMk : M ⟶ N where + toFun := φ + map_add' _ _ := map_add _ _ _ + map_smul' r x := (congr_hom (hφ r) x).symm + +lemma forget₂_map_homMk : + (forget₂ (ModuleCat R) AddCommGroupCat).map (homMk φ hφ) = φ := rfl + +end + end ModuleCat diff --git a/Mathlib/Algebra/Category/ModuleCat/Colimits.lean b/Mathlib/Algebra/Category/ModuleCat/Colimits.lean index 61580afeed13d..315f16ad418ee 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Colimits.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Colimits.lean @@ -1,355 +1,127 @@ /- Copyright (c) 2019 Scott Morrison. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Scott Morrison +Authors: Scott Morrison, Joël Riou -/ import Mathlib.Algebra.Category.ModuleCat.Basic import Mathlib.CategoryTheory.ConcreteCategory.Elementwise +import Mathlib.Algebra.Category.GroupCat.Colimits #align_import algebra.category.Module.colimits from "leanprover-community/mathlib"@"5a684ce82399d820475609907c6ef8dba5b1b97c" /-! # The category of R-modules has all colimits. -This file uses a "pre-automated" approach, just as for `Mathlib.Algebra.Category.MonCat.Colimits`. +From the existence of colimits in `AddCommGroupCat`, we deduce the existence of colimits +in `ModuleCat R`. This way, we get for free that the functor +`forget₂ (ModuleCat R) AddCommGroupCat` commutes with colimits. Note that finite colimits can already be obtained from the instance `Abelian (Module R)`. TODO: -In fact, in `Module R` there is a much nicer model of colimits as quotients -of finitely supported functions, and we really should implement this as well (or instead). +In fact, in `ModuleCat R` there is a much nicer model of colimits as quotients +of finitely supported functions, and we really should implement this as well. -/ +universe w' w u v + +open CategoryTheory Category Limits + +variable {R : Type w} [Ring R] + +namespace ModuleCat + +variable {J : Type u} [Category.{v} J] (F : J ⥤ ModuleCat.{w'} R) + +namespace HasColimit + +variable [HasColimit (F ⋙ forget₂ _ AddCommGroupCat)] + +/-- The induced scalar multiplication on +`colimit (F ⋙ forget₂ _ AddCommGroupCat)`. -/ +@[simps] +noncomputable def coconePointSMul : + R →+* End (colimit (F ⋙ forget₂ _ AddCommGroupCat)) where + toFun r := colimMap + { app := fun j => (F.obj j).smul r + naturality := fun X Y f => smul_naturality _ _ } + map_zero' := colimit.hom_ext (by simp) + map_one' := colimit.hom_ext (by simp) + map_add' r s := colimit.hom_ext (fun j => by + simp only [Functor.comp_obj, forget₂_obj, map_add, ι_colimMap] + rw [Preadditive.add_comp, Preadditive.comp_add] + simp only [ι_colimMap, Functor.comp_obj, forget₂_obj]) + map_mul' r s := colimit.hom_ext (fun j => by simp) + +/-- The cocone for `F` constructed from the colimit of +`(F ⋙ forget₂ (ModuleCat R) AddCommGroupCat)`. -/ +@[simps] +noncomputable def colimitCocone : Cocone F where + pt := mkOfSMul (coconePointSMul F) + ι := + { app := fun j => homMk (colimit.ι (F ⋙ forget₂ _ AddCommGroupCat) j) (fun r => by + dsimp + rw [mkOfSMul_smul] + simp) + naturality := fun i j f => by + apply (forget₂ _ AddCommGroupCat).map_injective + simp only [Functor.map_comp, forget₂_map_homMk] + dsimp + erw [colimit.w (F ⋙ forget₂ _ AddCommGroupCat), comp_id] } + +/-- The cocone for `F` constructed from the colimit of +`(F ⋙ forget₂ (ModuleCat R) AddCommGroupCat)` is a colimit cocone. -/ +noncomputable def isColimitColimitCocone : IsColimit (colimitCocone F) where + desc s := homMk (colimit.desc _ ((forget₂ _ AddCommGroupCat).mapCocone s)) (fun r => by + apply colimit.hom_ext + intro j + dsimp + rw [colimit.ι_desc_assoc] + rw [mkOfSMul_smul] + dsimp + simp only [ι_colimMap_assoc, Functor.comp_obj, forget₂_obj, colimit.ι_desc, + Functor.mapCocone_pt, Functor.mapCocone_ι_app, forget₂_map] + exact smul_naturality (s.ι.app j) r) + fac s j := by + apply (forget₂ _ AddCommGroupCat).map_injective + exact colimit.ι_desc ((forget₂ _ AddCommGroupCat).mapCocone s) j + uniq s m hm := by + apply (forget₂ _ AddCommGroupCat).map_injective + apply colimit.hom_ext + intro j + erw [colimit.ι_desc ((forget₂ _ AddCommGroupCat).mapCocone s) j] + dsimp + rw [← hm] + rfl -universe u v w +instance : HasColimit F := ⟨_, isColimitColimitCocone F⟩ -open CategoryTheory +noncomputable instance : PreservesColimit F (forget₂ _ AddCommGroupCat) := + preservesColimitOfPreservesColimitCocone (isColimitColimitCocone F) (colimit.isColimit _) -open CategoryTheory.Limits +end HasColimit -variable {R : Type u} [Ring R] +variable (J R) --- [ROBOT VOICE]: --- You should pretend for now that this file was automatically generated. --- It follows the same template as colimits in Mon. -namespace ModuleCat.Colimits - -/-! -We build the colimit of a diagram in `Module` by constructing the -free group on the disjoint union of all the abelian groups in the diagram, -then taking the quotient by the abelian group laws within each abelian group, -and the identifications given by the morphisms in the diagram. --/ +instance hasColimitsOfShape [HasColimitsOfShape J AddCommGroupCat.{w'}] : + HasColimitsOfShape J (ModuleCat.{w'} R) where +instance hasColimitsOfSize [HasColimitsOfSize.{v, u} AddCommGroupCat.{w'}] : + HasColimitsOfSize.{v, u} (ModuleCat.{w'} R) where -variable {J : Type w} [Category.{v} J] (F : J ⥤ ModuleCat.{max u v w} R) +noncomputable instance forget₂PreservesColimitsOfShape + [HasColimitsOfShape J AddCommGroupCat.{w'}] : + PreservesColimitsOfShape J (forget₂ (ModuleCat.{w'} R) AddCommGroupCat) where -/-- An inductive type representing all module expressions (without relations) -on a collection of types indexed by the objects of `J`. --/ -inductive Prequotient - -- There's always `of` - | of : ∀ (j : J) (_ : F.obj j), Prequotient - -- Then one generator for each operation - | zero : Prequotient - | neg : Prequotient → Prequotient - | add : Prequotient → Prequotient → Prequotient - | smul : R → Prequotient → Prequotient -set_option linter.uppercaseLean3 false in -#align Module.colimits.prequotient ModuleCat.Colimits.Prequotient - -instance : Inhabited (Prequotient F) := - ⟨Prequotient.zero⟩ - -open Prequotient - -/-- The relation on `Prequotient` saying when two expressions are equal -because of the module laws, or -because one element is mapped to another by a morphism in the diagram. --/ -inductive Relation : Prequotient F → Prequotient F → Prop - -- Make it an equivalence relation: - | refl : ∀ x, Relation x x - | symm : ∀ (x y) (_ : Relation x y), Relation y x - | trans : ∀ (x y z) (_ : Relation x y) (_ : Relation y z), Relation x z - -- There's always a `map` Relation - | map : ∀ (j j' : J) (f : j ⟶ j') (x : F.obj j), - Relation (Prequotient.of j' (F.map f x)) (Prequotient.of j x) - -- Then one Relation per operation, describing the interaction with `of` - | zero : ∀ j, Relation (Prequotient.of j 0) zero - | neg : ∀ (j) (x : F.obj j), - Relation (Prequotient.of j (-x)) (neg (Prequotient.of j x)) - | add : ∀ (j) (x y : F.obj j), - Relation (Prequotient.of j (x + y)) (add (Prequotient.of j x) (Prequotient.of j y)) - | smul : ∀ (j) (s) (x : F.obj j), - Relation (Prequotient.of j (s • x)) (smul s (Prequotient.of j x)) - -- Then one Relation per argument of each operation - | neg_1 : ∀ (x x') (_ : Relation x x'), Relation (neg x) (neg x') - | add_1 : ∀ (x x' y) (_ : Relation x x'), Relation (add x y) (add x' y) - | add_2 : ∀ (x y y') (_ : Relation y y'), Relation (add x y) (add x y') - | smul_1 : ∀ (s) (x x') (_ : Relation x x'), Relation (smul s x) (smul s x') - -- And one Relation per axiom - | zero_add : ∀ x, Relation (add zero x) x - | add_zero : ∀ x, Relation (add x zero) x - | add_left_neg : ∀ x, Relation (add (neg x) x) zero - | add_comm : ∀ x y, Relation (add x y) (add y x) - | add_assoc : ∀ x y z, Relation (add (add x y) z) (add x (add y z)) - | one_smul : ∀ x, Relation (smul 1 x) x - | mul_smul : ∀ s t x, Relation (smul (s * t) x) (smul s (smul t x)) - | smul_add : ∀ s x y, Relation (smul s (add x y)) (add (smul s x) (smul s y)) - | smul_zero : ∀ s, Relation (smul s zero) zero - | add_smul : ∀ s t x, Relation (smul (s + t) x) (add (smul s x) (smul t x)) - | zero_smul : ∀ x, Relation (smul 0 x) zero -set_option linter.uppercaseLean3 false in -#align Module.colimits.relation ModuleCat.Colimits.Relation - -/-- The setoid corresponding to module expressions modulo module relations and identifications. --/ -def colimitSetoid : Setoid (Prequotient F) where - r := Relation F - iseqv := ⟨Relation.refl, Relation.symm _ _, Relation.trans _ _ _⟩ -set_option linter.uppercaseLean3 false in -#align Module.colimits.colimit_setoid ModuleCat.Colimits.colimitSetoid +noncomputable instance forget₂PreservesColimitsOfSize + [HasColimitsOfSize.{u, v} AddCommGroupCat.{w'}] : + PreservesColimitsOfSize.{u, v} (forget₂ (ModuleCat.{w'} R) AddCommGroupCat) where -attribute [instance] colimitSetoid +noncomputable instance + [HasColimitsOfSize.{u, v} AddCommGroupCatMax.{w, w'}] : + PreservesColimitsOfSize.{u, v} (forget₂ (ModuleCatMax.{w, w'} R) AddCommGroupCat) where -/-- The underlying type of the colimit of a diagram in `Module R`. --/ -def ColimitType : Type max u v w := - Quotient (colimitSetoid F) -set_option linter.uppercaseLean3 false in -#align Module.colimits.colimit_type ModuleCat.Colimits.ColimitType - -instance : Inhabited (ColimitType F) := ⟨Quot.mk _ <| .zero⟩ - -instance : AddCommGroup (ColimitType F) where - zero := Quotient.mk _ zero - neg := Quotient.map neg Relation.neg_1 - add := Quotient.map₂ add <| fun x x' rx y y' ry => - Setoid.trans (Relation.add_1 _ _ y rx) (Relation.add_2 x' _ _ ry) - zero_add := Quotient.ind <| fun _ => Quotient.sound <| Relation.zero_add _ - add_zero := Quotient.ind <| fun _ => Quotient.sound <| Relation.add_zero _ - add_left_neg := Quotient.ind <| fun _ => Quotient.sound <| Relation.add_left_neg _ - add_comm := Quotient.ind₂ <| fun _ _ => Quotient.sound <| Relation.add_comm _ _ - add_assoc := Quotient.ind <| fun _ => Quotient.ind₂ <| fun _ _ => - Quotient.sound <| Relation.add_assoc _ _ _ - -instance : Module R (ColimitType F) where - smul s := Quotient.map (smul s) <| Relation.smul_1 s - one_smul := Quotient.ind <| fun _ => Quotient.sound <| Relation.one_smul _ - mul_smul _s _r := Quotient.ind <| fun _ => Quotient.sound <| Relation.mul_smul _ _ _ - smul_add _s := Quotient.ind₂ <| fun _ _ => Quotient.sound <| Relation.smul_add _ _ _ - smul_zero _s := Quotient.sound <| Relation.smul_zero _ - add_smul _s _t := Quotient.ind <| fun _ => Quotient.sound <| Relation.add_smul _ _ _ - zero_smul := Quotient.ind <| fun _ => Quotient.sound <| Relation.zero_smul _ - -@[simp] -theorem quot_zero : Quot.mk Setoid.r zero = (0 : ColimitType F) := - rfl -set_option linter.uppercaseLean3 false in -#align Module.colimits.quot_zero ModuleCat.Colimits.quot_zero - -def ColimitType.mk {F : J ⥤ ModuleCat R} (x : Prequotient F) : ColimitType F := Quot.mk Setoid.r x - -@[simp] -theorem quot_neg (x) : Quot.mk Setoid.r (neg x) = (-ColimitType.mk x : ColimitType F) := - rfl -set_option linter.uppercaseLean3 false in -#align Module.colimits.quot_neg ModuleCat.Colimits.quot_neg - -@[simp] -theorem quot_add (x y) : - Quot.mk Setoid.r (add x y) = (ColimitType.mk x + ColimitType.mk y : ColimitType F) := - rfl -set_option linter.uppercaseLean3 false in -#align Module.colimits.quot_add ModuleCat.Colimits.quot_add - -@[simp] -theorem quot_smul (s x) : Quot.mk Setoid.r (smul s x) = (s • ColimitType.mk x : ColimitType F) := - rfl -set_option linter.uppercaseLean3 false in -#align Module.colimits.quot_smul ModuleCat.Colimits.quot_smul - -/-- The bundled module giving the colimit of a diagram. -/ -def colimit : ModuleCat R := - ModuleCat.of R (ColimitType F) -set_option linter.uppercaseLean3 false in -#align Module.colimits.colimit ModuleCat.Colimits.colimit - -/-- The function from a given module in the diagram to the colimit module. -/ -def coconeFun (j : J) (x : F.obj j) : ColimitType F := - Quot.mk _ (Prequotient.of j x) -set_option linter.uppercaseLean3 false in -#align Module.colimits.cocone_fun ModuleCat.Colimits.coconeFun - -/-- The group homomorphism from a given module in the diagram to the colimit module. -/ -def coconeMorphism (j : J) : F.obj j ⟶ colimit F where - toFun := coconeFun F j - map_smul' := by intros; apply Quot.sound; apply Relation.smul - map_add' := by intros; apply Quot.sound; apply Relation.add -set_option linter.uppercaseLean3 false in -#align Module.colimits.cocone_morphism ModuleCat.Colimits.coconeMorphism - -@[simp] -theorem cocone_naturality {j j' : J} (f : j ⟶ j') : - F.map f ≫ coconeMorphism F j' = coconeMorphism F j := by - ext - apply Quot.sound - apply ModuleCat.Colimits.Relation.map -set_option linter.uppercaseLean3 false in -#align Module.colimits.cocone_naturality ModuleCat.Colimits.cocone_naturality - -@[simp] -theorem cocone_naturality_components (j j' : J) (f : j ⟶ j') (x : F.obj j) : - (coconeMorphism F j') (F.map f x) = (coconeMorphism F j) x := by - rw [← cocone_naturality F f] - rfl -set_option linter.uppercaseLean3 false in -#align Module.colimits.cocone_naturality_components ModuleCat.Colimits.cocone_naturality_components - -/-- The cocone over the proposed colimit module. -/ -def colimitCocone : Cocone F where - pt := colimit F - ι := { app := coconeMorphism F } -set_option linter.uppercaseLean3 false in -#align Module.colimits.colimit_cocone ModuleCat.Colimits.colimitCocone - -/-- The function from the free module on the diagram to the cone point of any other cocone. -/ -@[simp] -def descFunLift (s : Cocone F) : Prequotient F → s.pt - | Prequotient.of j x => (s.ι.app j) x - | zero => 0 - | neg x => -descFunLift _ x - | add x y => descFunLift _ x + descFunLift _ y - | smul s x => s • descFunLift _ x -set_option linter.uppercaseLean3 false in -#align Module.colimits.desc_fun_lift ModuleCat.Colimits.descFunLift - -/-- The function from the colimit module to the cone point of any other cocone. -/ -def descFun (s : Cocone F) : ColimitType F → s.pt := by - fapply Quot.lift - · exact descFunLift F s - · intro x y r - induction' r with h₁ r_x r_y r_h r_ih r_x r_y r_z r_h r_k r_ih_h r_ih_k r_j r_j' r_f r_x j j x - j x y j s x u v r r_ih u v w r r_ih u v w r r_ih s u v r r_ih <;> try dsimp - -- refl - -- · rfl -- porting note: `dsimp` (above) now closes this - -- symm - · exact r_ih.symm - -- trans - · exact Eq.trans r_ih_h r_ih_k - -- map - · exact s.w_apply r_f r_x -- porting note: `simp` failed - -- zero - · simp - -- neg - · simp - -- add - · simp - -- smul, - · simp - -- neg_1 - · rw [r_ih] - -- add_1 - · rw [r_ih] - -- add_2 - · rw [r_ih] - -- smul_1 - · rw [r_ih] - -- zero_add - · rw [zero_add] - -- add_zero - · rw [add_zero] - -- add_left_neg - · rw [add_left_neg] - -- add_comm - · rw [add_comm] - -- add_assoc - · rw [add_assoc] - -- one_smul - · rw [one_smul] - -- mul_smul - · rw [mul_smul] - -- smul_add - · rw [smul_add] - -- smul_zero - · rw [smul_zero] - -- add_smul - · rw [add_smul] - -- zero_smul - · rw [zero_smul] -set_option linter.uppercaseLean3 false in -#align Module.colimits.desc_fun ModuleCat.Colimits.descFun - -/-- The group homomorphism from the colimit module to the cone point of any other cocone. -/ -def descMorphism (s : Cocone F) : colimit F ⟶ s.pt where - toFun := descFun F s - map_smul' s x := by rcases x; rfl - map_add' x y := by rcases x; rcases y; rfl -set_option linter.uppercaseLean3 false in -#align Module.colimits.desc_morphism ModuleCat.Colimits.descMorphism - -/-- Evidence that the proposed colimit is the colimit. -/ -def colimitCoconeIsColimit : IsColimit (colimitCocone F) where - desc s := descMorphism F s - uniq s m w := by - ext x - -- porting note: was `induction x` but now need `Quot.rec` with explicit `motive` - refine Quot.rec (motive := fun x ↦ m x = _) (fun x ↦ ?_) (fun x_a x_b x_p ↦ ?_) x - dsimp - induction' x with x_j x_x - · have w' := - congr_fun (congr_arg (fun f : F.obj x_j ⟶ s.pt => (f : F.obj x_j → s.pt)) (w x_j)) x_x - simp only at w' - erw [w'] - rfl - · rw [quot_zero, map_zero] -- porting note: was `simp` but `map_zero` won't fire - rfl - · simpa - · rw [quot_add, map_add, map_add] -- porting note: this was closed by `simp [*]` - congr 1 - · rw [quot_smul, map_smul, map_smul] -- porting note: this was closed by `simp [*]` - congr 1 - · rfl -- porting note: this wasn't here -set_option linter.uppercaseLean3 false in -#align Module.colimits.colimit_cocone_is_colimit ModuleCat.Colimits.colimitCoconeIsColimit - -instance hasColimits_moduleCat : HasColimits (ModuleCatMax.{v, u, u} R) - where has_colimits_of_shape _ _ := - { has_colimit := fun F => - HasColimit.mk - { cocone := colimitCocone F - isColimit := colimitCoconeIsColimit F } } -set_option linter.uppercaseLean3 false in -#align Module.colimits.has_colimits_Module ModuleCat.Colimits.hasColimits_moduleCat - -instance hasColimitsOfSize_moduleCat : HasColimitsOfSize.{v, v} (ModuleCatMax.{v, u, u} R) := - hasColimitsOfSize_shrink.{v, v, u, u} _ -set_option linter.uppercaseLean3 false in -#align Module.colimits.has_colimits_of_size_Module ModuleCat.Colimits.hasColimitsOfSize_moduleCat - -instance hasColimitsOfSize_zero_moduleCat : HasColimitsOfSize.{0, 0} (ModuleCatMax.{v, u, u} R) := - -- Porting note: had to specify further universes. - hasColimitsOfSize_shrink.{0, 0, v, v} (ModuleCatMax.{v, u, u} R) -set_option linter.uppercaseLean3 false in -#align Module.colimits.has_colimits_of_size_zero_Module ModuleCat.Colimits.hasColimitsOfSize_zero_moduleCat - --- Porting note: in mathlib3 it was helpful to add to more instances with specialised universes. --- However in Lean 4 they *break*, rather than *enable*, the examples below. - --- -- We manually add a `has_colimits` instance with universe parameters swapped, for otherwise --- -- the instance is not found by typeclass search. --- instance hasColimits_Module' (R : Type u) [Ring R] : HasColimits (ModuleCatMax.{u, v, u} R) := --- ModuleCat.Colimits.hasColimits_moduleCat.{u, v} --- set_option linter.uppercaseLean3 false in --- #align Module.colimits.has_colimits_Module' ModuleCat.Colimits.hasColimits_Module' - --- -- We manually add a `has_colimits` instance with equal universe parameters, for otherwise --- -- the instance is not found by typeclass search. --- instance hasColimits_Module'' (R : Type u) [Ring R] : HasColimits (ModuleCat.{u} R) := --- ModuleCat.Colimits.hasColimits_moduleCat.{u, u} --- set_option linter.uppercaseLean3 false in --- #align Module.colimits.has_colimits_Module'' ModuleCat.Colimits.hasColimits_Module'' +instance : HasFiniteColimits (ModuleCat.{w'} R) := inferInstance -- Sanity checks, just to make sure typeclass search can find the instances we want. example (R : Type u) [Ring R] : HasColimits (ModuleCatMax.{v, u} R) := @@ -361,4 +133,13 @@ example (R : Type u) [Ring R] : HasColimits (ModuleCatMax.{u, v} R) := example (R : Type u) [Ring R] : HasColimits (ModuleCat.{u} R) := inferInstance -end ModuleCat.Colimits +example (R : Type u) [Ring R] : HasCoequalizers (ModuleCat.{u} R) := by + infer_instance + +-- for some reason, this instance is not found automatically later on +instance : HasCoequalizers (ModuleCat.{v} R) where + +noncomputable example (R : Type u) [Ring R] : + PreservesColimits (forget₂ (ModuleCat.{u} R) AddCommGroupCat) := inferInstance + +end ModuleCat diff --git a/Mathlib/Algebra/Homology/LocalCohomology.lean b/Mathlib/Algebra/Homology/LocalCohomology.lean index 68d6251810ed1..564d3a589dd28 100644 --- a/Mathlib/Algebra/Homology/LocalCohomology.lean +++ b/Mathlib/Algebra/Homology/LocalCohomology.lean @@ -94,6 +94,11 @@ section -- along diagrams either in Type, or in the same universe as the ring, and we need to cover both. variable {R : Type max u v} [CommRing R] {D : Type v} [SmallCategory D] +lemma hasColimitDiagram (I : D ⥤ Ideal R) (i : ℕ) : + HasColimit (diagram I i) := by + have : HasColimitsOfShape Dᵒᵖ (AddCommGroupCatMax.{u, v}) := inferInstance + infer_instance + /- In this definition we do not assume any special property of the diagram `I`, but the relevant case will be where `I` is (cofinal with) the diagram of powers of a single given ideal. @@ -104,8 +109,9 @@ in an ideal `J`, `localCohomology` and `localCohomology.ofSelfLERadical`. /-- `localCohomology.ofDiagram I i` is the functor sending a module `M` over a commutative ring `R` to the direct limit of `Ext^i(R/J, M)`, where `J` ranges over a collection of ideals of `R`, represented as a functor `I`. -/ -def ofDiagram (I : D ⥤ Ideal R) (i : ℕ) : ModuleCat.{max u v} R ⥤ ModuleCat.{max u v} R := - colimit (diagram.{max u v, v} I i) +def ofDiagram (I : D ⥤ Ideal R) (i : ℕ) : ModuleCatMax.{u, v} R ⥤ ModuleCatMax.{u, v} R := + have := hasColimitDiagram.{u, v} I i + colimit (diagram I i) #align local_cohomology.of_diagram localCohomology.ofDiagram end @@ -123,9 +129,12 @@ def diagramComp (i : ℕ) : diagram (I' ⋙ I) i ≅ I'.op ⋙ diagram I i := #align local_cohomology.diagram_comp localCohomology.diagramComp /-- Local cohomology agrees along precomposition with a cofinal diagram. -/ +@[nolint unusedHavesSuffices] def isoOfFinal [Functor.Initial I'] (i : ℕ) : ofDiagram.{max u v, v'} (I' ⋙ I) i ≅ ofDiagram.{max u v', v} I i := - HasColimit.isoOfNatIso (diagramComp.{u} _ _ _) ≪≫ Functor.Final.colimitIso _ _ + have := hasColimitDiagram.{max u v', v} I i + have := hasColimitDiagram.{max u v, v'} (I' ⋙ I) i + HasColimit.isoOfNatIso (diagramComp.{u} I' I i) ≪≫ Functor.Final.colimitIso _ _ #align local_cohomology.iso_of_final localCohomology.isoOfFinal end @@ -247,11 +256,6 @@ instance ideal_powers_initial [hR : IsNoetherian R R] : left; exact ⟨CostructuredArrow.homMk (homOfLE h).op (AsTrue.get trivial)⟩ #align local_cohomology.ideal_powers_initial localCohomology.ideal_powers_initial --- FIXME again, this instance is not found by `inferInstance`, but `#synth` finds it just fine. --- #synth HasColimitsOfSize.{0, 0, u, u + 1} (ModuleCat.{u, u} R) -instance : HasColimitsOfSize.{0, 0, u, u + 1} (ModuleCat.{u, u} R) := - ModuleCat.Colimits.hasColimitsOfSize_zero_moduleCat.{u, u} - example : HasColimitsOfSize.{0, 0, u, u + 1} (ModuleCat.{u, u} R) := inferInstance /-- Local cohomology (defined in terms of powers of `J`) agrees with local cohomology computed over all ideals with radical containing `J`. -/