bump to nightly-2023-06-26-03

mathlib commit leanprover-community/mathlib@fdc286c

Mathbin/Algebra/Category/Mon/Colimits.lean

@@ -52,6 +52,7 @@ and the identifications given by the morphisms in the diagram.
 
 variable {J : Type v} [SmallCategory J] (F : J ⥤ MonCat.{v})
 
+#print MonCat.Colimits.Prequotient /-
 /-- An inductive type representing all monoid expressions (without relations)
 on a collection of types indexed by the objects of `J`.
 -/
@@ -62,12 +63,14 @@ inductive Prequotient-- There's always `of`
   | one : prequotient
   | mul : prequotient → prequotient → prequotient
 #align Mon.colimits.prequotient MonCat.Colimits.Prequotient
+-/
 
 instance : Inhabited (Prequotient F) :=
   ⟨Prequotient.one⟩
 
 open Prequotient
 
+#print MonCat.Colimits.Relation /-
 /-- The relation on `prequotient` saying when two expressions are equal
 because of the monoid laws, or
 because one element is mapped to another by a morphism in the diagram.
@@ -97,24 +100,30 @@ inductive Relation : Prequotient F → Prequotient F → Prop-- Make it an equiv
   | one_mul : ∀ x, relation (mul one x) x
   | mul_one : ∀ x, relation (mul x one) x
 #align Mon.colimits.relation MonCat.Colimits.Relation
+-/
 
+#print MonCat.Colimits.colimitSetoid /-
 /-- The setoid corresponding to monoid expressions modulo monoid relations and identifications.
 -/
 def colimitSetoid : Setoid (Prequotient F)
     where
   R := Relation F
   iseqv := ⟨Relation.refl, Relation.symm, Relation.trans⟩
 #align Mon.colimits.colimit_setoid MonCat.Colimits.colimitSetoid
+-/
 
 attribute [instance] colimit_setoid
 
+#print MonCat.Colimits.ColimitType /-
 /-- The underlying type of the colimit of a diagram in `Mon`.
 -/
 def ColimitType : Type v :=
   Quotient (colimitSetoid F)
 deriving Inhabited
 #align Mon.colimits.colimit_type MonCat.Colimits.ColimitType
+-/
 
+#print MonCat.Colimits.monoidColimitType /-
 instance monoidColimitType : Monoid (ColimitType F)
     where
   mul := by
@@ -157,36 +166,48 @@ instance monoidColimitType : Monoid (ColimitType F)
     apply relation.mul_one
     rfl
 #align Mon.colimits.monoid_colimit_type MonCat.Colimits.monoidColimitType
+-/
 
+#print MonCat.Colimits.quot_one /-
 @[simp]
 theorem quot_one : Quot.mk Setoid.r one = (1 : ColimitType F) :=
   rfl
 #align Mon.colimits.quot_one MonCat.Colimits.quot_one
+-/
 
+#print MonCat.Colimits.quot_mul /-
 @[simp]
 theorem quot_mul (x y) :
     Quot.mk Setoid.r (mul x y) = (Quot.mk Setoid.r x * Quot.mk Setoid.r y : ColimitType F) :=
   rfl
 #align Mon.colimits.quot_mul MonCat.Colimits.quot_mul
+-/
 
+#print MonCat.Colimits.colimit /-
 /-- The bundled monoid giving the colimit of a diagram. -/
 def colimit : MonCat :=
   ⟨ColimitType F, by infer_instance⟩
 #align Mon.colimits.colimit MonCat.Colimits.colimit
+-/
 
+#print MonCat.Colimits.coconeFun /-
 /-- The function from a given monoid in the diagram to the colimit monoid. -/
 def coconeFun (j : J) (x : F.obj j) : ColimitType F :=
   Quot.mk _ (of j x)
 #align Mon.colimits.cocone_fun MonCat.Colimits.coconeFun
+-/
 
+#print MonCat.Colimits.coconeMorphism /-
 /-- The monoid homomorphism from a given monoid in the diagram to the colimit monoid. -/
 def coconeMorphism (j : J) : F.obj j ⟶ colimit F
     where
   toFun := coconeFun F j
   map_one' := Quot.sound (Relation.one _)
   map_mul' x y := Quot.sound (Relation.mul _ _ _)
 #align Mon.colimits.cocone_morphism MonCat.Colimits.coconeMorphism
+-/
 
+#print MonCat.Colimits.cocone_naturality /-
 @[simp]
 theorem cocone_naturality {j j' : J} (f : j ⟶ j') :
     F.map f ≫ coconeMorphism F j' = coconeMorphism F j :=
@@ -195,27 +216,35 @@ theorem cocone_naturality {j j' : J} (f : j ⟶ j') :
   apply Quot.sound
   apply Relation.Map
 #align Mon.colimits.cocone_naturality MonCat.Colimits.cocone_naturality
+-/
 
+#print MonCat.Colimits.cocone_naturality_components /-
 @[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
 #align Mon.colimits.cocone_naturality_components MonCat.Colimits.cocone_naturality_components
+-/
 
+#print MonCat.Colimits.colimitCocone /-
 /-- The cocone over the proposed colimit monoid. -/
 def colimitCocone : Cocone F where
   pt := colimit F
   ι := { app := coconeMorphism F }
 #align Mon.colimits.colimit_cocone MonCat.Colimits.colimitCocone
+-/
 
+#print MonCat.Colimits.descFunLift /-
 /-- The function from the free monoid on the diagram to the cone point of any other cocone. -/
 @[simp]
 def descFunLift (s : Cocone F) : Prequotient F → s.pt
   | of j x => (s.ι.app j) x
   | one => 1
   | mul x y => desc_fun_lift x * desc_fun_lift y
 #align Mon.colimits.desc_fun_lift MonCat.Colimits.descFunLift
+-/
 
+#print MonCat.Colimits.descFun /-
 /-- The function from the colimit monoid to the cone point of any other cocone. -/
 def descFun (s : Cocone F) : ColimitType F → s.pt :=
   by
@@ -246,15 +275,19 @@ def descFun (s : Cocone F) : ColimitType F → s.pt :=
     -- mul_one
     · rw [mul_one]
 #align Mon.colimits.desc_fun MonCat.Colimits.descFun
+-/
 
+#print MonCat.Colimits.descMorphism /-
 /-- The monoid homomorphism from the colimit monoid to the cone point of any other cocone. -/
 def descMorphism (s : Cocone F) : colimit F ⟶ s.pt
     where
   toFun := descFun F s
   map_one' := rfl
   map_mul' x y := by induction x <;> induction y <;> rfl
 #align Mon.colimits.desc_morphism MonCat.Colimits.descMorphism
+-/
 
+#print MonCat.Colimits.colimitIsColimit /-
 /-- Evidence that the proposed colimit is the colimit. -/
 def colimitIsColimit : IsColimit (colimitCocone F)
     where
@@ -271,7 +304,9 @@ def colimitIsColimit : IsColimit (colimitCocone F)
     · simp [*]
     rfl
 #align Mon.colimits.colimit_is_colimit MonCat.Colimits.colimitIsColimit
+-/
 
+#print MonCat.Colimits.hasColimits_monCat /-
 instance hasColimits_monCat : HasColimits MonCat
     where HasColimitsOfShape J 𝒥 :=
     {
@@ -280,6 +315,7 @@ instance hasColimits_monCat : HasColimits MonCat
           { Cocone := colimit_cocone F
             IsColimit := colimit_is_colimit F } }
 #align Mon.colimits.has_colimits_Mon MonCat.Colimits.hasColimits_monCat
+-/
 
 end MonCat.Colimits
 

Mathbin/Algebra/Homology/LocalCohomology.lean

@@ -79,11 +79,11 @@ def ringModIdeals (I : D ⥤ Ideal R) : D ⥤ ModuleCat.{u} R
 #align local_cohomology.ring_mod_ideals localCohomology.ringModIdeals
 -/
 
-#print localCohomology.moduleCat_enough_projectives' /-
+#print localCohomology.moduleCat_enoughProjectives' /-
 -- TODO:  Once this file is ported, move this file to the right location.
-instance moduleCat_enough_projectives' : EnoughProjectives (ModuleCat.{u} R) :=
+instance moduleCat_enoughProjectives' : EnoughProjectives (ModuleCat.{u} R) :=
   ModuleCat.moduleCat_enoughProjectives.{u}
-#align local_cohomology.Module_enough_projectives' localCohomology.moduleCat_enough_projectives'
+#align local_cohomology.Module_enough_projectives' localCohomology.moduleCat_enoughProjectives'
 -/
 
 #print localCohomology.diagram /-
@@ -153,26 +153,26 @@ def idealPowersDiagram (J : Ideal R) : ℕᵒᵖ ⥤ Ideal R
 #align local_cohomology.ideal_powers_diagram localCohomology.idealPowersDiagram
 -/
 
-#print localCohomology.SelfLeRadical /-
+#print localCohomology.SelfLERadical /-
 /-- The full subcategory of all ideals with radical containing `J` -/
-def SelfLeRadical (J : Ideal R) : Type u :=
+def SelfLERadical (J : Ideal R) : Type u :=
   FullSubcategory fun J' : Ideal R => J ≤ J'.radical
 deriving Category
-#align local_cohomology.self_le_radical localCohomology.SelfLeRadical
+#align local_cohomology.self_le_radical localCohomology.SelfLERadical
 -/
 
-#print localCohomology.SelfLeRadical.inhabited /-
-instance SelfLeRadical.inhabited (J : Ideal R) : Inhabited (SelfLeRadical J)
+#print localCohomology.SelfLERadical.inhabited /-
+instance SelfLERadical.inhabited (J : Ideal R) : Inhabited (SelfLERadical J)
     where default := ⟨J, Ideal.le_radical⟩
-#align local_cohomology.self_le_radical.inhabited localCohomology.SelfLeRadical.inhabited
+#align local_cohomology.self_le_radical.inhabited localCohomology.SelfLERadical.inhabited
 -/
 
-#print localCohomology.selfLeRadicalDiagram /-
+#print localCohomology.selfLERadicalDiagram /-
 /-- The diagram of all ideals with radical containing `J`, represented as a functor.
 This is the "largest" diagram that computes local cohomology with support in `J`. -/
-def selfLeRadicalDiagram (J : Ideal R) : SelfLeRadical J ⥤ Ideal R :=
+def selfLERadicalDiagram (J : Ideal R) : SelfLERadical J ⥤ Ideal R :=
   fullSubcategoryInclusion _
-#align local_cohomology.self_le_radical_diagram localCohomology.selfLeRadicalDiagram
+#align local_cohomology.self_le_radical_diagram localCohomology.selfLERadicalDiagram
 -/
 
 end Diagrams
@@ -199,12 +199,12 @@ def localCohomology (J : Ideal R) (i : ℕ) : ModuleCat.{u} R ⥤ ModuleCat.{u}
 #align local_cohomology localCohomology
 -/
 
-#print localCohomology.ofSelfLeRadical /-
+#print localCohomology.ofSelfLERadical /-
 /-- Local cohomology as the direct limit of `Ext^i(R/J', M)` over *all* ideals `J'` with radical
 containing `J`. -/
-def localCohomology.ofSelfLeRadical (J : Ideal R) (i : ℕ) : ModuleCat.{u} R ⥤ ModuleCat.{u} R :=
-  ofDiagram.{u} (selfLeRadicalDiagram.{u} J) i
-#align local_cohomology.of_self_le_radical localCohomology.ofSelfLeRadical
+def localCohomology.ofSelfLERadical (J : Ideal R) (i : ℕ) : ModuleCat.{u} R ⥤ ModuleCat.{u} R :=
+  ofDiagram.{u} (selfLERadicalDiagram.{u} J) i
+#align local_cohomology.of_self_le_radical localCohomology.ofSelfLERadical
 -/
 
 end ModelsForLocalCohomology
@@ -224,17 +224,17 @@ section LocalCohomologyEquiv
 
 variable {R : Type u} [CommRing R]
 
-#print localCohomology.idealPowersToSelfLeRadical /-
+#print localCohomology.idealPowersToSelfLERadical /-
 /-- Lifting `ideal_powers_diagram J` from a diagram valued in `ideals R` to a diagram
 valued in `self_le_radical J`. -/
-def idealPowersToSelfLeRadical (J : Ideal R) : ℕᵒᵖ ⥤ SelfLeRadical J :=
+def idealPowersToSelfLERadical (J : Ideal R) : ℕᵒᵖ ⥤ SelfLERadical J :=
   FullSubcategory.lift _ (idealPowersDiagram J) fun k =>
     by
     change _ ≤ (J ^ unop k).radical
     cases unop k
     · simp only [Ideal.radical_top, pow_zero, Ideal.one_eq_top, le_top]
     · simp only [J.radical_pow _ n.succ_pos, Ideal.le_radical]
-#align local_cohomology.ideal_powers_to_self_le_radical localCohomology.idealPowersToSelfLeRadical
+#align local_cohomology.ideal_powers_to_self_le_radical localCohomology.idealPowersToSelfLERadical
 -/
 
 variable {I J K : Ideal R}
@@ -255,7 +255,7 @@ theorem Ideal.exists_pow_le_of_le_radical_of_fG (hIJ : I ≤ J.radical) (hJ : J.
 /-- The diagram of powers of `J` is initial in the diagram of all ideals with
 radical containing `J`. This uses noetherianness. -/
 instance ideal_powers_initial [hR : IsNoetherian R R] :
-    Functor.Initial (idealPowersToSelfLeRadical J)
+    Functor.Initial (idealPowersToSelfLERadical J)
     where out J' := by
     apply @zigzag_is_connected _ _ _
     · intro j1 j2
@@ -265,48 +265,48 @@ instance ideal_powers_initial [hR : IsNoetherian R R] :
       cases' le_total (unop j1.left) (unop j2.left) with h
       right; exact ⟨costructured_arrow.hom_mk (hom_of_le h).op (AsTrue.get trivial)⟩
       left; exact ⟨costructured_arrow.hom_mk (hom_of_le h).op (AsTrue.get trivial)⟩
-    · obtain ⟨k, hk⟩ := Ideal.exists_pow_le_of_le_radical_of_fG J'.2 (is_noetherian_def.mp hR _)
+    · obtain ⟨k, hk⟩ := Ideal.exists_pow_le_of_le_radical_of_fg J'.2 (is_noetherian_def.mp hR _)
       exact ⟨costructured_arrow.mk (⟨⟨hk⟩⟩ : (ideal_powers_to_self_le_radical J).obj (op k) ⟶ J')⟩
 #align local_cohomology.ideal_powers_initial localCohomology.ideal_powers_initial
 
 /-- Local cohomology (defined in terms of powers of `J`) agrees with local
 cohomology computed over all ideals with radical containing `J`. -/
 def isoSelfLeRadical (J : Ideal R) [IsNoetherian R R] (i : ℕ) :
-    localCohomology.ofSelfLeRadical J i ≅ localCohomology J i :=
-  (localCohomology.isoOfFinal.{u, u, 0} (idealPowersToSelfLeRadical J) (selfLeRadicalDiagram J)
+    localCohomology.ofSelfLERadical J i ≅ localCohomology J i :=
+  (localCohomology.isoOfFinal.{u, u, 0} (idealPowersToSelfLERadical J) (selfLERadicalDiagram J)
         i).symm ≪≫
     HasColimit.isoOfNatIso (Iso.refl _)
 #align local_cohomology.iso_self_le_radical localCohomology.isoSelfLeRadical
 
 /-- Casting from the full subcategory of ideals with radical containing `J` to the full
 subcategory of ideals with radical containing `K`. -/
-def SelfLeRadical.cast (hJK : J.radical = K.radical) : SelfLeRadical J ⥤ SelfLeRadical K :=
+def SelfLERadical.cast (hJK : J.radical = K.radical) : SelfLERadical J ⥤ SelfLERadical K :=
   FullSubcategory.map fun L hL =>
     by
     rw [← Ideal.radical_le_radical_iff] at hL ⊢
     exact hJK.symm.trans_le hL
-#align local_cohomology.self_le_radical.cast localCohomology.SelfLeRadical.cast
+#align local_cohomology.self_le_radical.cast localCohomology.SelfLERadical.cast
 
 -- TODO generalize this to the equivalence of full categories for any `iff`.
-instance SelfLeRadical.castIsEquivalence (hJK : J.radical = K.radical) :
-    IsEquivalence (SelfLeRadical.cast hJK)
+instance SelfLERadical.castIsEquivalence (hJK : J.radical = K.radical) :
+    IsEquivalence (SelfLERadical.cast hJK)
     where
-  inverse := SelfLeRadical.cast hJK.symm
+  inverse := SelfLERadical.cast hJK.symm
   unitIso := by tidy
   counitIso := by tidy
-#align local_cohomology.self_le_radical.cast_is_equivalence localCohomology.SelfLeRadical.castIsEquivalence
+#align local_cohomology.self_le_radical.cast_is_equivalence localCohomology.SelfLERadical.castIsEquivalence
 
 /-- The natural isomorphism between local cohomology defined using the `of_self_le_radical`
 diagram, assuming `J.radical = K.radical`. -/
-def SelfLeRadical.isoOfSameRadical (hJK : J.radical = K.radical) (i : ℕ) :
-    ofSelfLeRadical J i ≅ ofSelfLeRadical K i :=
-  (isoOfFinal.{u, u, u} (SelfLeRadical.cast hJK.symm) _ _).symm
-#align local_cohomology.self_le_radical.iso_of_same_radical localCohomology.SelfLeRadical.isoOfSameRadical
+def SelfLERadical.isoOfSameRadical (hJK : J.radical = K.radical) (i : ℕ) :
+    ofSelfLERadical J i ≅ ofSelfLERadical K i :=
+  (isoOfFinal.{u, u, u} (SelfLERadical.cast hJK.symm) _ _).symm
+#align local_cohomology.self_le_radical.iso_of_same_radical localCohomology.SelfLERadical.isoOfSameRadical
 
 /-- Local cohomology agrees on ideals with the same radical. -/
 def isoOfSameRadical [IsNoetherian R R] (hJK : J.radical = K.radical) (i : ℕ) :
     localCohomology J i ≅ localCohomology K i :=
-  (isoSelfLeRadical J i).symm ≪≫ SelfLeRadical.isoOfSameRadical hJK i ≪≫ isoSelfLeRadical K i
+  (isoSelfLeRadical J i).symm ≪≫ SelfLERadical.isoOfSameRadical hJK i ≪≫ isoSelfLeRadical K i
 #align local_cohomology.iso_of_same_radical localCohomology.isoOfSameRadical
 
 end LocalCohomologyEquiv