diff --git a/Mathlib/Algebra/Algebra/Hom.lean b/Mathlib/Algebra/Algebra/Hom.lean index df17ba4e63c307..5a9d0e0cff4dc8 100644 --- a/Mathlib/Algebra/Algebra/Hom.lean +++ b/Mathlib/Algebra/Algebra/Hom.lean @@ -508,13 +508,10 @@ lemma algebraMapSubmonoid_map_eq (f : A →ₐ[R] B) : ext x constructor · rintro ⟨a, ⟨r, hr, rfl⟩, rfl⟩ - simp only [AlgHom.commutes] - use r + exact ⟨r, hr, by simp⟩ · rintro ⟨r, hr, rfl⟩ simp only [Submonoid.mem_map] - use (algebraMap R A r) - simp only [AlgHom.commutes, and_true] - use r + exact ⟨(algebraMap R A r), ⟨r, hr, by simp⟩, by simp⟩ lemma algebraMapSubmonoid_le_comap (f : A →ₐ[R] B) : algebraMapSubmonoid A M ≤ (algebraMapSubmonoid B M).comap f.toRingHom := by diff --git a/Mathlib/Algebra/Algebra/Operations.lean b/Mathlib/Algebra/Algebra/Operations.lean index 38184a3262bee3..746bf81a7de4d1 100644 --- a/Mathlib/Algebra/Algebra/Operations.lean +++ b/Mathlib/Algebra/Algebra/Operations.lean @@ -751,7 +751,8 @@ theorem span_singleton_eq_one_iff {x : A} : span R {x} = 1 ↔ ∃ r : Rˣ, x = mpr := by rintro ⟨r, rfl⟩; exact span_singleton_algebraMap_of_isUnit r.isUnit theorem mker_spanSingleton : - MonoidHom.mker (Submodule.spanSingleton R) = (IsUnit.submonoid R).map (algebraMap R A) := by + (Submodule.spanSingleton R).toMonoidHom.mker = + (IsUnit.submonoid R).map (algebraMap R A).toMonoidHom := by ext; simp_rw [Submonoid.mem_map, IsUnit.mem_submonoid_iff, IsUnit, existsAndEq, true_and, eq_comm] exact span_singleton_eq_one_iff diff --git a/Mathlib/Algebra/Category/Ring/Constructions.lean b/Mathlib/Algebra/Category/Ring/Constructions.lean index 01ed6736dc8080..b1bff4b9e855c8 100644 --- a/Mathlib/Algebra/Category/Ring/Constructions.lean +++ b/Mathlib/Algebra/Category/Ring/Constructions.lean @@ -162,7 +162,8 @@ lemma isPushout_iff_isPushout {R S : Type u} [CommRing R] [CommRing S] [Algebra lemma isPushout_of_isLocalization {R S Rₘ Sₘ : Type u} [CommRing R] [CommRing Rₘ] [Algebra R Rₘ] [CommRing S] [CommRing Sₘ] [Algebra S Sₘ] (f : R →+* S) (fₘ : Rₘ →+* Sₘ) (H : fₘ.comp (algebraMap _ _) = (algebraMap _ _).comp f) - (M : Submonoid R) [IsLocalization M Rₘ] [IsLocalization (M.map f) Sₘ] : + (M : Submonoid R) [IsLocalization M Rₘ] + [IsLocalization (M.map (MonoidHomClass.toMonoidHom f)) Sₘ] : IsPushout (CommRingCat.ofHom f) (CommRingCat.ofHom (algebraMap R Rₘ)) (CommRingCat.ofHom (algebraMap S Sₘ)) (CommRingCat.ofHom fₘ) := by algebraize [f, fₘ, fₘ.comp (algebraMap R Rₘ)] diff --git a/Mathlib/Algebra/Group/Subgroup/Actions.lean b/Mathlib/Algebra/Group/Subgroup/Actions.lean index a677c52125ae53..785b4555900733 100644 --- a/Mathlib/Algebra/Group/Subgroup/Actions.lean +++ b/Mathlib/Algebra/Group/Subgroup/Actions.lean @@ -79,4 +79,4 @@ end Subgroup open MonoidHom in lemma MonoidWithZeroHom.comap_mker {M N P : Type*} [MulZeroOneClass M] [MulZeroOneClass N] [MulZeroOneClass P] (g : N →*₀ P) (f : M →*₀ N) : - Submonoid.comap f (mker g) = mker (g.comp f) := rfl + Submonoid.comap f g.toMonoidHom.mker = (g.comp f).toMonoidHom.mker := rfl diff --git a/Mathlib/Algebra/Group/Submonoid/Membership.lean b/Mathlib/Algebra/Group/Submonoid/Membership.lean index 01e73b2c7a7a47..c2ab5e8f5806d9 100644 --- a/Mathlib/Algebra/Group/Submonoid/Membership.lean +++ b/Mathlib/Algebra/Group/Submonoid/Membership.lean @@ -428,8 +428,7 @@ theorem log_pow_int_eq_self {x : ℤ} (h : 1 < x.natAbs) (m : ℕ) : log (pow x (powLogEquiv (Int.pow_right_injective h)).symm_apply_apply _ @[simp] -theorem map_powers {N : Type*} {F : Type*} [Monoid N] [FunLike F M N] [MonoidHomClass F M N] - (f : F) (m : M) : +theorem map_powers {N : Type*} [Monoid N] (f : M →* N) (m : M) : (powers m).map f = powers (f m) := by simp only [powers_eq_closure, map_mclosure f, Set.image_singleton] @@ -495,7 +494,7 @@ variable [AddMonoid A] open Set theorem closure_singleton_eq (x : A) : - closure ({x} : Set A) = AddMonoidHom.mrange (multiplesHom A x) := + closure ({x} : Set A) = (multiplesHom A x).mrange := closure_eq_of_le (Set.singleton_subset_iff.2 ⟨1, one_nsmul x⟩) fun _ ⟨_n, hn⟩ => hn ▸ nsmul_mem (subset_closure <| Set.mem_singleton _) _ @@ -509,7 +508,7 @@ theorem closure_singleton_zero : closure ({0} : Set A) = ⊥ := by /-- The additive submonoid generated by an element. -/ def multiples (x : A) : AddSubmonoid A := - AddSubmonoid.copy (AddMonoidHom.mrange (multiplesHom A x)) (Set.range (fun i => i • x : ℕ → A)) <| + AddSubmonoid.copy (multiplesHom A x).mrange (Set.range (fun i => i • x : ℕ → A)) <| Set.ext fun n => exists_congr fun i => by simp attribute [to_additive existing] Submonoid.powers diff --git a/Mathlib/Algebra/Group/Submonoid/Operations.lean b/Mathlib/Algebra/Group/Submonoid/Operations.lean index b9f429f4672d9d..9dfc06cab2cb7f 100644 --- a/Mathlib/Algebra/Group/Submonoid/Operations.lean +++ b/Mathlib/Algebra/Group/Submonoid/Operations.lean @@ -163,8 +163,6 @@ end namespace Submonoid -variable {F : Type*} [FunLike F M N] [mc : MonoidHomClass F M N] - open Set /-! @@ -174,18 +172,18 @@ open Set /-- The preimage of a `Submonoid` along a `MonoidHom` is a `Submonoid`. -/ @[to_additive /-- The preimage of an `AddSubmonoid` along an `AddMonoidHom` is an `AddSubmonoid`. -/] -def comap (f : F) (S : Submonoid N) : +def comap (f : M →* N) (S : Submonoid N) : Submonoid M where carrier := f ⁻¹' S one_mem' := show f 1 ∈ S by rw [map_one]; exact S.one_mem mul_mem' ha hb := show f (_ * _) ∈ S by rw [map_mul]; exact S.mul_mem ha hb @[to_additive (attr := simp)] -theorem coe_comap (S : Submonoid N) (f : F) : (S.comap f : Set M) = f ⁻¹' S := +theorem coe_comap (S : Submonoid N) (f : M →* N) : (S.comap f : Set M) = f ⁻¹' S := rfl @[to_additive (attr := simp)] -theorem mem_comap {S : Submonoid N} {f : F} {x : M} : x ∈ S.comap f ↔ f x ∈ S := +theorem mem_comap {S : Submonoid N} {f : M →* N} {x : M} : x ∈ S.comap f ↔ f x ∈ S := Iff.rfl @[to_additive] @@ -200,7 +198,7 @@ theorem comap_id (S : Submonoid P) : S.comap (MonoidHom.id P) = S := /-- The image of a `Submonoid` along a `MonoidHom` is a `Submonoid`. -/ @[to_additive /-- The image of an `AddSubmonoid` along an `AddMonoidHom` is an `AddSubmonoid`. -/] -def map (f : F) (S : Submonoid M) : +def map (f : M →* N) (S : Submonoid M) : Submonoid N where carrier := f '' S one_mem' := ⟨1, S.one_mem, map_one f⟩ @@ -209,116 +207,121 @@ def map (f : F) (S : Submonoid M) : exact ⟨x * y, S.mul_mem hx hy, by rw [map_mul]⟩ @[to_additive (attr := simp)] -theorem coe_map (f : F) (S : Submonoid M) : (S.map f : Set N) = f '' S := +theorem coe_map (f : M →* N) (S : Submonoid M) : (S.map f : Set N) = f '' S := rfl -@[to_additive (attr := simp)] -theorem map_coe_toMonoidHom (f : F) (S : Submonoid M) : S.map (f : M →* N) = S.map f := - rfl +-- now a syntactic tautology +--@[to_additive (attr := simp)] +--theorem map_coe_toMonoidHom (f : M →* N) (S : Submonoid M) : S.map (f : M →* N) = S.map f := +-- rfl -@[to_additive (attr := simp)] -theorem map_coe_toMulEquiv {F} [EquivLike F M N] [MulEquivClass F M N] (f : F) (S : Submonoid M) : - S.map (f : M ≃* N) = S.map f := - rfl +-- now a tautology also +-- @[to_additive (attr := simp)] +-- theorem map_coe_toMulEquiv (f : M ≃* N) (S : Submonoid M) : S.map f = S.map f.toMonoidHom := +-- rfl @[to_additive (attr := simp)] -theorem mem_map {f : F} {S : Submonoid M} {y : N} : y ∈ S.map f ↔ ∃ x ∈ S, f x = y := Iff.rfl +theorem mem_map {f : M →* N} {S : Submonoid M} {y : N} : y ∈ S.map f ↔ ∃ x ∈ S, f x = y := Iff.rfl @[to_additive] -theorem mem_map_of_mem (f : F) {S : Submonoid M} {x : M} (hx : x ∈ S) : f x ∈ S.map f := +theorem mem_map_of_mem (f : M →* N) {S : Submonoid M} {x : M} (hx : x ∈ S) : f x ∈ S.map f := mem_image_of_mem f hx @[to_additive] -theorem apply_coe_mem_map (f : F) (S : Submonoid M) (x : S) : f x ∈ S.map f := +theorem apply_coe_mem_map (f : M →* N) (S : Submonoid M) (x : S) : f x ∈ S.map f := mem_map_of_mem f x.2 @[to_additive] theorem map_map (g : N →* P) (f : M →* N) : (S.map f).map g = S.map (g.comp f) := SetLike.coe_injective <| image_image _ _ _ +variable {T : Submonoid N} {f : M →* N} + @[to_additive (attr := simp 1100)] -theorem mem_map_iff_mem {f : F} (hf : Function.Injective f) {S : Submonoid M} {x : M} : +theorem mem_map_iff_mem (hf : Function.Injective f) {S : Submonoid M} {x : M} : f x ∈ S.map f ↔ x ∈ S := hf.mem_set_image @[to_additive] -theorem map_le_iff_le_comap {f : F} {S : Submonoid M} {T : Submonoid N} : +theorem map_le_iff_le_comap {f : M →* N} {S : Submonoid M} {T : Submonoid N} : S.map f ≤ T ↔ S ≤ T.comap f := image_subset_iff +variable (f) in @[to_additive] -theorem gc_map_comap (f : F) : GaloisConnection (map f) (comap f) := fun _ _ => map_le_iff_le_comap +theorem gc_map_comap : GaloisConnection (map f) (comap f) := fun _ _ => map_le_iff_le_comap @[to_additive] -theorem map_le_of_le_comap {T : Submonoid N} {f : F} : S ≤ T.comap f → S.map f ≤ T := +theorem map_le_of_le_comap : S ≤ T.comap f → S.map f ≤ T := (gc_map_comap f).l_le @[to_additive] -theorem le_comap_of_map_le {T : Submonoid N} {f : F} : S.map f ≤ T → S ≤ T.comap f := +theorem le_comap_of_map_le : S.map f ≤ T → S ≤ T.comap f := (gc_map_comap f).le_u @[to_additive] -theorem le_comap_map {f : F} : S ≤ (S.map f).comap f := +theorem le_comap_map : S ≤ (S.map f).comap f := (gc_map_comap f).le_u_l _ @[to_additive] -theorem map_comap_le {S : Submonoid N} {f : F} : (S.comap f).map f ≤ S := +theorem map_comap_le : (T.comap f).map f ≤ T := (gc_map_comap f).l_u_le _ @[to_additive (attr := gcongr)] -theorem monotone_map {f : F} : Monotone (map f) := +theorem monotone_map : Monotone (map f) := (gc_map_comap f).monotone_l @[to_additive (attr := gcongr)] -theorem monotone_comap {f : F} : Monotone (comap f) := +theorem monotone_comap : Monotone (comap f) := (gc_map_comap f).monotone_u @[to_additive (attr := simp)] -theorem map_comap_map {f : F} : ((S.map f).comap f).map f = S.map f := +theorem map_comap_map : ((S.map f).comap f).map f = S.map f := (gc_map_comap f).l_u_l_eq_l _ @[to_additive (attr := simp)] -theorem comap_map_comap {S : Submonoid N} {f : F} : ((S.comap f).map f).comap f = S.comap f := +theorem comap_map_comap : ((T.comap f).map f).comap f = T.comap f := (gc_map_comap f).u_l_u_eq_u _ @[to_additive] -theorem map_sup (S T : Submonoid M) (f : F) : (S ⊔ T).map f = S.map f ⊔ T.map f := +theorem map_sup (S T : Submonoid M) (f : M →* N) : (S ⊔ T).map f = S.map f ⊔ T.map f := (gc_map_comap f : GaloisConnection (map f) (comap f)).l_sup @[to_additive] -theorem map_iSup {ι : Sort*} (f : F) (s : ι → Submonoid M) : (iSup s).map f = ⨆ i, (s i).map f := +theorem map_iSup {ι : Sort*} (f : M →* N) (s : ι → Submonoid M) : + (iSup s).map f = ⨆ i, (s i).map f := (gc_map_comap f : GaloisConnection (map f) (comap f)).l_iSup @[to_additive] -theorem map_inf (S T : Submonoid M) (f : F) (hf : Function.Injective f) : +theorem map_inf (S T : Submonoid M) (f : M →* N) (hf : Function.Injective f) : (S ⊓ T).map f = S.map f ⊓ T.map f := SetLike.coe_injective (Set.image_inter hf) @[to_additive] -theorem map_iInf {ι : Sort*} [Nonempty ι] (f : F) (hf : Function.Injective f) +theorem map_iInf {ι : Sort*} [Nonempty ι] (f : M →* N) (hf : Function.Injective f) (s : ι → Submonoid M) : (iInf s).map f = ⨅ i, (s i).map f := by apply SetLike.coe_injective simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coe ∘ s) @[to_additive] -theorem comap_inf (S T : Submonoid N) (f : F) : (S ⊓ T).comap f = S.comap f ⊓ T.comap f := +theorem comap_inf (S T : Submonoid N) (f : M →* N) : (S ⊓ T).comap f = S.comap f ⊓ T.comap f := (gc_map_comap f : GaloisConnection (map f) (comap f)).u_inf @[to_additive] -theorem comap_iInf {ι : Sort*} (f : F) (s : ι → Submonoid N) : +theorem comap_iInf {ι : Sort*} (f : M →* N) (s : ι → Submonoid N) : (iInf s).comap f = ⨅ i, (s i).comap f := (gc_map_comap f : GaloisConnection (map f) (comap f)).u_iInf @[to_additive (attr := simp)] -theorem map_bot (f : F) : (⊥ : Submonoid M).map f = ⊥ := +theorem map_bot (f : M →* N) : (⊥ : Submonoid M).map f = ⊥ := (gc_map_comap f).l_bot @[to_additive] -lemma disjoint_map {f : F} (hf : Function.Injective f) {H K : Submonoid M} (h : Disjoint H K) : +lemma disjoint_map (hf : Function.Injective f) {H K : Submonoid M} (h : Disjoint H K) : Disjoint (H.map f) (K.map f) := by rw [disjoint_iff, ← map_inf _ _ f hf, disjoint_iff.mp h, map_bot] @[to_additive (attr := simp)] -theorem comap_top (f : F) : (⊤ : Submonoid N).comap f = ⊤ := +theorem comap_top (f : M →* N) : (⊤ : Submonoid N).comap f = ⊤ := (gc_map_comap f).u_top @[to_additive (attr := simp)] @@ -327,7 +330,7 @@ theorem map_id (S : Submonoid M) : S.map (MonoidHom.id M) = S := section GaloisCoinsertion -variable {ι : Type*} {f : F} +variable {ι : Type*} {f : M →* N} /-- `map f` and `comap f` form a `GaloisCoinsertion` when `f` is injective. -/ @[to_additive /-- `map f` and `comap f` form a `GaloisCoinsertion` when `f` is injective. -/] @@ -377,7 +380,7 @@ end GaloisCoinsertion section GaloisInsertion -variable {ι : Type*} {f : F} +variable {ι : Type*} {f : M →* N} /-- `map f` and `comap f` form a `GaloisInsertion` when `f` is surjective. -/ @[to_additive /-- `map f` and `comap f` form a `GaloisInsertion` when `f` is surjective. -/] @@ -531,21 +534,22 @@ theorem prod_bot_sup_bot_prod (s : Submonoid M) (t : Submonoid N) : @[to_additive] theorem mem_map_equiv {f : M ≃* N} {K : Submonoid M} {x : N} : - x ∈ K.map f.toMonoidHom ↔ f.symm x ∈ K := + x ∈ K.map (MonoidHomClass.toMonoidHom f) ↔ f.symm x ∈ K := Set.mem_image_equiv @[to_additive] theorem map_equiv_eq_comap_symm (f : M ≃* N) (K : Submonoid M) : - K.map f = K.comap f.symm := + K.map f = K.comap (MonoidHomClass.toMonoidHom f.symm) := SetLike.coe_injective (f.toEquiv.image_eq_preimage_symm K) @[to_additive] theorem comap_equiv_eq_map_symm (f : N ≃* M) (K : Submonoid M) : - K.comap f = K.map f.symm := + K.comap f = K.map (MonoidHomClass.toMonoidHom f.symm) := (map_equiv_eq_comap_symm f.symm K).symm +-- TODO: should this lemma be fixed to generalise to any surjective monoid homomorphism instead? @[to_additive (attr := simp)] -theorem map_equiv_top (f : M ≃* N) : (⊤ : Submonoid M).map f = ⊤ := +theorem map_equiv_top (f : M ≃* N) : (⊤ : Submonoid M).map (MonoidHomClass.toMonoidHom f) = ⊤ := SetLike.coe_injective <| Set.image_univ.trans f.surjective.range_eq @[to_additive le_prod_iff] @@ -609,8 +613,6 @@ end Submonoid namespace MonoidHom -variable {F : Type*} [FunLike F M N] [mc : MonoidHomClass F M N] - open Submonoid library_note «range copy pattern» /-- @@ -646,15 +648,15 @@ def mrange (f : M →* N) : Submonoid N := /-- The range of a `MonoidHom` is a `Submonoid`. See Note [range copy pattern]. -/ @[to_additive /-- The range of an `AddMonoidHom` is an `AddSubmonoid`. -/] -def mrange (f : F) : Submonoid N := +def mrange (f : M →* N) : Submonoid N := ((⊤ : Submonoid M).map f).copy (Set.range f) Set.image_univ.symm @[to_additive (attr := simp)] -theorem coe_mrange (f : F) : (mrange f : Set N) = Set.range f := +theorem coe_mrange (f : M →* N) : (mrange f : Set N) = Set.range f := rfl @[to_additive (attr := simp)] -theorem mem_mrange {f : F} {y : N} : y ∈ mrange f ↔ ∃ x, f x = y := +theorem mem_mrange {f : M →* N} {y : N} : y ∈ mrange f ↔ ∃ x, f x = y := Iff.rfl @[to_additive] @@ -662,7 +664,7 @@ lemma mrange_comp {O : Type*} [MulOneClass O] (f : N →* O) (g : M →* N) : mrange (f.comp g) = (mrange g).map f := SetLike.coe_injective <| Set.range_comp f _ @[to_additive] -theorem mrange_eq_map (f : F) : mrange f = (⊤ : Submonoid M).map f := +theorem mrange_eq_map (f : M →* N) : mrange f = (⊤ : Submonoid M).map f := Submonoid.copy_eq _ @[to_additive (attr := simp)] @@ -674,7 +676,7 @@ theorem map_mrange (g : N →* P) (f : M →* N) : (mrange f).map g = mrange (co simpa only [mrange_eq_map] using (⊤ : Submonoid M).map_map g f @[to_additive] -theorem mrange_eq_top {f : F} : mrange f = (⊤ : Submonoid N) ↔ Surjective f := +theorem mrange_eq_top {f : M →* N} : mrange f = (⊤ : Submonoid N) ↔ Surjective f := SetLike.ext'_iff.trans <| Iff.trans (by rw [coe_mrange, coe_top]) Set.range_eq_univ @[to_additive (attr := simp) mrange_prodMap] @@ -686,12 +688,12 @@ lemma mrange_prodMap {M' N' : Type*} [MulOneClass M'] [MulOneClass N'] (f : M /-- The range of a surjective `MonoidHom` is the whole of the codomain. -/ @[to_additive (attr := simp) /-- The range of a surjective `AddMonoidHom` is the whole of the codomain. -/] -theorem mrange_eq_top_of_surjective (f : F) (hf : Function.Surjective f) : +theorem mrange_eq_top_of_surjective (f : M →* N) (hf : Function.Surjective f) : mrange f = (⊤ : Submonoid N) := mrange_eq_top.2 hf @[to_additive] -theorem mclosure_preimage_le (f : F) (s : Set N) : closure (f ⁻¹' s) ≤ (closure s).comap f := +theorem mclosure_preimage_le (f : M →* N) (s : Set N) : closure (f ⁻¹' s) ≤ (closure s).comap f := closure_le.2 fun _ hx => SetLike.mem_coe.2 <| mem_comap.2 <| subset_closure hx /-- The image under a `MonoidHom` of the `Submonoid` generated by a set equals the `Submonoid` @@ -699,12 +701,12 @@ generated by the image of the set. -/ @[to_additive /-- The image under an `AddMonoidHom` of the `AddSubmonoid` generated by a set equals the `AddSubmonoid` generated by the image of the set. -/] -theorem map_mclosure (f : F) (s : Set M) : (closure s).map f = closure (f '' s) := +theorem map_mclosure (f : M →* N) (s : Set M) : (closure s).map f = closure (f '' s) := Set.image_preimage.l_comm_of_u_comm (gc_map_comap f) (Submonoid.gi N).gc (Submonoid.gi M).gc fun _ ↦ rfl @[to_additive (attr := simp)] -theorem mclosure_range (f : F) : closure (Set.range f) = mrange f := by +theorem mclosure_range (f : M →* N) : closure (Set.range f) = mrange f := by rw [← Set.image_univ, ← map_mclosure, mrange_eq_map, closure_univ] /-- Restriction of a `MonoidHom` to a `Submonoid` of the domain. -/ @@ -790,19 +792,19 @@ theorem mrangeRestrict_surjective (f : M →* N) : Function.Surjective f.mrangeR @[to_additive /-- The additive kernel of an `AddMonoidHom` is the `AddSubmonoid` of elements such that `f x = 0`. -/] -def mker (f : F) : Submonoid M := +def mker (f : M →* N) : Submonoid M := (⊥ : Submonoid N).comap f @[to_additive (attr := simp)] -theorem mem_mker {f : F} {x : M} : x ∈ mker f ↔ f x = 1 := +theorem mem_mker {f : M →* N} {x : M} : x ∈ mker f ↔ f x = 1 := Iff.rfl @[to_additive] -theorem coe_mker (f : F) : (mker f : Set M) = (f : M → N) ⁻¹' {1} := +theorem coe_mker (f : M →* N) : (mker f : Set M) = (f : M → N) ⁻¹' {1} := rfl @[to_additive] -instance decidableMemMker [DecidableEq N] (f : F) : DecidablePred (· ∈ mker f) := fun x => +instance decidableMemMker [DecidableEq N] (f : M →* N) : DecidablePred (· ∈ mker f) := fun x => decidable_of_iff (f x = 1) mem_mker @[to_additive] @@ -810,7 +812,7 @@ theorem comap_mker (g : N →* P) (f : M →* N) : (mker g).comap f = mker (comp rfl @[to_additive (attr := simp)] -theorem comap_bot' (f : F) : (⊥ : Submonoid N).comap f = mker f := +theorem comap_bot' (f : M →* N) : (⊥ : Submonoid N).comap f = mker f := rfl @[to_additive (attr := simp)] @@ -1005,8 +1007,8 @@ theorem bot_or_exists_ne_one (S : Submonoid M) : S = ⊥ ∨ ∃ x ∈ S, x ≠ S.bot_or_nontrivial.imp_right S.nontrivial_iff_exists_ne_one.mp @[to_additive] -lemma codisjoint_map {F : Type*} [FunLike F M N] [MonoidHomClass F M N] {f : F} - (hf : Function.Surjective f) {H K : Submonoid M} (h : Codisjoint H K) : +lemma codisjoint_map {f : M →* N} (hf : Function.Surjective f) + {H K : Submonoid M} (h : Codisjoint H K) : Codisjoint (H.map f) (K.map f) := by rw [codisjoint_iff, ← map_sup, codisjoint_iff.mp h, ← MonoidHom.mrange_eq_map, mrange_eq_top_of_surjective _ hf] @@ -1124,7 +1126,7 @@ See `MonoidHom.submonoidMap` for a variant for `MonoidHom`s. -/ /-- An `AddEquiv` `φ` between two additive monoids `M` and `N` induces an `AddEquiv` between a submonoid `S ≤ M` and the submonoid `φ(S) ≤ N`. See `AddMonoidHom.addSubmonoidMap` for a variant for `AddMonoidHom`s. -/] -def submonoidMap (e : M ≃* N) (S : Submonoid M) : S ≃* S.map e := +def submonoidMap (e : M ≃* N) (S : Submonoid M) : S ≃* S.map e.toMonoidHom := { (e : M ≃ N).image S with map_mul' := fun _ _ => Subtype.ext (map_mul e _ _) } @[to_additive (attr := simp)] @@ -1173,19 +1175,17 @@ end Units namespace Submonoid -variable {F : Type*} [FunLike F M N] [mc : MonoidHomClass F M N] - @[to_additive] -theorem map_comap_eq (f : F) (S : Submonoid N) : (S.comap f).map f = S ⊓ MonoidHom.mrange f := +theorem map_comap_eq (f : M →* N) (S : Submonoid N) : (S.comap f).map f = S ⊓ MonoidHom.mrange f := SetLike.coe_injective Set.image_preimage_eq_inter_range @[to_additive] -theorem map_comap_eq_self {f : F} {S : Submonoid N} (h : S ≤ MonoidHom.mrange f) : +theorem map_comap_eq_self {f : M →* N} {S : Submonoid N} (h : S ≤ MonoidHom.mrange f) : (S.comap f).map f = S := by simpa only [inf_of_le_left h] using map_comap_eq f S @[to_additive] -theorem map_comap_eq_self_of_surjective {f : F} (h : Function.Surjective f) {S : Submonoid N} : +theorem map_comap_eq_self_of_surjective {f : M →* N} (h : Function.Surjective f) {S : Submonoid N} : map f (comap f S) = S := map_comap_eq_self (MonoidHom.mrange_eq_top_of_surjective _ h ▸ le_top) diff --git a/Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean b/Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean index 8274ca11bc0e46..af923d847d23f0 100644 --- a/Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean +++ b/Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean @@ -252,15 +252,13 @@ theorem map_mem_nonZeroDivisors [Nontrivial M₀] [NoZeroDivisors M₀'] [ZeroHo ⟨fun _ ↦ eq_zero_of_ne_zero_of_mul_left_eq_zero (map_ne_zero_of_mem_nonZeroDivisors g hg h), fun _ ↦ eq_zero_of_ne_zero_of_mul_right_eq_zero (map_ne_zero_of_mem_nonZeroDivisors g hg h)⟩ -theorem MulEquivClass.map_nonZeroDivisors {M₀ S F : Type*} [MonoidWithZero M₀] [MonoidWithZero S] - [EquivLike F M₀ S] [MulEquivClass F M₀ S] (h : F) : +theorem MulEquivClass.map_nonZeroDivisors + {M₀ S : Type*} [MonoidWithZero M₀] [MonoidWithZero S] (h : M₀ ≃* S) : Submonoid.map h (nonZeroDivisors M₀) = nonZeroDivisors S := by - let h : M₀ ≃* S := h - change Submonoid.map h _ = _ ext - simp_rw [Submonoid.map_equiv_eq_comap_symm, Submonoid.mem_comap, mem_nonZeroDivisors_iff, - ← h.symm.forall_congr_right, h.symm.toEquiv_eq_coe, h.symm.coe_toEquiv, ← map_mul, - map_eq_zero_iff _ h.symm.injective] + simp_rw [Submonoid.map_equiv_eq_comap_symm , Submonoid.mem_comap, mem_nonZeroDivisors_iff, + ← h.symm.forall_congr_right, h.symm.toEquiv_eq_coe, h.symm.coe_toEquiv, MonoidHom.coe_coe, + ← map_mul, map_eq_zero_iff _ h.symm.injective] theorem map_le_nonZeroDivisors_of_injective [NoZeroDivisors M₀'] [MonoidWithZeroHomClass F M₀ M₀'] (f : F) (hf : Injective f) {S : Submonoid M₀} (hS : S ≤ M₀⁰) : S.map f ≤ M₀'⁰ := by diff --git a/Mathlib/Algebra/GroupWithZero/Range.lean b/Mathlib/Algebra/GroupWithZero/Range.lean index 41eb80908b517f..15f5d7d13abcf7 100644 --- a/Mathlib/Algebra/GroupWithZero/Range.lean +++ b/Mathlib/Algebra/GroupWithZero/Range.lean @@ -56,12 +56,10 @@ section mrange variable {G H : Type*} [MulZeroOneClass G] [MulZeroOneClass H] [Nontrivial H] (f : G →*₀ H) -lemma mrange_nontrivial : - Nontrivial (MonoidHom.mrange f) := +lemma mrange_nontrivial : Nontrivial f.toMonoidHom.mrange := ⟨1, 0, by simp [Subtype.ext_iff]⟩ -lemma range_nontrivial : - (Set.range f).Nontrivial := +lemma range_nontrivial : (Set.range f).Nontrivial := Set.nontrivial_coe_sort.mp f.mrange_nontrivial end mrange diff --git a/Mathlib/Algebra/GroupWithZero/Submonoid/Instances.lean b/Mathlib/Algebra/GroupWithZero/Submonoid/Instances.lean index 41a52266808e81..93704efdb2781a 100644 --- a/Mathlib/Algebra/GroupWithZero/Submonoid/Instances.lean +++ b/Mathlib/Algebra/GroupWithZero/Submonoid/Instances.lean @@ -21,24 +21,24 @@ namespace MonoidWithZeroHom variable {G H : Type*} instance [MulZeroOneClass G] [MulZeroOneClass H] (f : G →*₀ H) : - MulZeroOneClass (MonoidHom.mrange f) where + MulZeroOneClass f.toMonoidHom.mrange where zero := ⟨0, 0, by simp⟩ zero_mul _ := Subtype.ext (zero_mul _) mul_zero _ := Subtype.ext (mul_zero _) @[simp] lemma val_mrange_zero [MulZeroOneClass G] [MulZeroOneClass H] (f : G →*₀ H) : - ((0 : MonoidHom.mrange f) : H) = 0 := + ((0 : f.toMonoidHom.mrange) : H) = 0 := rfl instance [MulZeroOneClass G] [MonoidWithZero H] (f : G →*₀ H) : - MonoidWithZero (MonoidHom.mrange f) where + MonoidWithZero f.toMonoidHom.mrange where instance [MulZeroOneClass G] [CommMonoidWithZero H] (f : G →*₀ H) : - CommMonoidWithZero (MonoidHom.mrange f) where + CommMonoidWithZero f.toMonoidHom.mrange where instance [GroupWithZero G] [GroupWithZero H] (f : G →*₀ H) : - GroupWithZero (MonoidHom.mrange f) where + GroupWithZero f.toMonoidHom.mrange where inv := fun x ↦ ⟨x⁻¹, by obtain ⟨y, hy⟩ := x.prop use y⁻¹ @@ -51,10 +51,10 @@ instance [GroupWithZero G] [GroupWithZero H] (f : G →*₀ H) : simpa using mul_inv_cancel₀ h instance [GroupWithZero G] [CommGroupWithZero H] (f : G →*₀ H) : - CommGroupWithZero (MonoidHom.mrange f) where + CommGroupWithZero f.toMonoidHom.mrange where lemma mker_inverse [CommGroupWithZero H] : - MonoidHom.mker (MonoidWithZero.inverse (M := H)) = ⊥ := by + (MonoidWithZero.inverse (M := H)).toMonoidHom.mker = ⊥ := by ext simp diff --git a/Mathlib/Algebra/Module/LocalizedModule/Basic.lean b/Mathlib/Algebra/Module/LocalizedModule/Basic.lean index 467646b2838e25..a47aae8a437e8b 100644 --- a/Mathlib/Algebra/Module/LocalizedModule/Basic.lean +++ b/Mathlib/Algebra/Module/LocalizedModule/Basic.lean @@ -759,7 +759,7 @@ lemma IsLocalizedModule.of_restrictScalars (S : Submonoid R) map_units x := by obtain ⟨_, x, hx, rfl⟩ := x have := IsLocalizedModule.map_units (f.restrictScalars R) ⟨x, hx⟩ - simp only [← IsScalarTower.algebraMap_apply, Module.End.isUnit_iff] at this ⊢ + simp only [End.isUnit_iff, MonoidHom.coe_coe, ← IsScalarTower.algebraMap_apply] at this ⊢ exact this surj y := by obtain ⟨⟨x, t⟩, e⟩ := IsLocalizedModule.surj S (f.restrictScalars R) y diff --git a/Mathlib/Algebra/Module/LocalizedModule/IsLocalization.lean b/Mathlib/Algebra/Module/LocalizedModule/IsLocalization.lean index 89f0714709261a..4031d4e62a95d5 100644 --- a/Mathlib/Algebra/Module/LocalizedModule/IsLocalization.lean +++ b/Mathlib/Algebra/Module/LocalizedModule/IsLocalization.lean @@ -26,9 +26,8 @@ theorem isLocalizedModule_iff_isLocalization : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ := by rw [isLocalizedModule_iff, isLocalization_iff] refine and_congr ?_ (and_congr (forall_congr' fun _ ↦ ?_) (forall₂_congr fun _ _ ↦ ?_)) - · simp_rw [← (Algebra.lmul R Aₛ).commutes, Algebra.lmul_isUnit_iff, Subtype.forall, - Algebra.algebraMapSubmonoid, ← SetLike.mem_coe, Submonoid.coe_map, - Set.forall_mem_image, ← IsScalarTower.algebraMap_apply] + · simp_rw [← (Algebra.lmul R Aₛ).commutes, Algebra.lmul_isUnit_iff] + simp [Algebra.algebraMapSubmonoid, ← IsScalarTower.algebraMap_apply] · simp_rw [Prod.exists, Subtype.exists, Algebra.algebraMapSubmonoid] simp [← IsScalarTower.algebraMap_apply, Submonoid.mk_smul, Algebra.smul_def, mul_comm] · congr!; simp_rw [Subtype.exists, Algebra.algebraMapSubmonoid]; simp [Algebra.smul_def] diff --git a/Mathlib/Algebra/Module/Submodule/Ker.lean b/Mathlib/Algebra/Module/Submodule/Ker.lean index e3ecddf1bb034b..c5de2fd7eca1b0 100644 --- a/Mathlib/Algebra/Module/Submodule/Ker.lean +++ b/Mathlib/Algebra/Module/Submodule/Ker.lean @@ -72,7 +72,7 @@ theorem ker_id : ker (LinearMap.id : M →ₗ[R] M) = ⊥ := theorem map_coe_ker (f : M →ₛₗ[τ₁₂] M₂) (x : ker f) : f x = 0 := mem_ker.1 x.2 -theorem ker_toAddSubmonoid (f : M →ₛₗ[τ₁₂] M₂) : (ker f).toAddSubmonoid = (AddMonoidHom.mker f) := +theorem ker_toAddSubmonoid (f : M →ₛₗ[τ₁₂] M₂) : (ker f).toAddSubmonoid = f.toAddMonoidHom.mker := rfl theorem le_ker_iff_comp_subtype_eq_zero {N : Submodule R M} {f : M →ₛₗ[τ₁₂] M₂} : diff --git a/Mathlib/Algebra/Module/Submodule/Map.lean b/Mathlib/Algebra/Module/Submodule/Map.lean index 0c7d87f99a9186..c9d93010233c24 100644 --- a/Mathlib/Algebra/Module/Submodule/Map.lean +++ b/Mathlib/Algebra/Module/Submodule/Map.lean @@ -51,7 +51,7 @@ variable [RingHomSurjective σ₁₂] /-- The pushforward of a submodule `p ⊆ M` by `f : M → M₂` -/ def map (f : M →ₛₗ[σ₁₂] M₂) (p : Submodule R M) : Submodule R₂ M₂ := - { p.toAddSubmonoid.map f with + { p.toAddSubmonoid.map f.toAddMonoidHom with carrier := f '' p smul_mem' := by rintro c x ⟨y, hy, rfl⟩ @@ -170,7 +170,7 @@ theorem map_equivMapOfInjective_symm_apply (f : M →ₛₗ[σ₁₂] M₂) (i : /-- The pullback of a submodule `p ⊆ M₂` along `f : M → M₂` -/ @[implicit_reducible] def comap (f : M →ₛₗ[σ₁₂] M₂) (p : Submodule R₂ M₂) : Submodule R M := - { p.toAddSubmonoid.comap f with + { p.toAddSubmonoid.comap f.toAddMonoidHom with carrier := f ⁻¹' p -- Note: https://github.com/leanprover-community/mathlib4/pull/8386 added `map_smulₛₗ _` smul_mem' := fun a x h => by simp [p.smul_mem (σ₁₂ a) h, map_smulₛₗ _] } diff --git a/Mathlib/Algebra/Module/Submodule/Range.lean b/Mathlib/Algebra/Module/Submodule/Range.lean index 80f52ef00ffa7d..e47bf78ce9232a 100644 --- a/Mathlib/Algebra/Module/Submodule/Range.lean +++ b/Mathlib/Algebra/Module/Submodule/Range.lean @@ -61,7 +61,7 @@ theorem coe_range [RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) rfl theorem range_toAddSubmonoid [RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) : - (range f).toAddSubmonoid = AddMonoidHom.mrange f := + (range f).toAddSubmonoid = f.toAddMonoidHom.mrange := rfl @[simp] diff --git a/Mathlib/Algebra/Order/Star/Basic.lean b/Mathlib/Algebra/Order/Star/Basic.lean index a7a23a2cf9db86..e6bac45771c84b 100644 --- a/Mathlib/Algebra/Order/Star/Basic.lean +++ b/Mathlib/Algebra/Order/Star/Basic.lean @@ -281,7 +281,7 @@ lemma star_le_star_iff {x y : R} : star x ≤ star y ↔ x ≤ y := by rw [StarOrderedRing.le_iff] at h ⊢ obtain ⟨d, hd, rfl⟩ := h refine ⟨starAddEquiv d, ?_, star_add _ _⟩ - refine AddMonoidHom.mclosure_preimage_le _ _ <| AddSubmonoid.closure_mono ?_ hd + refine starAddEquiv.toAddMonoidHom.mclosure_preimage_le _ <| AddSubmonoid.closure_mono ?_ hd rintro - ⟨s, rfl⟩ exact ⟨s, by simp⟩ @@ -395,7 +395,8 @@ instance [NonUnitalSemiring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] StarOrderedRing Rᵐᵒᵖ where le_iff x y := by rw [← unop_le_unop, StarOrderedRing.le_iff, op_surjective.exists, - ← (AddSubmonoid.closure _).comap_map_eq_of_injective opAddEquiv.injective] + ← (AddSubmonoid.closure _).comap_map_eq_of_injective (f := opAddEquiv (α := R).toAddMonoidHom) + opAddEquiv.injective] congr! with p · simp [AddMonoidHom.map_mclosure, ← range_comp', Function.comp_def, ← (star_involutive.surjective.comp op_surjective).range_comp] diff --git a/Mathlib/Algebra/Polynomial/Splits.lean b/Mathlib/Algebra/Polynomial/Splits.lean index a74f7a3cc409ed..1b7dfe988e24d2 100644 --- a/Mathlib/Algebra/Polynomial/Splits.lean +++ b/Mathlib/Algebra/Polynomial/Splits.lean @@ -157,15 +157,16 @@ lemma Splits.taylor {p : R[X]} (hp : p.Splits) (r : R) : (p.taylor r).Splits := theorem splits_iff_exists_multiset' {f : R[X]} : Splits f ↔ ∃ m : Multiset R, f = C f.leadingCoeff * (m.map (X + C ·)).prod := by refine ⟨fun hf ↦ ?_, ?_⟩ - · let S : Submonoid R[X] := MonoidHom.mrange C - have hS : S = {C a | a : R} := MonoidHom.coe_mrange C + · let S : Submonoid R[X] := C.toMonoidHom.mrange + have hS : S = {C a | a : R} := C.toMonoidHom.coe_mrange rw [Splits, Submonoid.closure_union, ← hS, Submonoid.closure_eq, Submonoid.mem_sup] at hf obtain ⟨-, ⟨a, rfl⟩, g, hg, rfl⟩ := hf obtain ⟨mg, hmg, rfl⟩ := Submonoid.exists_multiset_of_mem_closure hg choose! j hj using hmg have hmg : mg = (mg.map j).map (X + C ·) := by simp [Multiset.map_congr rfl hj] - rw [hmg, leadingCoeff_mul_monic, leadingCoeff_C] + rw [hmg, leadingCoeff_mul_monic] · use mg.map j + simp · rw [hmg] apply monic_multiset_prod_of_monic simp [monic_X_add_C] diff --git a/Mathlib/Algebra/Ring/Equiv.lean b/Mathlib/Algebra/Ring/Equiv.lean index 01f6881c0fb665..d7d99974bc1e9f 100644 --- a/Mathlib/Algebra/Ring/Equiv.lean +++ b/Mathlib/Algebra/Ring/Equiv.lean @@ -808,6 +808,15 @@ theorem toMonoidHom_refl : (RingEquiv.refl R).toMonoidHom = MonoidHom.id R := theorem toAddMonoidHom_refl : (RingEquiv.refl R).toAddMonoidHom = AddMonoidHom.id R := rfl +@[simp] +theorem toMonoidHom_refl' : MonoidHomClass.toMonoidHom (RingEquiv.refl R) = MonoidHom.id R := + rfl + +@[simp] +theorem toAddMonoidHom_refl' : AddMonoidHomClass.toAddMonoidHom (RingEquiv.refl R) = + AddMonoidHom.id R := + rfl + theorem toRingHom_apply_symm_toRingHom_apply (e : R ≃+* S) : ∀ y : S, e.toRingHom (e.symm.toRingHom y) = y := e.toEquiv.apply_symm_apply diff --git a/Mathlib/AlgebraicGeometry/IdealSheaf/Subscheme.lean b/Mathlib/AlgebraicGeometry/IdealSheaf/Subscheme.lean index 807d549eba1105..4e23a012e0c941 100644 --- a/Mathlib/AlgebraicGeometry/IdealSheaf/Subscheme.lean +++ b/Mathlib/AlgebraicGeometry/IdealSheaf/Subscheme.lean @@ -118,7 +118,7 @@ lemma isLocalization_away {U V : X.affineOpens} let := (X.presheaf.map (homOfLE (X := X.Opens) h).op).hom.toAlgebra have : IsLocalization.Away f Γ(X, U) := by subst hU; exact V.2.isLocalization_of_eq_basicOpen _ _ rfl - simp only [IsLocalization.Away, ← Submonoid.map_powers] + rw [IsLocalization.Away, ← MonoidHom.coe_coe, ← Submonoid.map_powers] refine IsLocalization.of_surjective _ _ _ Ideal.Quotient.mk_surjective _ Ideal.Quotient.mk_surjective ?_ ?_ · simp [RingHom.algebraMap_toAlgebra, Ideal.quotientMap_comp_mk]; rfl diff --git a/Mathlib/AlgebraicGeometry/StructureSheaf.lean b/Mathlib/AlgebraicGeometry/StructureSheaf.lean index a4c4f331dfaf37..d88bc982307489 100644 --- a/Mathlib/AlgebraicGeometry/StructureSheaf.lean +++ b/Mathlib/AlgebraicGeometry/StructureSheaf.lean @@ -403,7 +403,7 @@ def toBasicOpenₗ (f : R) : LocalizedModule.Away f M →ₗ[R] Γ(M, PrimeSpectrum.basicOpen f) := IsLocalizedModule.lift (.powers f) (LocalizedModule.mkLinearMap ..) (toOpenₗ R M _) <| by simp only [Subtype.forall] - exact Submonoid.powers_le (P := (IsUnit.submonoid _).comap (algebraMap R _)).mpr + exact Submonoid.powers_le (P := (IsUnit.submonoid _).comap (algebraMap R _).toMonoidHom).mpr (isUnit_basicOpen_end ..) @[simp] diff --git a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Basic.lean b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Basic.lean index f260aed58f3d47..1715ab44710677 100644 --- a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Basic.lean +++ b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Basic.lean @@ -434,7 +434,7 @@ instance CStarAlgebra.instNonnegSpectrumClass' : NonnegSpectrumClass ℝ A where have := CStarAlgebra.spectralOrderedRing A⁺¹ apply spectrum_nonneg_of_nonneg rw [StarOrderedRing.nonneg_iff] at ha ⊢ - have := AddSubmonoid.mem_map_of_mem (Unitization.inrNonUnitalStarAlgHom ℂ A) ha + have := AddSubmonoid.mem_map_of_mem (Unitization.inrNonUnitalStarAlgHom ℂ A).toAddMonoidHom ha rw [AddMonoidHom.map_mclosure, ← Set.range_comp] at this apply AddSubmonoid.closure_mono ?_ this rintro _ ⟨s, rfl⟩ diff --git a/Mathlib/Data/Matrix/Basis.lean b/Mathlib/Data/Matrix/Basis.lean index 9223ab828cdd11..68a9a0bd51ee6b 100644 --- a/Mathlib/Data/Matrix/Basis.lean +++ b/Mathlib/Data/Matrix/Basis.lean @@ -415,7 +415,7 @@ theorem center_eq_scalar_image : exact ⟨x, by simpa using fun r ↦ congr($(hx (single i i r)) i i)⟩ theorem submonoidCenter_eq_scalar_map : - Submonoid.center (Matrix n n α) = (Submonoid.center α).map (scalar n) := + Submonoid.center (Matrix n n α) = (Submonoid.center α).map (scalar n).toMonoidHom := SetLike.coe_injective center_eq_scalar_image theorem subsemigroupCenter_eq_scalar_map : diff --git a/Mathlib/Data/Rat/Star.lean b/Mathlib/Data/Rat/Star.lean index dfbd8497525211..162e5754285a24 100644 --- a/Mathlib/Data/Rat/Star.lean +++ b/Mathlib/Data/Rat/Star.lean @@ -49,7 +49,7 @@ namespace Rat @[simp] lemma addSubmonoid_closure_range_pow {n : ℕ} (hn₀ : n ≠ 0) (hn : Even n) : closure (range fun x : ℚ ↦ x ^ n) = nonneg _ := by - convert! (AddMonoidHom.map_mclosure NNRat.coeHom <| range fun x ↦ x ^ n).symm + convert! (AddMonoidHom.map_mclosure NNRat.coeHom.toAddMonoidHom <| range fun x ↦ x ^ n).symm · have (x : ℚ) : ∃ y : ℚ≥0, y ^ n = x ^ n := ⟨x.nnabs, by simp [hn.pow_abs]⟩ simp [subset_antisymm_iff, range_subset_iff, this] · ext diff --git a/Mathlib/FieldTheory/RatFunc/Basic.lean b/Mathlib/FieldTheory/RatFunc/Basic.lean index 9fbd322f65c4f3..0e8a8672fbb51f 100644 --- a/Mathlib/FieldTheory/RatFunc/Basic.lean +++ b/Mathlib/FieldTheory/RatFunc/Basic.lean @@ -323,10 +323,11 @@ def map [MonoidHomClass F R[X] S[X]] (φ : F) (hφ : R[X]⁰ ≤ S[X]⁰.comap RatFunc.liftOn f (fun n d => if h : φ d ∈ S[X]⁰ then ofFractionRing (Localization.mk (φ n) ⟨φ d, h⟩) else 0) fun {p q p' q'} hq hq' h => by - simp only [Submonoid.mem_comap.mp (hφ hq), Submonoid.mem_comap.mp (hφ hq'), - dite_eq_left, ofFractionRing.injEq, Localization.mk_eq_mk_iff] - refine Localization.r_of_eq ?_ - simpa only [map_mul] using congr_arg φ h + rw [← MonoidHom.coe_coe] + simp only [Submonoid.mem_comap.mp (hφ hq), Submonoid.mem_comap.mp (hφ hq'), + dite_eq_left, ofFractionRing.injEq, Localization.mk_eq_mk_iff] + refine Localization.r_of_eq ?_ + simpa [map_mul] using congr_arg φ h map_one' := by simp_rw [← ofFractionRing_one, ← Localization.mk_one, liftOn_ofFractionRing_mk, OneMemClass.coe_one, map_one, OneMemClass.one_mem, dite_true, ofFractionRing.injEq, @@ -348,8 +349,8 @@ theorem map_apply_ofFractionRing_mk [MonoidHomClass F R[X] S[X]] (φ : F) (hφ : R[X]⁰ ≤ S[X]⁰.comap φ) (n : R[X]) (d : R[X]⁰) : map φ hφ (ofFractionRing (Localization.mk n d)) = ofFractionRing (Localization.mk (φ n) ⟨φ d, hφ d.prop⟩) := by - simp only [map, MonoidHom.coe_mk, OneHom.coe_mk, liftOn_ofFractionRing_mk, - Submonoid.mem_comap.mp (hφ d.2), ↓reduceDIte] + simp [map, MonoidHom.coe_mk, OneHom.coe_mk, liftOn_ofFractionRing_mk, + MonoidHom.coe_coe φ ▸ Submonoid.mem_comap.mp (hφ d.2)] theorem map_injective [MonoidHomClass F R[X] S[X]] (φ : F) (hφ : R[X]⁰ ≤ S[X]⁰.comap φ) (hf : Function.Injective φ) : Function.Injective (map φ hφ) := by diff --git a/Mathlib/GroupTheory/MonoidLocalization/MonoidWithZero.lean b/Mathlib/GroupTheory/MonoidLocalization/MonoidWithZero.lean index df2dc06d833cb7..2160e40f5b8d27 100644 --- a/Mathlib/GroupTheory/MonoidLocalization/MonoidWithZero.lean +++ b/Mathlib/GroupTheory/MonoidLocalization/MonoidWithZero.lean @@ -128,7 +128,8 @@ theorem nonZeroDivisors_le_comap (f : LocalizationMap S N) : nonZeroDivisors M ≤ (nonZeroDivisors N).comap f := by refine fun m hm ↦ nonZeroDivisorsRight_eq_nonZeroDivisors (M₀ := N) ▸ fun n h0 ↦ ?_ have ⟨ms, eq⟩ := f.surj n - rw [← (f.map_units ms.2).mul_left_eq_zero, mul_right_comm, eq, ← map_mul, map_eq_zero_iff] at h0 + rw [← (f.map_units ms.2).mul_left_eq_zero, mul_right_comm, eq, MonoidHom.coe_coe, + ← map_mul, map_eq_zero_iff] at h0 simp_rw [← mul_assoc, mul_right_mem_nonZeroDivisorsRight_eq_zero_iff hm.2] at h0 rwa [← (f.map_units ms.2).mul_left_eq_zero, eq, map_eq_zero_iff] diff --git a/Mathlib/LinearAlgebra/RootSystem/Base.lean b/Mathlib/LinearAlgebra/RootSystem/Base.lean index 77e95b084476d1..dcc20f186ca1d4 100644 --- a/Mathlib/LinearAlgebra/RootSystem/Base.lean +++ b/Mathlib/LinearAlgebra/RootSystem/Base.lean @@ -109,6 +109,7 @@ private lemma map_aux_pos [DecidableEq ι₂] (s : Finset ι) {f : ι → M} {f have aux₁ : f (e₁.symm i) = e₂.symm (f₂ i) := by have := congr_fun he (e₁.symm i); simp_all have aux₂ : AddSubmonoid.closure (f₂ '' e₁ '' s) = (AddSubmonoid.closure (f '' s)).map e₂ := by rw [AddMonoidHom.map_mclosure, ← image_comp, ← image_comp, he] + simp aesop private lemma map_aux_neg [DecidableEq ι₂] (s : Finset ι) {f : ι → M} {f₂ : ι₂ → M₂} @@ -118,6 +119,7 @@ private lemma map_aux_neg [DecidableEq ι₂] (s : Finset ι) {f : ι → M} {f have aux₁ : f (e₁.symm i) = e₂.symm (f₂ i) := by have := congr_fun he (e₁.symm i); simp_all have aux₂ : AddSubmonoid.closure (f₂ '' e₁ '' s) = (AddSubmonoid.closure (f '' s)).map e₂ := by rw [AddMonoidHom.map_mclosure, ← image_comp, ← image_comp, he] + simp aesop /-- The push forward of a base along an equivalence. -/ diff --git a/Mathlib/ModelTheory/Arithmetic/Presburger/Semilinear/Defs.lean b/Mathlib/ModelTheory/Arithmetic/Presburger/Semilinear/Defs.lean index ee2a89592cef77..f5564b26af3be3 100644 --- a/Mathlib/ModelTheory/Arithmetic/Presburger/Semilinear/Defs.lean +++ b/Mathlib/ModelTheory/Arithmetic/Presburger/Semilinear/Defs.lean @@ -102,7 +102,8 @@ theorem IsLinearSet.add (hs₁ : IsLinearSet s₁) (hs₂ : IsLinearSet s₂) : theorem IsLinearSet.image (hs : IsLinearSet s) (f : F) : IsLinearSet (f '' s) := by rcases hs with ⟨a, t, ht, rfl⟩ refine ⟨f a, f '' t, ht.image f, ?_⟩ - simp [image_vadd_distrib, ← AddMonoidHom.map_mclosure] + simp [image_vadd_distrib, ← AddMonoidHom.coe_coe f ▸ + AddMonoidHom.map_mclosure (f := AddMonoidHomClass.toAddMonoidHom f)] /-- A set is semilinear if it is a finite union of linear sets. -/ def IsSemilinearSet (s : Set M) : Prop := diff --git a/Mathlib/NumberTheory/LocalField/Basic.lean b/Mathlib/NumberTheory/LocalField/Basic.lean index 2e27508baf8db5..41e82df0d285c8 100644 --- a/Mathlib/NumberTheory/LocalField/Basic.lean +++ b/Mathlib/NumberTheory/LocalField/Basic.lean @@ -119,11 +119,11 @@ def valueGroupWithZeroIsoInt : ValueGroupWithZero K ≃*o ℤᵐ⁰ := by have := isUniformAddGroup_of_addCommGroup (G := K) obtain ⟨_⟩ := Valued.integer.locallyFiniteOrder_units_mrange_of_isCompact_integer (isCompact_iff_compactSpace.mpr (inferInstance : CompactSpace 𝒪[K])) - let e : (MonoidHom.mrange (valuation K)) ≃*o ValueGroupWithZero K := - ⟨.ofBijective (MonoidHom.mrange (valuation K)).subtype ⟨Subtype.val_injective, fun x ↦ + let e : MonoidHom.mrange (valuation K).toMonoidHom ≃*o ValueGroupWithZero K := + ⟨.ofBijective ((valuation K).toMonoidHom.mrange).subtype ⟨Subtype.val_injective, fun x ↦ ⟨⟨x, ValuativeRel.valuation_surjective x⟩, rfl⟩⟩, .rfl⟩ have : Nontrivial (ValueGroupWithZero K)ˣ := isNontrivial_iff_nontrivial_units.mp inferInstance - have : Nontrivial (↥(MonoidHom.mrange (valuation K)))ˣ := + have : Nontrivial ((valuation K).toMonoidHom.mrange)ˣ := (Units.map_injective (f := e.symm.toMonoidHom) e.symm.injective).nontrivial exact ⟨e.symm.trans (LocallyFiniteOrder.orderMonoidWithZeroEquiv _)⟩ diff --git a/Mathlib/NumberTheory/NumberField/FractionalIdeal.lean b/Mathlib/NumberTheory/NumberField/FractionalIdeal.lean index 0ab938385f7260..0af122f4898099 100644 --- a/Mathlib/NumberTheory/NumberField/FractionalIdeal.lean +++ b/Mathlib/NumberTheory/NumberField/FractionalIdeal.lean @@ -62,7 +62,7 @@ instance (I : (FractionalIdeal (𝓞 K)⁰ K)ˣ) : · refine Submonoid.mul_mem _ hd (mem_nonZeroDivisors_of_ne_zero ?_) rw [Nat.cast_ne_zero, ne_eq, Ideal.absNorm_eq_zero_iff] exact FractionalIdeal.num_eq_zero_iff.not.mpr <| Units.ne_zero I - · simp_rw [LinearMap.coe_restrictScalars, Submodule.coe_subtype] at h ⊢ + · simp_rw [LinearMap.coe_restrictScalars, Submodule.coe_subtype, MonoidHom.coe_coe] at h ⊢ rw [← h] simp only [Submonoid.mk_smul, zsmul_eq_mul, Int.cast_mul, Int.cast_natCast, algebraMap_int_eq, eq_intCast, map_intCast] diff --git a/Mathlib/RepresentationTheory/Homological/GroupCohomology/Hilbert90.lean b/Mathlib/RepresentationTheory/Homological/GroupCohomology/Hilbert90.lean index b58f066d968989..4967c37f3fa0a5 100644 --- a/Mathlib/RepresentationTheory/Homological/GroupCohomology/Hilbert90.lean +++ b/Mathlib/RepresentationTheory/Homological/GroupCohomology/Hilbert90.lean @@ -181,6 +181,7 @@ lemma exists_mul_galRestrict_of_norm_eq_one (hg : ∀ x, x ∈ Subgroup.zpowers obtain ⟨a, b, h⟩ := IsLocalization.exists_mk'_eq (Algebra.algebraMapSubmonoid B A⁰) ε.1 obtain ⟨t, ht, ht'⟩ := b.prop have : t • IsLocalization.mk' L a b = algebraMap _ _ a := by + simp only [MonoidHom.coe_coe] at ht' rw [Algebra.smul_def, IsScalarTower.algebraMap_apply A B L, ht', IsLocalization.mk'_spec'] refine ⟨a, ?_, ?_⟩ · rintro rfl diff --git a/Mathlib/RingTheory/ClassGroup/Basic.lean b/Mathlib/RingTheory/ClassGroup/Basic.lean index d74fafaf5019f0..cd6a6d745ac797 100644 --- a/Mathlib/RingTheory/ClassGroup/Basic.lean +++ b/Mathlib/RingTheory/ClassGroup/Basic.lean @@ -125,7 +125,7 @@ theorem ClassGroup.mk_eq_mk {I J : (FractionalIdeal R⁰ <| FractionRing R)ˣ} : ClassGroup.mk (FractionRing R) I = ClassGroup.mk (FractionRing R) J ↔ ∃ x : (FractionRing R)ˣ, I * toPrincipalIdeal R (FractionRing R) x = J := by rw [mk_def, mk_def, QuotientGroup.mk'_eq_mk'] - simp [RingEquiv.coe_monoidHom_refl, MonoidHom.mem_range, -toPrincipalIdeal_eq_iff] + simp [-toPrincipalIdeal_eq_iff] theorem ClassGroup.mk_eq_mk_of_coe_ideal {I J : (FractionalIdeal R⁰ <| FractionRing R)ˣ} {I' J' : Ideal R} (hI : (I : FractionalIdeal R⁰ <| FractionRing R) = I') diff --git a/Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean b/Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean index 2a95d81f1d7ff8..daeeb2863bd0c0 100644 --- a/Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean +++ b/Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean @@ -69,7 +69,7 @@ theorem IsIntegralClosure.isLocalization [IsDomain A] [Algebra.IsAlgebraic K L] refine ⟨?_, fun z => ?_, fun {x y} h => ⟨1, ?_⟩⟩ · rintro ⟨_, x, hx, rfl⟩ rw [isUnit_iff_ne_zero, map_ne_zero_iff _ (IsIntegralClosure.algebraMap_injective C A L), - Subtype.coe_mk, map_ne_zero_iff _ (FaithfulSMul.algebraMap_injective A C)] + Subtype.coe_mk, MonoidHom.coe_coe, map_ne_zero_iff _ (FaithfulSMul.algebraMap_injective A C)] exact mem_nonZeroDivisors_iff_ne_zero.mp hx · obtain ⟨m, hm⟩ := IsIntegral.exists_multiple_integral_of_isLocalization A⁰ z diff --git a/Mathlib/RingTheory/EssentialFiniteness.lean b/Mathlib/RingTheory/EssentialFiniteness.lean index a57625a143386f..2e349070ba6494 100644 --- a/Mathlib/RingTheory/EssentialFiniteness.lean +++ b/Mathlib/RingTheory/EssentialFiniteness.lean @@ -39,7 +39,7 @@ See `IntermediateField.fg_top_iff`. -/ class EssFiniteType : Prop where cond : ∃ s : Finset S, - IsLocalization ((IsUnit.submonoid S).comap (algebraMap (adjoin R (s : Set S)) S)) S + IsLocalization ((IsUnit.submonoid S).comap (algebraMap (adjoin R (s : Set S)) S).toMonoidHom) S /-- Let `S` be an `R`-algebra essentially of finite type, this is a choice of a finset `s ⊆ S` such that `S` is the localization of `R[s]`. -/ @@ -70,7 +70,8 @@ instance EssFiniteType.isLocalization [h : EssFiniteType R S] : h.cond.choose_spec lemma essFiniteType_cond_iff (σ : Finset S) : - IsLocalization ((IsUnit.submonoid S).comap (algebraMap (adjoin R (σ : Set S)) S)) S ↔ + IsLocalization ((IsUnit.submonoid S).comap + (algebraMap (adjoin R (σ : Set S)) S).toMonoidHom) S ↔ (∀ s : S, ∃ t ∈ Algebra.adjoin R (σ : Set S), IsUnit t ∧ s * t ∈ Algebra.adjoin R (σ : Set S)) := by constructor <;> intro hσ diff --git a/Mathlib/RingTheory/Etale/Basic.lean b/Mathlib/RingTheory/Etale/Basic.lean index 9dbcb40ff16f7e..73877b9f652bb7 100644 --- a/Mathlib/RingTheory/Etale/Basic.lean +++ b/Mathlib/RingTheory/Etale/Basic.lean @@ -173,7 +173,7 @@ variable (M : Submonoid R) variable [Algebra R S] [Algebra R Sₘ] [Algebra S Sₘ] [Algebra R Rₘ] [Algebra Rₘ Sₘ] variable [IsScalarTower R Rₘ Sₘ] [IsScalarTower R S Sₘ] /-! and that Rₘ and Sₘ are localizations of R and S at M. -/ -variable [IsLocalization M Rₘ] [IsLocalization (M.map (algebraMap R S)) Sₘ] +variable [IsLocalization M Rₘ] [IsLocalization (M.map (algebraMap R S).toMonoidHom) Sₘ] include M theorem of_isLocalization : FormallyEtale R Rₘ := @@ -189,7 +189,7 @@ theorem localization_base [FormallyEtale R Sₘ] : FormallyEtale Rₘ Sₘ := /-- The localization of a formally étale map is formally étale. -/ theorem localization_map [FormallyEtale R S] : FormallyEtale Rₘ Sₘ := by - have : FormallyEtale S Sₘ := FormallyEtale.of_isLocalization (M.map (algebraMap R S)) + have : FormallyEtale S Sₘ := FormallyEtale.of_isLocalization (M.map (algebraMap R S).toMonoidHom) have : FormallyEtale R Sₘ := FormallyEtale.comp R S Sₘ exact FormallyEtale.localization_base M diff --git a/Mathlib/RingTheory/Etale/Kaehler.lean b/Mathlib/RingTheory/Etale/Kaehler.lean index 48bfeee74dc527..543e1dd3eec8fb 100644 --- a/Mathlib/RingTheory/Etale/Kaehler.lean +++ b/Mathlib/RingTheory/Etale/Kaehler.lean @@ -277,7 +277,7 @@ noncomputable def tensorH1CotangentOfIsLocalization (M : Submonoid S) [IsLocalization M T] : T ⊗[S] H1Cotangent R S ≃ₗ[T] H1Cotangent R T := by letI P : Extension R S := (Generators.self R S).toExtension - letI M' := M.comap (algebraMap P.Ring S) + letI M' := M.comap (algebraMap P.Ring S).toMonoidHom letI fQ : Localization M' →ₐ[R] T := IsLocalization.liftAlgHom (M := M') (f := (IsScalarTower.toAlgHom R S T).comp (IsScalarTower.toAlgHom R P.Ring S)) (fun ⟨y, hy⟩ ↦ by simpa using IsLocalization.map_units T ⟨algebraMap P.Ring S y, hy⟩) @@ -350,7 +350,7 @@ lemma tensorH1CotangentOfIsLocalization_toLinearMap LinearEquiv.ofBijective_apply, LinearMap.liftBaseChange_tmul, one_smul, Extension.equivH1CotangentOfFormallySmooth, LinearEquiv.trans_apply] let P : Extension R S := (Generators.self R S).toExtension - let M' := M.comap (algebraMap P.Ring S) + let M' := M.comap (algebraMap P.Ring S).toMonoidHom let fQ : Localization M' →ₐ[R] T := IsLocalization.liftAlgHom (M := M') (f := (IsScalarTower.toAlgHom R S T).comp (IsScalarTower.toAlgHom R P.Ring S)) (fun ⟨y, hy⟩ ↦ by simpa using IsLocalization.map_units T ⟨algebraMap P.Ring S y, hy⟩) diff --git a/Mathlib/RingTheory/Etale/StandardEtale.lean b/Mathlib/RingTheory/Etale/StandardEtale.lean index 7d328ace851c17..f1d09b596bb348 100644 --- a/Mathlib/RingTheory/Etale/StandardEtale.lean +++ b/Mathlib/RingTheory/Etale/StandardEtale.lean @@ -412,7 +412,7 @@ lemma IsStandardEtale.of_isLocalizationAway [IsStandardEtale R S] have := IsLocalization.Away.mul S' (Localization.Away (algebraMap _ S' (AdjoinRoot.mk P.f p))) (AdjoinRoot.mk P.f P.g) (.mk _ p) rw [← map_mul] at this - have H : Submonoid.map e.symm.toRingEquiv.toMonoidHom (.powers + have H : Submonoid.map (MonoidHomClass.toMonoidHom e.symm) (.powers (algebraMap _ S' (AdjoinRoot.mk P.f p))) = .powers (aeval P.x p) := by have : ((e.symm.toAlgHom.comp (IsScalarTower.toAlgHom R _ S')).comp (AdjoinRoot.mkₐ P.f)) = aeval P.x := by ext; simp [e, StandardEtalePair.equivAwayAdjoinRoot] diff --git a/Mathlib/RingTheory/Extension/Basic.lean b/Mathlib/RingTheory/Extension/Basic.lean index ef31a53ee80797..f7ae93caf3b44a 100644 --- a/Mathlib/RingTheory/Extension/Basic.lean +++ b/Mathlib/RingTheory/Extension/Basic.lean @@ -135,11 +135,7 @@ def localization (P : Extension.{w} R S) : Extension R S' where (g := (algebraMap S S').comp (algebraMap P.Ring S)) (by simpa using fun x hx ↦ IsLocalization.map_units S' ⟨_, hx⟩)).toAlgebra isScalarTower := by - let : Algebra (Localization (M.comap (algebraMap P.Ring S))) S' := - (IsLocalization.lift (M := (M.comap (algebraMap P.Ring S))) - (g := (algebraMap S S').comp (algebraMap P.Ring S)) - (by simpa using fun x hx ↦ IsLocalization.map_units S' ⟨_, hx⟩)).toAlgebra - apply IsScalarTower.of_algebraMap_eq' + apply +allowSynthFailures IsScalarTower.of_algebraMap_eq' rw [RingHom.algebraMap_toAlgebra, IsScalarTower.algebraMap_eq R P.Ring (Localization _), ← RingHom.comp_assoc, IsLocalization.lift_comp, RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq] diff --git a/Mathlib/RingTheory/Finiteness/FiniteTypeLocal.lean b/Mathlib/RingTheory/Finiteness/FiniteTypeLocal.lean index a095ecda7d6a6d..937392a27e4a3a 100644 --- a/Mathlib/RingTheory/Finiteness/FiniteTypeLocal.lean +++ b/Mathlib/RingTheory/Finiteness/FiniteTypeLocal.lean @@ -67,16 +67,17 @@ then there exists some `m : M` such that `m • x` falls in the adjoin of `IsLocalization.finsetIntegerMultiple _ s` over `R`. -/ theorem IsLocalization.lift_mem_adjoin_finsetIntegerMultiple [Algebra R S'] - [IsScalarTower R S S'] [IsLocalization (M.map (algebraMap R S)) S'] (x : S) (s : Finset S') - (hx : algebraMap S S' x ∈ Algebra.adjoin R (s : Set S')) : - ∃ m : M, m • x ∈ - Algebra.adjoin R - (IsLocalization.finsetIntegerMultiple (M.map (algebraMap R S)) s : Set S) := by + [IsScalarTower R S S'] [IsLocalization (M.map (MonoidHomClass.toMonoidHom (algebraMap R S))) S'] + (x : S) (s : Finset S') (hx : algebraMap S S' x ∈ Algebra.adjoin R (s : Set S')) : + ∃ m : M, m • x ∈ Algebra.adjoin R (IsLocalization.finsetIntegerMultiple + (M.map (MonoidHomClass.toMonoidHom (algebraMap R S))) s : Set S) := by obtain ⟨⟨_, a, ha, rfl⟩, e⟩ := - IsLocalization.exists_smul_mem_of_mem_adjoin (M.map (algebraMap R S)) x s (Algebra.adjoin R _) + IsLocalization.exists_smul_mem_of_mem_adjoin + (M.map (MonoidHomClass.toMonoidHom (algebraMap R S))) x s (Algebra.adjoin R _) Algebra.subset_adjoin (by rintro _ ⟨a, _, rfl⟩; exact Subalgebra.algebraMap_mem _ a) hx refine ⟨⟨a, ha⟩, ?_⟩ - simpa only [Submonoid.smul_def, algebraMap_smul] using e + rw [Submonoid.smul_def] at e + simpa [-smul_eq_mul, algebraMap_smul] using e /-- Finite-type can be checked on a standard covering of the target. -/ lemma Algebra.FiniteType.of_span_eq_top_target (s : Set S) (hs : Ideal.span (s : Set S) = ⊤) diff --git a/Mathlib/RingTheory/FractionalIdeal/Extended.lean b/Mathlib/RingTheory/FractionalIdeal/Extended.lean index cfd6b34781258a..38a76e1ee276fb 100644 --- a/Mathlib/RingTheory/FractionalIdeal/Extended.lean +++ b/Mathlib/RingTheory/FractionalIdeal/Extended.lean @@ -227,7 +227,7 @@ theorem extendedHom'_comp {C W : Type*} [CommRing C] [CommRing W] [Algebra C W] (extendedHom' (A := B) (K := L) W hg).comp (extendedHom' (A := A) (K := K) L hf) = extendedHom' (A := A) (B := C) (f := g.comp f) (K := K) W - (hf.trans (Submonoid.monotone_comap (f := f) hg)) := by + (hf.trans (Submonoid.monotone_comap (f := f.toMonoidHom) hg)) := by apply RingHom.ext intro I exact extended_extended (A := A) (B := B) (f := f) (K := K) (M := M) (L := L) diff --git a/Mathlib/RingTheory/FractionalIdeal/Operations.lean b/Mathlib/RingTheory/FractionalIdeal/Operations.lean index dd6730c6a47630..3c66716426adb6 100644 --- a/Mathlib/RingTheory/FractionalIdeal/Operations.lean +++ b/Mathlib/RingTheory/FractionalIdeal/Operations.lean @@ -220,7 +220,7 @@ ideals in `P` and in `P'`, which are both localizations of `R` at `S`. -/ noncomputable irreducible_def canonicalEquiv : FractionalIdeal S P ≃+* FractionalIdeal S P' := mapEquiv { ringEquivOfRingEquiv P P' (RingEquiv.refl R) - (show S.map _ = S by rw [RingEquiv.toMonoidHom_refl, Submonoid.map_id]) with + (show S.map _ = S by simp) with commutes' := fun _ => ringEquivOfRingEquiv_eq _ _ } @[simp] diff --git a/Mathlib/RingTheory/Ideal/Maps.lean b/Mathlib/RingTheory/Ideal/Maps.lean index d3597ae968d410..dc4ba99678c33d 100644 --- a/Mathlib/RingTheory/Ideal/Maps.lean +++ b/Mathlib/RingTheory/Ideal/Maps.lean @@ -514,14 +514,16 @@ theorem mem_map_of_equiv {E : Type*} [EquivLike E R S] [RingEquivClass E R S] (e · rintro ⟨x, hx, rfl⟩ exact mem_map_of_mem e hx -lemma map_primeCompl_comap_of_surjective (hf : Function.Surjective f) (p : Ideal S) [p.IsPrime] : - Submonoid.map f (p.comap f).primeCompl = p.primeCompl := by +lemma map_primeCompl_comap_of_surjective (f : R →+* S) (hf : Function.Surjective f) + (p : Ideal S) [p.IsPrime] : + Submonoid.map f.toMonoidHom (p.comap f).primeCompl = p.primeCompl := by rw [SetLike.ext_iff, hf.forall] - grind [Submonoid.mem_map, mem_primeCompl_iff, mem_comap] + simp + grind lemma _root_.RingEquiv.map_primeCompl_comap_eq (e : R ≃+* S) (p : Ideal S) [p.IsPrime] : (p.comap e).primeCompl.map e = p.primeCompl := - p.map_primeCompl_comap_of_surjective e e.surjective + p.map_primeCompl_comap_of_surjective e.toRingHom e.surjective section Bijective @@ -702,7 +704,7 @@ theorem le_comap_pow (n : ℕ) : K.comap f ^ n ≤ (K ^ n).comap f := by lemma disjoint_map_primeCompl_iff_comap_le {S : Type*} [Semiring S] {f : R →+* S} {p : Ideal R} {I : Ideal S} [p.IsPrime] : - Disjoint (I : Set S) (p.primeCompl.map f) ↔ I.comap f ≤ p := + Disjoint (I : Set S) (p.primeCompl.map f.toMonoidHom) ↔ I.comap f ≤ p := (@Set.disjoint_image_right _ _ f p.primeCompl I).trans disjoint_compl_right_iff /-- For a prime ideal `p` of `R`, `p` extended to `S` and diff --git a/Mathlib/RingTheory/Ideal/Norm/RelNorm.lean b/Mathlib/RingTheory/Ideal/Norm/RelNorm.lean index 37680f001821b4..f975120631a79f 100644 --- a/Mathlib/RingTheory/Ideal/Norm/RelNorm.lean +++ b/Mathlib/RingTheory/Ideal/Norm/RelNorm.lean @@ -146,9 +146,8 @@ theorem spanIntNorm_localization (I : Ideal S) (M : Submonoid R) (hM : M ≤ R apply_fun algebraMap _ L at has apply_fun Algebra.norm K at has simp only [map_mul] at has - rw [← IsScalarTower.algebraMap_apply, ← IsScalarTower.algebraMap_apply, - ← IsScalarTower.algebraMap_apply, - IsScalarTower.algebraMap_apply R K L, + rw [MonoidHom.coe_coe, ← IsScalarTower.algebraMap_apply, ← IsScalarTower.algebraMap_apply, + ← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply R K L, Algebra.norm_algebraMap] at has apply IsFractionRing.injective Rₘ K simp only [map_mul, map_pow] diff --git a/Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean b/Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean index 012aab7f2177cc..dd0eb2cc763434 100644 --- a/Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean +++ b/Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean @@ -94,8 +94,7 @@ def galLift (σ : B →ₐ[A] B₂) : L →ₐ[K] L₂ := haveI H : ∀ (y : Algebra.algebraMapSubmonoid B A⁰), IsUnit (((algebraMap B₂ L₂).comp σ) (y : B)) := by rintro ⟨_, x, hx, rfl⟩ - simpa only [RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply, AlgHom.commutes, - isUnit_iff_ne_zero, ne_eq, map_eq_zero_iff _ (FaithfulSMul.algebraMap_injective _ _), + simpa [map_eq_zero_iff _ (FaithfulSMul.algebraMap_injective _ _), ← IsScalarTower.algebraMap_apply] using nonZeroDivisors.ne_zero hx haveI H_eq : (IsLocalization.lift (S := L) H).comp (algebraMap K L) = (algebraMap K L₂) := by apply IsLocalization.ringHom_ext A⁰ diff --git a/Mathlib/RingTheory/Jacobson/Ring.lean b/Mathlib/RingTheory/Jacobson/Ring.lean index 6a9613649e0abf..4f2d9a270797e8 100644 --- a/Mathlib/RingTheory/Jacobson/Ring.lean +++ b/Mathlib/RingTheory/Jacobson/Ring.lean @@ -462,9 +462,7 @@ theorem isMaximal_comap_C_of_isMaximal [IsJacobsonRing R] [Nontrivial R] (IsLocalization.map_injective_of_injective M (Localization M) (Localization M') quotientMap_injective))] refine isMaximal_comap_of_isIntegral_of_isMaximal _ ?_ ⊥ - have isloc : IsLocalization (Submonoid.map φ M) (Localization M') := by infer_instance - exact @isIntegral_isLocalization_polynomial_quotient R _ - (Localization M) (Localization M') _ _ P m hmem_P _ _ _ isloc + exact isIntegral_isLocalization_polynomial_quotient P m hmem_P rw [(map_bot.symm : (⊥ : Ideal (Localization M')) = Ideal.map (algebraMap (R[X] ⧸ P) (Localization M')) ⊥)] let bot_maximal := (bot_quotient_isMaximal_iff _).mpr hP diff --git a/Mathlib/RingTheory/KrullDimension/Polynomial.lean b/Mathlib/RingTheory/KrullDimension/Polynomial.lean index dd6c596743a973..7411d99c53f605 100644 --- a/Mathlib/RingTheory/KrullDimension/Polynomial.lean +++ b/Mathlib/RingTheory/KrullDimension/Polynomial.lean @@ -87,18 +87,20 @@ lemma height_eq_height_add_one (p : Ideal R) rw [p'_def, Localization.AtPrime.map_eq_maximalIdeal] exact IsLocalRing.maximalIdeal.isMaximal Rₚ let P' : Ideal Rₚ[X] := P.map (algebraMap R[X] Rₚ[X]) - have disj : Disjoint (p.primeCompl.map C : Set R[X]) P := by + have disj : Disjoint (p.primeCompl.map C.toMonoidHom : Set R[X]) P := by refine Set.disjoint_left.mpr fun a ⟨b, hb⟩ ha ↦ hb.1 ?_ + simp only [RingHom.toMonoidHom_eq_coe, MonoidHom.coe_coe] at hb rwa [SetLike.mem_coe, LiesOver.over (P := P) (p := p), mem_comap, algebraMap_eq, hb.2] have eq := under_map_of_isPrime_disjoint _ Rₚ[X] ‹P.IsMaximal›.isPrime disj have : (P'.under R[X]).IsMaximal := eq.symm ▸ ‹P.IsMaximal› - have : P'.IsMaximal := IsLocalization.isMaximal_of_isMaximal_under (p.primeCompl.map C) Rₚ[X] P' + have : P'.IsMaximal := + IsLocalization.isMaximal_of_isMaximal_under (p.primeCompl.map C.toMonoidHom) Rₚ[X] P' have : P'.LiesOver p' := liesOver_of_isPrime_of_disjoint p.primeCompl _ _ disj have eq1 : p.height = p'.height := by rw [height_map_of_disjoint p.primeCompl] exact Disjoint.symm <| Set.disjoint_left.mpr fun _ a b ↦ b a have eq2 : P.height = P'.height := by - rw [height_map_of_disjoint (Submonoid.map C <| p.primeCompl) _ disj] + rw [height_map_of_disjoint (Submonoid.map C.toMonoidHom <| p.primeCompl) _ disj] rw [eq1, eq2] apply height_eq_height_add_one_of_isMaximal p' P' diff --git a/Mathlib/RingTheory/LocalProperties/Basic.lean b/Mathlib/RingTheory/LocalProperties/Basic.lean index af76a457e6a18a..105c2f58677a81 100644 --- a/Mathlib/RingTheory/LocalProperties/Basic.lean +++ b/Mathlib/RingTheory/LocalProperties/Basic.lean @@ -87,7 +87,7 @@ if `P` holds for `M⁻¹R →+* M⁻¹S` whenever `P` holds for `R →+* S`. -/ def RingHom.LocalizationPreserves := ∀ ⦃R S : Type u⦄ [CommRing R] [CommRing S] (f : R →+* S) (M : Submonoid R) (R' S' : Type u) [CommRing R'] [CommRing S'] [Algebra R R'] [Algebra S S'] [IsLocalization M R'] - [IsLocalization (M.map f) S'], + [IsLocalization (M.map (MonoidHomClass.toMonoidHom f)) S'], P f → P (IsLocalization.map S' f (Submonoid.le_comap_map M) : R' →+* S') /-- A property `P` of ring homs is said to be preserved by localization away @@ -257,22 +257,26 @@ lemma RingHom.HoldsForLocalization.isLocalizationMap (S' : Type u) [CommRing S'] [Algebra S S'] [IsLocalization T S'] {f : R →+* S} (hy : M ≤ Submonoid.comap f T) (hf : P f) : P (IsLocalization.map (S := R') S' f hy) := by - have hle : Submonoid.map f M ≤ T := by simpa [Submonoid.map_le_iff_le_comap] - let : Algebra (Localization (M.map f)) S' := - IsLocalization.localizationAlgebraOfSubmonoidLe _ _ (M.map f) T hle - have : IsScalarTower S (Localization (Submonoid.map f M)) S' := + have hle : Submonoid.map (MonoidHomClass.toMonoidHom f) M ≤ T := by + simpa [Submonoid.map_le_iff_le_comap] + let : Algebra (Localization (M.map (MonoidHomClass.toMonoidHom f))) S' := + IsLocalization.localizationAlgebraOfSubmonoidLe _ _ (M.map (MonoidHomClass.toMonoidHom f)) T hle + have : IsScalarTower S (Localization (Submonoid.map (MonoidHomClass.toMonoidHom f) M)) S' := IsLocalization.localization_isScalarTower_of_submonoid_le _ _ _ _ _ - have : IsLocalization (T.map (algebraMap S (Localization (M.map f)))) S' := - IsLocalization.isLocalization_of_submonoid_le _ _ (M.map f) T hle + have : IsLocalization (T.map (algebraMap S + (Localization (M.map (MonoidHomClass.toMonoidHom f)))).toMonoidHom) S' := + IsLocalization.isLocalization_of_submonoid_le _ _ (M.map (MonoidHomClass.toMonoidHom f)) T hle have heq : IsLocalization.map (S := R') S' f hy = - (algebraMap _ _).comp - (IsLocalization.map (M := M) (T := M.map f) (S := R') (Localization (M.map f)) f + (algebraMap (Localization (Submonoid.map ((MonoidHomClass.toMonoidHom f)) M)) _).comp + (IsLocalization.map (M := M) (T := M.map (MonoidHomClass.toMonoidHom f)) (S := R') + (Localization (M.map (MonoidHomClass.toMonoidHom f))) f (M.le_comap_map)) := by apply IsLocalization.ringHom_ext M - ext + ext x simp [← IsScalarTower.algebraMap_apply] rw [heq] - exact hPc _ _ (hPp _ _ _ _ hf) (hPl _ (T.map (algebraMap S (Localization (M.map f))))) + exact hPc _ _ (hPp _ _ _ _ hf) + (hPl _ (T.map (algebraMap S (Localization (M.map (MonoidHomClass.toMonoidHom f)))).toMonoidHom)) lemma RingHom.HoldsForLocalization.localRingHom (hPc : StableUnderComposition P) (hPp : LocalizationPreserves P) (hPl : HoldsForLocalization P) @@ -356,7 +360,8 @@ theorem RingHom.PropertyIsLocal.respectsIso (hP : RingHom.PropertyIsLocal @P) : theorem RingHom.LocalizationPreserves.away (H : RingHom.LocalizationPreserves @P) : RingHom.LocalizationAwayPreserves P := by intro R S _ _ f r R' S' _ _ _ _ _ _ hf - have : IsLocalization ((Submonoid.powers r).map f) S' := by rwa [Submonoid.map_powers] + have : IsLocalization ((Submonoid.powers r).map (MonoidHomClass.toMonoidHom f)) S' := by + rwa [Submonoid.map_powers] exact H f (Submonoid.powers r) R' S' hf lemma RingHom.PropertyIsLocal.HoldsForLocalizationAway (hP : RingHom.PropertyIsLocal @P) @@ -497,14 +502,15 @@ lemma RingHom.IsStableUnderBaseChange.of_isLocalization [Algebra R S] [Algebra R /-- If `P` is stable under base change and holds for `f`, then `P` holds for `f` localized at any submonoid `M` of `R`. -/ lemma RingHom.IsStableUnderBaseChange.isLocalization_map (M : Submonoid R) [IsLocalization M Rᵣ] - (f : R →+* S) [IsLocalization (M.map f) Sᵣ] (hf : P f) : - P (IsLocalization.map Sᵣ f M.le_comap_map : Rᵣ →+* Sᵣ) := by + (f : R →+* S) [IsLocalization (M.map (MonoidHomClass.toMonoidHom f)) Sᵣ] (hf : P f) : + P (IsLocalization.map Sᵣ f (M.le_comap_map + (f := (MonoidHomClass.toMonoidHom f))) : Rᵣ →+* Sᵣ) := by algebraize [f, IsLocalization.map (S := Rᵣ) Sᵣ f M.le_comap_map, (IsLocalization.map (S := Rᵣ) Sᵣ f M.le_comap_map).comp (algebraMap R Rᵣ)] have : IsScalarTower R S Sᵣ := IsScalarTower.of_algebraMap_eq' (IsLocalization.map_comp M.le_comap_map) have : IsLocalization (Algebra.algebraMapSubmonoid S M) Sᵣ := - inferInstanceAs <| IsLocalization (M.map f) Sᵣ + inferInstanceAs <| IsLocalization (M.map (MonoidHomClass.toMonoidHom f)) Sᵣ apply hP.of_isLocalization M hf lemma RingHom.IsStableUnderBaseChange.localizationPreserves : LocalizationPreserves P := by diff --git a/Mathlib/RingTheory/LocalRing/ResidueField/Ideal.lean b/Mathlib/RingTheory/LocalRing/ResidueField/Ideal.lean index 84ce960053b24d..7dae721149d488 100644 --- a/Mathlib/RingTheory/LocalRing/ResidueField/Ideal.lean +++ b/Mathlib/RingTheory/LocalRing/ResidueField/Ideal.lean @@ -127,7 +127,7 @@ instance : IsFractionRing (R ⧸ I) I.ResidueField where instance [IsDomain R] : IsFractionRing R (⊥ : Ideal R).ResidueField := IsLocalization.of_ringEquiv_left (RingEquiv.quotientBot R).symm - (MulEquivClass.map_nonZeroDivisors (RingEquiv.quotientBot R).symm) (by simp) + (MulEquivClass.map_nonZeroDivisors (RingEquiv.quotientBot R).symm.toMulEquiv) (by simp) instance [Finite (R ⧸ I)] : Finite I.ResidueField := IsLocalization.finite (R ⧸ I) (nonZeroDivisors (R ⧸ I)) diff --git a/Mathlib/RingTheory/LocalRing/ResidueField/Polynomial.lean b/Mathlib/RingTheory/LocalRing/ResidueField/Polynomial.lean index a6c602b8dc31f2..1d6c186e217fd9 100644 --- a/Mathlib/RingTheory/LocalRing/ResidueField/Polynomial.lean +++ b/Mathlib/RingTheory/LocalRing/ResidueField/Polynomial.lean @@ -140,7 +140,8 @@ theorem _root_.Ideal.exists_mem_span_singleton_map_residueField_eq rw [Ideal.map_map, RingHom.algebraMap_toAlgebra, mapRingHom_comp, ← IsScalarTower.algebraMap_eq, hp] exact Ideal.mem_span_singleton_self _ - obtain ⟨⟨⟨r, hr⟩, s⟩, e⟩ := (IsLocalization.mem_map_algebraMap_iff ((R ⧸ P)⁰.map C) _).mp this + obtain ⟨⟨⟨r, hr⟩, s⟩, e⟩ := + (IsLocalization.mem_map_algebraMap_iff ((R ⧸ P)⁰.map C.toMonoidHom) _).mp this obtain ⟨r, hr', rfl⟩ := (Ideal.mem_map_iff_of_surjective _ (Polynomial.map_surjective _ Ideal.Quotient.mk_surjective)).mp hr simp only [algebraMap_def, coe_mapRingHom, diff --git a/Mathlib/RingTheory/Localization/Algebra.lean b/Mathlib/RingTheory/Localization/Algebra.lean index 666e70b429d273..8a8b600947c282 100644 --- a/Mathlib/RingTheory/Localization/Algebra.lean +++ b/Mathlib/RingTheory/Localization/Algebra.lean @@ -99,9 +99,8 @@ variable [Algebra Rₚ Aₚ] [Algebra Rₚ Bₚ] [IsScalarTower R Rₚ Aₚ] [Is namespace IsLocalization instance isLocalization_algebraMapSubmonoid_map_algHom (f : A →ₐ[R] B) : - IsLocalization ((algebraMapSubmonoid A M).map f.toRingHom) Bₚ := by - rw [AlgHom.toRingHom_eq_coe, ← Submonoid.map_coe_toMonoidHom, AlgHom.toRingHom_toMonoidHom, - Submonoid.map_coe_toMonoidHom, algebraMapSubmonoid_map_eq M f] + IsLocalization ((algebraMapSubmonoid A M).map (MonoidHomClass.toMonoidHom f)) Bₚ := by + rw [algebraMapSubmonoid_map_eq M f] infer_instance /-- An algebra map `A →ₐ[R] B` induces an algebra map on localizations `Aₚ →ₐ[Rₚ] Bₚ`. -/ @@ -117,10 +116,18 @@ lemma mapₐ_coe (f : A →ₐ[R] B) : lemma mapₐ_injective_of_injective (f : A →ₐ[R] B) (hf : Function.Injective f) : Function.Injective (mapₐ M Rₚ Aₚ Bₚ f) := + have : IsLocalization (Submonoid.map (MonoidHomClass.toMonoidHom f.toRingHom) + (algebraMapSubmonoid A M)) Bₚ := by + simp only [AlgHom.toRingHom_eq_coe, AlgHom.toRingHom_toMonoidHom] + infer_instance IsLocalization.map_injective_of_injective _ _ _ hf lemma mapₐ_surjective_of_surjective (f : A →ₐ[R] B) (hf : Function.Surjective f) : Function.Surjective (mapₐ M Rₚ Aₚ Bₚ f) := + have : IsLocalization (Submonoid.map (MonoidHomClass.toMonoidHom f.toRingHom) + (algebraMapSubmonoid A M)) Bₚ := by + simp only [AlgHom.toRingHom_eq_coe, AlgHom.toRingHom_toMonoidHom] + infer_instance IsLocalization.map_surjective_of_surjective _ _ _ hf section @@ -190,7 +197,7 @@ attribute [local instance] Polynomial.algebra in See also `MvPolynomial.isLocalization` for the multivariate case. -/ lemma isLocalization {R} [CommSemiring R] (S : Submonoid R) (A) [CommSemiring A] [Algebra R A] - [IsLocalization S A] : IsLocalization (S.map C) A[X] := + [IsLocalization S A] : IsLocalization (S.map C.toMonoidHom) A[X] := isLocalizedModule_iff_isLocalization.mp <| (isLocalizedModule_iff_isBaseChange S A _).mpr <| .of_equiv (polyEquivTensor' R A).symm.toLinearEquiv fun _ ↦ by simp diff --git a/Mathlib/RingTheory/Localization/AtPrime/Basic.lean b/Mathlib/RingTheory/Localization/AtPrime/Basic.lean index 7eebc43c1d7f01..e3e7cc29273e87 100644 --- a/Mathlib/RingTheory/Localization/AtPrime/Basic.lean +++ b/Mathlib/RingTheory/Localization/AtPrime/Basic.lean @@ -659,7 +659,8 @@ lemma under_map_eq_map : (Ideal.map (algebraMap R Sₚ) p).under S = pS := by obtain ⟨c, hc⟩ := hy obtain ⟨α, hα, e⟩ := (c * s).prop refine ⟨α, hα, ?_⟩ - rw [Algebra.smul_def, e, Submonoid.coe_mul, mul_assoc, mul_comm _ x, hc] + simp only [MonoidHom.coe_coe, Submonoid.coe_mul] at e + rw [Algebra.smul_def, e, mul_assoc, mul_comm _ x, hc] exact Ideal.mul_mem_left _ _ y.prop obtain ⟨β, γ, hγ, hβ⟩ : ∃ β γ, γ ∈ p ∧ β * α = 1 + γ := by obtain ⟨β, hβ⟩ := Ideal.Quotient.mk_surjective (I := p) (Ideal.Quotient.mk p α)⁻¹ @@ -713,7 +714,7 @@ noncomputable def equivQuotientMapMaximalIdeal : S ⧸ pS ≃+* Sₚ ⧸ pSₚ : · rw [Algebra.smul_def] apply Ideal.mul_mem_right exact Ideal.mem_map_of_mem _ hγ - simp only + simp only [MonoidHom.coe_coe] at e ⊢ rw [mul_comm, mul_sub, IsLocalization.mul_mk'_eq_mk'_of_mul, IsLocalization.mk'_mul_cancel_left, ← map_mul, ← e, ← Algebra.smul_def, smul_smul, hβ, ← map_sub, add_smul, one_smul, add_comm x, add_sub_cancel_right] diff --git a/Mathlib/RingTheory/Localization/Away/Basic.lean b/Mathlib/RingTheory/Localization/Away/Basic.lean index 8bed43f5f6144b..81ab5dabc8a7b8 100644 --- a/Mathlib/RingTheory/Localization/Away/Basic.lean +++ b/Mathlib/RingTheory/Localization/Away/Basic.lean @@ -239,7 +239,8 @@ variable {B : Type*} [CommSemiring B] [Algebra R B] variable (Aₚ : Type*) [CommSemiring Aₚ] [Algebra A Aₚ] [Algebra R Aₚ] [IsScalarTower R A Aₚ] variable (Bₚ : Type*) [CommSemiring Bₚ] [Algebra B Bₚ] [Algebra R Bₚ] [IsScalarTower R B Bₚ] -instance {f : A →+* B} (a : A) [Away (f a) Bₚ] : IsLocalization (.map f (.powers a)) Bₚ := by +instance map_toMonoidHom_powers {f : A →+* B} (a : A) [Away (f a) Bₚ] : + IsLocalization (.map (MonoidHomClass.toMonoidHom f) (.powers a)) Bₚ := by simpa instance (x : R) [IsLocalization.Away (algebraMap R A x) Aₚ] : @@ -264,12 +265,17 @@ variable {Aₚ} {Bₚ} lemma mapₐ_injective_of_injective {f : A →ₐ[R] B} (a : A) [Away a Aₚ] [Away (f a) Bₚ] (hf : Function.Injective f) : Function.Injective (mapₐ Aₚ Bₚ f a) := + have : IsLocalization (Submonoid.map (MonoidHomClass.toMonoidHom f.toRingHom) + (Submonoid.powers a)) Bₚ := by + simp only [Submonoid.map_powers, MonoidHom.coe_coe] + infer_instance IsLocalization.map_injective_of_injective _ _ _ hf lemma mapₐ_surjective_of_surjective {f : A →ₐ[R] B} (a : A) [Away a Aₚ] [Away (f a) Bₚ] (hf : Function.Surjective f) : Function.Surjective (mapₐ Aₚ Bₚ f a) := - have : IsLocalization (Submonoid.map f.toRingHom (Submonoid.powers a)) Bₚ := by - simp only [AlgHom.toRingHom_eq_coe, Submonoid.map_powers, RingHom.coe_coe] + have : IsLocalization (Submonoid.map (MonoidHomClass.toMonoidHom f.toRingHom) + (Submonoid.powers a)) Bₚ := by + simp only [Submonoid.map_powers, MonoidHom.coe_coe] infer_instance IsLocalization.map_surjective_of_surjective _ _ _ hf diff --git a/Mathlib/RingTheory/Localization/BaseChange.lean b/Mathlib/RingTheory/Localization/BaseChange.lean index 7f2e4bbf9bcc3d..7f05b373e1e8c4 100644 --- a/Mathlib/RingTheory/Localization/BaseChange.lean +++ b/Mathlib/RingTheory/Localization/BaseChange.lean @@ -374,7 +374,8 @@ lemma IsLocalization.tensorProduct_tensorProduct_right (M : Submonoid A) [Algebra (S ⊗[R] A) (S ⊗[R] B)] [IsScalarTower S (S ⊗[R] A) (S ⊗[R] B)] (H : (algebraMap (S ⊗[R] A) (S ⊗[R] B)).comp Algebra.TensorProduct.includeRight.toRingHom = Algebra.TensorProduct.includeRight.toRingHom.comp (algebraMap A B)) : - IsLocalization (M.map (Algebra.TensorProduct.includeRight (R := R) (A := S))) (S ⊗[R] B) := by + IsLocalization + (M.map (Algebra.TensorProduct.includeRight (R := R) (A := S)).toMonoidHom) (S ⊗[R] B) := by change IsLocalization (Algebra.algebraMapSubmonoid _ M) (S ⊗[R] B) let : Algebra A (S ⊗[R] B) := .compHom _ (algebraMap A B) have : IsScalarTower A (S ⊗[R] A) (S ⊗[R] B) := .of_algebraMap_eq' H.symm @@ -395,9 +396,10 @@ def IsLocalization.tensorProductEquivOfMapIncludeRight (M : Submonoid A) (B : Type*) [CommSemiring B] [Algebra R B] [Algebra A B] [IsScalarTower R A B] [IsLocalization M B] (C : Type*) [CommSemiring C] [Algebra S C] [Algebra (S ⊗[R] A) C] [IsScalarTower S (S ⊗[R] A) C] - [IsLocalization (M.map (Algebra.TensorProduct.includeRight (R := R) (A := S))) C] : + [IsLocalization (M.map (Algebra.TensorProduct.includeRight (R := R) (A := S)).toMonoidHom) C] : S ⊗[R] B ≃ₐ[S] C := - letI M' : Submonoid (S ⊗[R] A) := M.map (Algebra.TensorProduct.includeRight (R := R) (A := S)) + letI M' : Submonoid (S ⊗[R] A) := + M.map (Algebra.TensorProduct.includeRight (R := R) (A := S)).toMonoidHom letI : Algebra (S ⊗[R] A) (S ⊗[R] B) := (Algebra.TensorProduct.map (AlgHom.id R S) (IsScalarTower.toAlgHom R _ _)).toAlgebra haveI : IsScalarTower S (S ⊗[R] A) (S ⊗[R] B) := @@ -412,7 +414,7 @@ lemma IsLocalization.tensorProductEquivOfMapIncludeRight_tmul (M : Submonoid A) (B : Type*) [CommSemiring B] [Algebra R B] [Algebra A B] [IsScalarTower R A B] [IsLocalization M B] (C : Type*) [CommSemiring C] [Algebra S C] [Algebra (S ⊗[R] A) C] [IsScalarTower S (S ⊗[R] A) C] - [IsLocalization (M.map (Algebra.TensorProduct.includeRight (R := R) (A := S))) C] + [IsLocalization (M.map (Algebra.TensorProduct.includeRight (R := R) (A := S)).toMonoidHom) C] (x : S) (a : A) : IsLocalization.tensorProductEquivOfMapIncludeRight R S M B C (x ⊗ₜ algebraMap A B a) = algebraMap _ _ (x ⊗ₜ[R] a) := by @@ -428,9 +430,10 @@ def IsLocalization.Away.tensorProductEquivTMulRight (g : A) (B : Type*) [CommSem [Algebra R B] [Algebra A B] [IsScalarTower R A B] [IsLocalization.Away g B] : S ⊗[R] B ≃ₐ[S] Localization.Away ((1 : S) ⊗ₜ[R] g) := haveI : IsLocalization - ((Submonoid.powers g).map (Algebra.TensorProduct.includeRight (R := R) (A := S))) + ((Submonoid.powers g).map (Algebra.TensorProduct.includeRight (R := R) (A := S)).toMonoidHom) (Localization.Away ((1 : S) ⊗ₜ[R] g)) := by - simp only [Submonoid.map_powers, Algebra.TensorProduct.includeRight_apply] + simp only [AlgHom.toRingHom_eq_coe, RingHom.toMonoidHom_eq_coe, AlgHom.toRingHom_toMonoidHom, + Submonoid.map_powers, MonoidHom.coe_coe, Algebra.TensorProduct.includeRight_apply] infer_instance IsLocalization.tensorProductEquivOfMapIncludeRight _ _ (.powers g) _ _ @@ -441,9 +444,10 @@ lemma IsLocalization.Away.tensorProductEquivTMulRight_tmul (g : A) (B : Type*) [ IsLocalization.Away.tensorProductEquivTMulRight R S g B (x ⊗ₜ algebraMap _ _ a) = algebraMap _ _ (x ⊗ₜ[R] a) := haveI : IsLocalization - ((Submonoid.powers g).map (Algebra.TensorProduct.includeRight (R := R) (A := S))) + ((Submonoid.powers g).map (Algebra.TensorProduct.includeRight (R := R) (A := S)).toMonoidHom) (Localization.Away ((1 : S) ⊗ₜ[R] g)) := by - simp only [Submonoid.map_powers, Algebra.TensorProduct.includeRight_apply] + simp only [AlgHom.toRingHom_eq_coe, RingHom.toMonoidHom_eq_coe, AlgHom.toRingHom_toMonoidHom, + Submonoid.map_powers, MonoidHom.coe_coe, Algebra.TensorProduct.includeRight_apply] infer_instance IsLocalization.tensorProductEquivOfMapIncludeRight_tmul _ _ _ _ _ _ diff --git a/Mathlib/RingTheory/Localization/Basic.lean b/Mathlib/RingTheory/Localization/Basic.lean index 8767d1701d07bd..323e3dd8f17e35 100644 --- a/Mathlib/RingTheory/Localization/Basic.lean +++ b/Mathlib/RingTheory/Localization/Basic.lean @@ -85,12 +85,12 @@ variable {i : ι} (S : Submonoid (R i)) /-- `IsLocalization.map` applied to a projection homomorphism from a product ring. -/ noncomputable abbrev mapPiEvalRingHom : - Localization (S.comap <| Pi.evalRingHom R i) →+* Localization S := + Localization (S.comap (MonoidHomClass.toMonoidHom (Pi.evalRingHom R i))) →+* Localization S := map (T := S) _ (Pi.evalRingHom R i) le_rfl open Function in theorem mapPiEvalRingHom_bijective : Bijective (mapPiEvalRingHom S) := by - let T := S.comap (Pi.evalRingHom R i) + let T := S.comap (MonoidHomClass.toMonoidHom (Pi.evalRingHom R i)) classical refine ⟨fun x₁ x₂ eq ↦ ?_, fun x ↦ ?_⟩ · obtain ⟨r₁, s₁, rfl⟩ := exists_mk'_eq T x₁ @@ -253,11 +253,11 @@ theorem algEquivOfAlgEquiv_mk' (x : R) (y : M) : mk' Q (h x) ⟨h y, show h y ∈ T from H ▸ Set.mem_image_of_mem h y.2⟩ := by simp [map_mk'] -theorem algEquivOfAlgEquiv_symm : (algEquivOfAlgEquiv S Q h H).symm = - algEquivOfAlgEquiv Q S h.symm (show Submonoid.map h.symm T = M by - rw [← H, ← Submonoid.map_coe_toMulEquiv, AlgEquiv.symm_toMulEquiv, - ← Submonoid.comap_equiv_eq_map_symm, ← Submonoid.map_coe_toMulEquiv, - Submonoid.comap_map_eq_of_injective (h : R ≃* P).injective]) := rfl +theorem algEquivOfAlgEquiv_symm : + (algEquivOfAlgEquiv S Q h H).symm = + algEquivOfAlgEquiv Q S h.symm (show Submonoid.map h.symm.toMonoidHom T = M by + rw [← H]; convert Submonoid.map_id M; ext; simp) := + rfl end AlgEquivOfAlgEquiv @@ -330,7 +330,7 @@ theorem isLocalization_of_algEquiv [Algebra R P] [IsLocalization M S] (h : S ≃ IsLocalization M P := by constructor; constructor · intro y - convert! (IsLocalization.map_units S y).map h.toAlgHom.toRingHom.toMonoidHom + convert! (IsLocalization.map_units S y).map (MonoidHomClass.toMonoidHom h) exact (h.commutes y).symm · intro y obtain ⟨⟨x, s⟩, e⟩ := IsLocalization.surj M (h.symm y) @@ -384,10 +384,12 @@ lemma commutes (S₁ S₂ T : Type*) [CommSemiring S₁] IsLocalization (Algebra.algebraMapSubmonoid S₁ M₂) T where map_units := by rintro ⟨m, ⟨a, ha, rfl⟩⟩ + simp only [MonoidHom.coe_coe] rw [← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply R S₂ T] exact IsUnit.map _ (IsLocalization.map_units _ ⟨a, ha⟩) surj a := by obtain ⟨⟨y, -, m, hm, rfl⟩, hy⟩ := surj (M := Algebra.algebraMapSubmonoid S₂ M₁) a + simp only [MonoidHom.coe_coe] at hy rw [← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply R S₁ T] at hy obtain ⟨⟨z, n, hn⟩, hz⟩ := IsLocalization.surj (M := M₂) y have hunit : IsUnit (algebraMap R S₁ m) := map_units _ ⟨m, hm⟩ @@ -406,6 +408,7 @@ lemma commutes (S₁ S₂ T : Type*) [CommSemiring S₁] simp_rw [← map_mul, hr, hs, ← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply R S₂ T] at hxy obtain ⟨⟨-, c, hmc, rfl⟩, hc⟩ := exists_of_eq (M := Algebra.algebraMapSubmonoid S₂ M₁) hxy + simp only [MonoidHom.coe_coe] at hc simp_rw [← map_mul] at hc obtain ⟨a, ha⟩ := IsLocalization.exists_of_eq (M := M₂) hc use ⟨algebraMap R S₁ a, a, a.property, rfl⟩ @@ -618,7 +621,7 @@ theorem localizationAlgebraMap_def : /-- Injectivity of the underlying `algebraMap` descends to the algebra induced by localization. -/ theorem localizationAlgebra_injective (hRS : Function.Injective (algebraMap R S)) : Function.Injective (@algebraMap Rₘ Sₘ _ _ (localizationAlgebra M S)) := - have : IsLocalization (M.map (algebraMap R S)) Sₘ := i + have : IsLocalization (M.map (MonoidHomClass.toMonoidHom (algebraMap R S))) Sₘ := i IsLocalization.map_injective_of_injective _ _ _ hRS instance : IsLocalization (Algebra.algebraMapSubmonoid R M) Rₘ := by diff --git a/Mathlib/RingTheory/Localization/Defs.lean b/Mathlib/RingTheory/Localization/Defs.lean index cd24e373b44241..f5e546186a10af 100644 --- a/Mathlib/RingTheory/Localization/Defs.lean +++ b/Mathlib/RingTheory/Localization/Defs.lean @@ -666,8 +666,9 @@ set_option backward.isDefEq.respectTransparency false in isomorphism `j : R ≃+* P` such that `j(M) = T` induces an isomorphism of localizations `S ≃+* Q`. -/ @[simps apply] -noncomputable def ringEquivOfRingEquiv (h : R ≃+* P) (H : M.map h.toMonoidHom = T) : S ≃+* Q := - have H' : T.map h.symm.toMonoidHom = M := by +noncomputable def ringEquivOfRingEquiv (h : R ≃+* P) + (H : M.map (MonoidHomClass.toMonoidHom h) = T) : S ≃+* Q := + have H' : T.map (MonoidHomClass.toMonoidHom h.symm) = M := by rw [← M.map_id, ← H, Submonoid.map_map] congr ext @@ -684,26 +685,25 @@ noncomputable def ringEquivOfRingEquiv (h : R ≃+* P) (H : M.map h.toMonoidHom end -theorem ringEquivOfRingEquiv_eq_map {j : R ≃+* P} (H : M.map j.toMonoidHom = T) : +theorem ringEquivOfRingEquiv_eq_map {j : R ≃+* P} (H : M.map (MonoidHomClass.toMonoidHom j) = T) : (ringEquivOfRingEquiv S Q j H : S →+* Q) = map Q (j : R →+* P) (M.le_comap_of_map_le (le_of_eq H)) := rfl -theorem ringEquivOfRingEquiv_eq {j : R ≃+* P} (H : M.map j.toMonoidHom = T) (x) : +theorem ringEquivOfRingEquiv_eq {j : R ≃+* P} (H : M.map (MonoidHomClass.toMonoidHom j) = T) (x) : ringEquivOfRingEquiv S Q j H ((algebraMap R S) x) = algebraMap P Q (j x) := by simp -theorem ringEquivOfRingEquiv_mk' {j : R ≃+* P} (H : M.map j.toMonoidHom = T) (x : R) (y : M) : - ringEquivOfRingEquiv S Q j H (mk' S x y) = - mk' Q (j x) ⟨j y, show j y ∈ T from H ▸ Set.mem_image_of_mem j y.2⟩ := by +theorem ringEquivOfRingEquiv_mk' {j : R ≃+* P} (H : M.map (MonoidHomClass.toMonoidHom j) = T) + (x : R) (y : M) : ringEquivOfRingEquiv S Q j H (mk' S x y) = + mk' Q (j x) ⟨j y, show j y ∈ T from H ▸ Set.mem_image_of_mem j y.2⟩ := by simp [map_mk'] @[simp] theorem ringEquivOfRingEquiv_symm {j : R ≃+* P} (H : M.map j = T) : (ringEquivOfRingEquiv S Q j H).symm = ringEquivOfRingEquiv Q S j.symm (show T.map (j : R ≃* P).symm = M by - rw [← H, ← Submonoid.comap_equiv_eq_map_symm, ← Submonoid.map_coe_toMulEquiv, - Submonoid.comap_map_eq_of_injective (j : R ≃* P).injective]) := rfl + rw [← H]; convert Submonoid.map_id M; ext; simp) := rfl end Map @@ -712,14 +712,19 @@ section variable (M S) (Q : Type*) [CommSemiring Q] [Algebra P Q] /-- Injectivity of a map descends to the map induced on localizations. -/ -theorem map_injective_of_injective (h : Function.Injective g) [IsLocalization (M.map g) Q] : - Function.Injective (map Q g M.le_comap_map : S → Q) := - (toLocalizationMap M S).map_injective_of_injective h (toLocalizationMap (M.map g) Q) +theorem map_injective_of_injective + (h : Function.Injective g) [IsLocalization (M.map (MonoidHomClass.toMonoidHom g)) Q] : + Function.Injective ((map Q g (M := M) (M.le_comap_map + (f := (MonoidHomClass.toMonoidHom g)))) : S → Q) := + (toLocalizationMap M S).map_injective_of_injective h + (toLocalizationMap (M.map (MonoidHomClass.toMonoidHom g)) Q) /-- Surjectivity of a map descends to the map induced on localizations. -/ -theorem map_surjective_of_surjective (h : Function.Surjective g) [IsLocalization (M.map g) Q] : - Function.Surjective (map Q g M.le_comap_map : S → Q) := - (toLocalizationMap M S).map_surjective_of_surjective h (toLocalizationMap (M.map g) Q) +theorem map_surjective_of_surjective + (h : Function.Surjective g) [IsLocalization (M.map (MonoidHomClass.toMonoidHom g)) Q] : + Function.Surjective (map Q g (M.le_comap_map (f := MonoidHomClass.toMonoidHom g)) : S → Q) := + (toLocalizationMap M S).map_surjective_of_surjective h + (toLocalizationMap (M.map (MonoidHomClass.toMonoidHom g)) Q) end @@ -731,7 +736,7 @@ variable (M) theorem isLocalization_of_base_ringEquiv [IsLocalization M S] (h : R ≃+* P) : haveI := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra - IsLocalization (M.map h) S := by + IsLocalization (M.map (MonoidHomClass.toMonoidHom h)) S := by let : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra constructor; constructor · rintro ⟨_, ⟨y, hy, rfl⟩⟩ @@ -742,7 +747,7 @@ theorem isLocalization_of_base_ringEquiv [IsLocalization M S] (h : R ≃+* P) : obtain ⟨⟨x, s⟩, e⟩ := IsLocalization.surj M y refine ⟨⟨h x, _, _, s.prop, rfl⟩, ?_⟩ dsimp only [RingHom.algebraMap_toAlgebra, RingHom.comp_apply] at e ⊢ - convert! e <;> exact h.symm_apply_apply _ + convert e <;> exact h.symm_apply_apply _ · intro x y rw [RingHom.algebraMap_toAlgebra, RingHom.comp_apply, RingHom.comp_apply, IsLocalization.eq_iff_exists M S] @@ -751,14 +756,12 @@ theorem isLocalization_of_base_ringEquiv [IsLocalization M S] (h : R ≃+* P) : theorem isLocalization_iff_of_base_ringEquiv (h : R ≃+* P) : IsLocalization M S ↔ haveI := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra - IsLocalization (M.map h) S := by + IsLocalization (M.map (MonoidHomClass.toMonoidHom h)) S := by let : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra refine ⟨fun _ => isLocalization_of_base_ringEquiv M S h, ?_⟩ - intro (H : IsLocalization (Submonoid.map (h : R ≃* P) M) S) - convert! isLocalization_of_base_ringEquiv (Submonoid.map (h : R ≃* P) M) S h.symm - · rw [← Submonoid.map_coe_toMulEquiv, RingEquiv.coe_toMulEquiv_symm, ← - Submonoid.comap_equiv_eq_map_symm, Submonoid.comap_map_eq_of_injective] - exact h.toEquiv.injective + intro (H : IsLocalization (M.map (MonoidHomClass.toMonoidHom h)) S) + convert isLocalization_of_base_ringEquiv (M.map (MonoidHomClass.toMonoidHom h)) S h.symm + · convert Submonoid.map_id M <;> ext <;> simp rw [RingHom.algebraMap_toAlgebra, RingHom.comp_assoc] simp only [RingHom.comp_id, RingEquiv.symm_symm, RingEquiv.symm_toRingHom_comp_toRingHom] apply Algebra.algebra_ext @@ -767,7 +770,8 @@ theorem isLocalization_iff_of_base_ringEquiv (h : R ≃+* P) : theorem of_ringEquiv_left {S : Type*} [CommSemiring S] {K : Type*} [CommSemiring K] [Algebra R K] (e : R ≃+* S) [Algebra S K] {M₁ : Submonoid S} {M₂ : Submonoid R} - (hM : M₂.map e = M₁) (h : ∀ x, algebraMap R K x = algebraMap S K (e x)) [IsLocalization M₁ K] : + (hM : M₂.map (MonoidHomClass.toMonoidHom e) = M₁) + (h : ∀ x, algebraMap R K x = algebraMap S K (e x)) [IsLocalization M₁ K] : IsLocalization M₂ K := by rw [IsLocalization.isLocalization_iff_of_base_ringEquiv _ _ e, hM] convert! (inferInstance : IsLocalization M₁ K) diff --git a/Mathlib/RingTheory/Localization/Finiteness.lean b/Mathlib/RingTheory/Localization/Finiteness.lean index c8a5894b575792..ebf3c6f397730a 100644 --- a/Mathlib/RingTheory/Localization/Finiteness.lean +++ b/Mathlib/RingTheory/Localization/Finiteness.lean @@ -53,16 +53,15 @@ then there exists some `m : M` such that `m • x` falls in the span of `IsLocalization.finsetIntegerMultiple _ s` over `R`. -/ theorem IsLocalization.smul_mem_finsetIntegerMultiple_span [Algebra R S] [Algebra R S'] - [IsScalarTower R S S'] [IsLocalization (M.map (algebraMap R S)) S'] (x : S) (s : Finset S') - (hx : algebraMap S S' x ∈ Submodule.span R (s : Set S')) : - ∃ m : M, m • x ∈ - Submodule.span R - (IsLocalization.finsetIntegerMultiple (M.map (algebraMap R S)) s : Set S) := by + [IsScalarTower R S S'] [IsLocalization (M.map (algebraMap R S).toMonoidHom) S'] (x : S) + (s : Finset S') (hx : algebraMap S S' x ∈ Submodule.span R (s : Set S')) : + ∃ m : M, m • x ∈ Submodule.span R + (IsLocalization.finsetIntegerMultiple (M.map (algebraMap R S).toMonoidHom) s : Set S) := by let g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') fun c x => by simp [Algebra.algebraMap_eq_smul_one] have g_apply : ∀ x, g x = algebraMap S S' x := fun _ => rfl -- We first obtain the `y' ∈ M` such that `s' = y' • s` is falls in the image of `S` in `S'`. - let y := IsLocalization.commonDenomOfFinset (M.map (algebraMap R S)) s + let y := IsLocalization.commonDenomOfFinset (M.map (algebraMap R S).toMonoidHom) s have hx₁ : (y : S) • (s : Set S') = g '' _ := (IsLocalization.finsetIntegerMultiple_image _ s).symm obtain ⟨y', hy', e : algebraMap R S y' = y⟩ := y.prop @@ -79,11 +78,11 @@ theorem IsLocalization.smul_mem_finsetIntegerMultiple_span [Algebra R S] [Algebr -- Thus `a • (y' • x) = a • x' ∈ span s'` in `S` for some `a ∈ M`. obtain ⟨x', hx', hx'' : algebraMap _ _ _ = _⟩ := hx obtain ⟨⟨_, a, ha₁, rfl⟩, ha₂⟩ := - (IsLocalization.eq_iff_exists (M.map (algebraMap R S)) S').mp hx'' + (IsLocalization.eq_iff_exists (M.map (algebraMap R S).toMonoidHom) S').mp hx'' use (⟨a, ha₁⟩ : M) * (⟨y', hy'⟩ : M) convert! (Submodule.span R - (IsLocalization.finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s : + (IsLocalization.finsetIntegerMultiple (M.map (algebraMap R S).toMonoidHom) s : Set S)).smul_mem a hx' using 1 convert! ha₂.symm using 1 @@ -332,5 +331,6 @@ lemma RingHom.ker_fg_of_localizationSpan (t : Set R) (ht : Ideal.span t = ⊤) (RingHom.ker f).FG := by apply Ideal.fg_of_localizationSpan t ht intro g - rw [← IsLocalization.ker_map (Localization.Away (f g.val)) f (Submonoid.map_powers f g.val)] + rw [← IsLocalization.ker_map (Localization.Away (f g.val)) f + (Submonoid.map_powers f.toMonoidHom g.val)] exact H g diff --git a/Mathlib/RingTheory/Localization/FractionRing.lean b/Mathlib/RingTheory/Localization/FractionRing.lean index 915d9cf3c6c250..1e20d1e321d7bb 100644 --- a/Mathlib/RingTheory/Localization/FractionRing.lean +++ b/Mathlib/RingTheory/Localization/FractionRing.lean @@ -122,7 +122,8 @@ section CommSemiring theorem of_ringEquiv_left {R : Type*} [CommSemiring R] {S : Type*} [CommSemiring S] {K : Type*} [CommSemiring K] [Algebra R K] (e : R ≃+* S) [Algebra S K] (h : ∀ x, algebraMap R K x = algebraMap S K (e x)) [IsFractionRing S K] : - IsFractionRing R K := IsLocalization.of_ringEquiv_left e (MulEquivClass.map_nonZeroDivisors e) h + IsFractionRing R K := + IsLocalization.of_ringEquiv_left e (MulEquivClass.map_nonZeroDivisors e.toMulEquiv) h end CommSemiring @@ -434,7 +435,7 @@ variable {A K B L : Type*} [CommRing A] [CommRing B] [CommRing K] [CommRing L] fraction rings `K ≃+* L`. -/ @[simps! apply] noncomputable def ringEquivOfRingEquiv : K ≃+* L := - IsLocalization.ringEquivOfRingEquiv K L h (MulEquivClass.map_nonZeroDivisors h) + IsLocalization.ringEquivOfRingEquiv K L h (MulEquivClass.map_nonZeroDivisors h.toMulEquiv) lemma ringEquivOfRingEquiv_algebraMap (a : A) : ringEquivOfRingEquiv h (algebraMap A K a) = algebraMap B L (h a) := by @@ -533,7 +534,7 @@ variable {R A K B L : Type*} [CommSemiring R] [CommRing A] [CommRing B] [CommRin `f : A →ₐ[R] K, g : B →ₐ[R] L`, an isomorphism `h : A ≃ₐ[R] B` induces an isomorphism of fraction rings `K ≃ₐ[R] L`. -/ noncomputable def algEquivOfAlgEquiv : K ≃ₐ[R] L := - IsLocalization.algEquivOfAlgEquiv K L h (MulEquivClass.map_nonZeroDivisors h) + IsLocalization.algEquivOfAlgEquiv K L h (MulEquivClass.map_nonZeroDivisors h.toMulEquiv) set_option backward.isDefEq.respectTransparency false in @[simp] @@ -633,7 +634,7 @@ theorem isFractionRing_iff_of_base_ringEquiv (h : R ≃+* P) : @IsFractionRing P _ S _ ((algebraMap R S).comp h.symm.toRingHom).toAlgebra := by delta IsFractionRing convert! isLocalization_iff_of_base_ringEquiv (nonZeroDivisors R) S h - exact (MulEquivClass.map_nonZeroDivisors h).symm + exact (MulEquivClass.map_nonZeroDivisors h.toMulEquiv).symm variable (R S : Type*) [CommSemiring R] [CommSemiring S] [Algebra R S] [h : IsFractionRing R S] diff --git a/Mathlib/RingTheory/Localization/Ideal.lean b/Mathlib/RingTheory/Localization/Ideal.lean index 7074c615cbcdc6..d5dc869714a7d9 100644 --- a/Mathlib/RingTheory/Localization/Ideal.lean +++ b/Mathlib/RingTheory/Localization/Ideal.lean @@ -371,23 +371,26 @@ lemma _root_.Module.IsTorsionFree.of_isLocalization [IsDomain R] [IsDomain S] {R simp only [IsLocalization.map_mk', IsLocalization.mk'_eq_zero_iff, Subtype.exists, exists_prop, this] at hx ⊢ obtain ⟨_, ⟨a, ha, rfl⟩, H⟩ := hx - simp only [← map_mul, + simp only [MonoidHom.coe_coe, ← map_mul, (injective_iff_map_eq_zero' _).mp (FaithfulSMul.algebraMap_injective R S)] at H exact ⟨a, ha, H⟩ lemma of_surjective {R' S' : Type*} [CommRing R'] [CommRing S'] [Algebra R' S'] (f : R →+* R') (hf : Function.Surjective f) (g : S →+* S') (hg : Function.Surjective g) (H : g.comp (algebraMap R S) = (algebraMap _ _).comp f) - (H' : RingHom.ker g ≤ (RingHom.ker f).map (algebraMap R S)) : IsLocalization (M.map f) S' where + (H' : RingHom.ker g ≤ (RingHom.ker f).map (algebraMap R S)) : + IsLocalization (M.map f.toMonoidHom) S' where map_units := by rintro ⟨_, y, hy, rfl⟩ - simpa only [← RingHom.comp_apply, H] using (IsLocalization.map_units S ⟨y, hy⟩).map g + simpa only [RingHom.toMonoidHom_eq_coe, MonoidHom.coe_coe, ← RingHom.comp_apply, ← H] + using (IsLocalization.map_units S ⟨y, hy⟩).map g surj := by intro z obtain ⟨z, rfl⟩ := hg z obtain ⟨⟨r, s⟩, e⟩ := IsLocalization.surj M z refine ⟨⟨f r, _, s.1, s.2, rfl⟩, ?_⟩ - simpa only [map_mul, ← RingHom.comp_apply, H] using DFunLike.congr_arg g e + simpa only [RingHom.toMonoidHom_eq_coe, MonoidHom.coe_coe, map_mul, ← RingHom.comp_apply, H] + using DFunLike.congr_arg g e exists_of_eq := by intro x y e obtain ⟨x, rfl⟩ := hf x diff --git a/Mathlib/RingTheory/Localization/Integral.lean b/Mathlib/RingTheory/Localization/Integral.lean index fd3fd64f39b0a9..e197ba699b5f6f 100644 --- a/Mathlib/RingTheory/Localization/Integral.lean +++ b/Mathlib/RingTheory/Localization/Integral.lean @@ -40,8 +40,9 @@ set_option backward.isDefEq.respectTransparency.types false in attribute [local instance] Polynomial.algebra Polynomial.isLocalization in private theorem exists_integer_polynomial_multiple_and_support_subset (p : S[X]) : ∃ b ∈ M, ∃ (q : R[X]), q.map (algebraMap R S) = b • p ∧ q.support ⊆ p.support := by - obtain ⟨⟨_, b, hb, rfl⟩, h⟩ := exists_integer_multiple (Submonoid.map C M) p - rw [Subtype.coe_mk, C_eq_algebraMap, algebraMap_smul] at h + obtain ⟨⟨_, b, hb, rfl⟩, h⟩ := exists_integer_multiple (Submonoid.map C.toMonoidHom M) p + simp only [RingHom.toMonoidHom_eq_coe, MonoidHom.coe_coe, C_eq_algebraMap, algebraMap_eq, + algebraMap_smul] at h obtain ⟨q', h₁, h₂⟩ := exists_support_eq_of_mem_lifts h exact ⟨b, hb, q', h₁, h₂ ▸ support_smul b p⟩ @@ -164,7 +165,7 @@ theorem is_integral_localization_at_leadingCoeff {x : S} (p : R[X]) (hp : aeval (show _ ≤ (Algebra.algebraMapSubmonoid S M).comap _ from M.le_comap_map) : Rₘ →+* _).IsIntegralElem (algebraMap S Sₘ x) := - haveI : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ := + haveI : IsLocalization (Submonoid.map (MonoidHomClass.toMonoidHom (algebraMap R S)) M) Sₘ := inferInstanceAs (IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ) (algebraMap R S).isIntegralElem_localization_at_leadingCoeff x p hp M hM @@ -423,16 +424,17 @@ protected lemma IsLocalization.integralClosure simp [← IsScalarTower.algebraMap_apply] · rintro ⟨s, hs⟩ obtain ⟨⟨x, _, m₁, hm₁, rfl⟩, e⟩ := IsLocalization.surj (Algebra.algebraMapSubmonoid S M) s - simp only [← IsScalarTower.algebraMap_apply] at e + -- used to fire: simp only [← IsScalarTower.algebraMap_apply] at e obtain ⟨⟨m₂, hm₂⟩, hm₂s⟩ := IsIntegral.exists_multiple_integral_of_isLocalization M _ hs simp only [Submonoid.smul_def, Algebra.smul_def] at hm₂s obtain ⟨m₃, hm₃, hm₃s⟩ := IsLocalization.exists_isIntegral_smul_of_isIntegral_map (Sₘ := Sf) M (x := m₂ • x) <| by - simp only [Algebra.smul_def, map_mul, ← IsScalarTower.algebraMap_apply, ← e, ← mul_assoc] + simp only [Algebra.smul_def, map_mul, ← IsScalarTower.algebraMap_apply, ← e, + MonoidHom.coe_coe, ← mul_assoc] exact hm₂s.mul (.algebraMap (Algebra.IsIntegral.isIntegral _)) refine ⟨⟨⟨_, hm₃s⟩, _, _, mul_mem hm₁ (mul_mem hm₂ hm₃), rfl⟩, ?_⟩ · apply (FaithfulSMul.algebraMap_injective (integralClosure Rf Sf) Sf) - simp [← IsScalarTower.algebraMap_apply, e, ← mul_assoc, Algebra.smul_def] + simp [← IsScalarTower.algebraMap_apply, ← e, ← mul_assoc, Algebra.smul_def] ring · rintro ⟨a, ha⟩ ⟨b, hb⟩ e have := congr(algebraMap _ Sf $e) diff --git a/Mathlib/RingTheory/Localization/InvSubmonoid.lean b/Mathlib/RingTheory/Localization/InvSubmonoid.lean index c4ec3d6c2dd7de..9fb991a8f909e1 100644 --- a/Mathlib/RingTheory/Localization/InvSubmonoid.lean +++ b/Mathlib/RingTheory/Localization/InvSubmonoid.lean @@ -49,15 +49,15 @@ theorem submonoid_map_le_is_unit : M.map (algebraMap R S) ≤ IsUnit.submonoid S exact IsLocalization.map_units S ⟨_, ha⟩ /-- There is an equivalence of monoids between the image of `M` and `invSubmonoid`. -/ -noncomputable abbrev equivInvSubmonoid : M.map (algebraMap R S) ≃* invSubmonoid M S := - ((M.map (algebraMap R S)).leftInvEquiv (submonoid_map_le_is_unit M S)).symm +noncomputable abbrev equivInvSubmonoid : M.map (algebraMap R S).toMonoidHom ≃* invSubmonoid M S := + ((M.map (algebraMap R S).toMonoidHom).leftInvEquiv (submonoid_map_le_is_unit M S)).symm /-- There is a canonical map from `M` to `invSubmonoid` sending `x` to `1 / x`. -/ noncomputable def toInvSubmonoid : M →* invSubmonoid M S := (equivInvSubmonoid M S).toMonoidHom.comp ((algebraMap R S : R →* S).submonoidMap M) theorem toInvSubmonoid_surjective : Function.Surjective (toInvSubmonoid M S) := - Function.Surjective.comp (β := M.map (algebraMap R S)) + Function.Surjective.comp (β := M.map (algebraMap R S).toMonoidHom) (Equiv.surjective (equivInvSubmonoid _ _).toEquiv) (MonoidHom.submonoidMap_surjective _ _) @[simp] diff --git a/Mathlib/RingTheory/Localization/LocalizationLocalization.lean b/Mathlib/RingTheory/Localization/LocalizationLocalization.lean index adfd07f78650dd..41fa07624cb8b2 100644 --- a/Mathlib/RingTheory/Localization/LocalizationLocalization.lean +++ b/Mathlib/RingTheory/Localization/LocalizationLocalization.lean @@ -119,7 +119,7 @@ include M in localization is a localization. -/ theorem localization_localization_isLocalization_of_has_all_units [IsLocalization N T] - (H : ∀ x : S, IsUnit x → x ∈ N) : IsLocalization (N.comap (algebraMap R S)) T := by + (H : ∀ x : S, IsUnit x → x ∈ N) : IsLocalization (N.comap (algebraMap R S).toMonoidHom) T := by convert! localization_localization_isLocalization M N T using 1 dsimp [localizationLocalizationSubmodule] congr @@ -193,7 +193,7 @@ instance {R : Type*} [CommRing R] [IsDomain R] (p : Ideal R) [p.IsPrime] : /-- If `M ≤ N` are submonoids of `R`, then `N⁻¹S` is also the localization of `M⁻¹S` at `N`. -/ theorem isLocalization_of_submonoid_le (M N : Submonoid R) (h : M ≤ N) [IsLocalization M S] [IsLocalization N T] [Algebra S T] [IsScalarTower R S T] : - IsLocalization (N.map (algebraMap R S)) T where + IsLocalization (N.map (algebraMap R S).toMonoidHom) T where map_units := by rintro ⟨_, ⟨y, hy, rfl⟩⟩ convert! IsLocalization.map_units T ⟨y, hy⟩ diff --git a/Mathlib/RingTheory/Localization/Pi.lean b/Mathlib/RingTheory/Localization/Pi.lean index c5c6260446a323..729515e57238f2 100644 --- a/Mathlib/RingTheory/Localization/Pi.lean +++ b/Mathlib/RingTheory/Localization/Pi.lean @@ -53,7 +53,8 @@ instance (M : Π i, Submonoid (R i)) [∀ i, IsLocalization (M i) (S i)] : variable (S' : Type*) [CommSemiring S'] [Algebra (Π i, R i) S'] (M : Submonoid (Π i, R i)) theorem iff_map_piEvalRingHom [Finite ι] : - IsLocalization M S' ↔ IsLocalization (.pi .univ fun i ↦ M.map (Pi.evalRingHom R i)) S' := + IsLocalization M S' ↔ IsLocalization (.pi .univ fun i ↦ + M.map (MonoidHomClass.toMonoidHom (Pi.evalRingHom R i))) S' := iff_of_le_of_exists_dvd M _ (fun m hm i _ ↦ ⟨m, hm, rfl⟩) fun n hn ↦ by choose m mem eq using hn have := Fintype.ofFinite ι @@ -61,7 +62,7 @@ theorem iff_map_piEvalRingHom [Finite ι] : rw [Fintype.prod_apply] exact (eq i ⟨⟩).symm.dvd.trans (Finset.dvd_prod_of_mem _ <| Finset.mem_univ _) -variable [∀ i, IsLocalization (M.map (Pi.evalRingHom R i)) (S i)] +variable [∀ i, IsLocalization (M.map (MonoidHomClass.toMonoidHom (Pi.evalRingHom R i))) (S i)] /-- Let `M` be a submonoid of a direct product of commutative rings `R i`, and let `M' i` denote the projection of `M` onto each corresponding factor. Given a ring homomorphism from the direct @@ -69,7 +70,8 @@ product `Π i, R i` to the product of the localizations of each `R i` at `M' i`, maps to a unit under this homomorphism. -/ lemma isUnit_piRingHom_algebraMap_comp_piEvalRingHom (y : M) : IsUnit ((RingHom.pi fun i ↦ (algebraMap (R i) (S i)).comp (Pi.evalRingHom R i)) y) := - Pi.isUnit_iff.mpr fun i ↦ map_units _ (⟨y.1 i, y, y.2, rfl⟩ : M.map (Pi.evalRingHom R i)) + Pi.isUnit_iff.mpr fun i ↦ map_units _ + (⟨y.1 i, y, y.2, rfl⟩ : M.map (MonoidHomClass.toMonoidHom (Pi.evalRingHom R i))) /-- Let `M` be a submonoid of a direct product of commutative rings `R i`, and let `M' i` denote the projection of `M` onto each factor. Then the canonical map from the localization of the direct @@ -89,7 +91,7 @@ lemma surjective_piRingHom_algebraMap_comp_piEvalRingHom [∀ i, Ring.KrullDimLE 0 (R i)] [∀ i, IsLocalRing (R i)] : Surjective (RingHom.pi (fun i ↦ (algebraMap (R i) (S i)).comp (Pi.evalRingHom R i))) := by apply Surjective.piMap (fun i ↦ ?_) - by_cases h₀ : (0 : R i) ∈ (M.map (Pi.evalRingHom R i)) + by_cases h₀ : (0 : R i) ∈ (M.map (MonoidHomClass.toMonoidHom (Pi.evalRingHom R i))) · have := uniqueOfZeroMem h₀ (S := (S i)) exact surjective_to_subsingleton (algebraMap (R i) (S i)) · exact (IsLocalization.atUnits _ _ (by simpa)).surjective @@ -102,7 +104,7 @@ lemma algebraMap_pi_surjective_of_isLocalization [∀ i, Ring.KrullDimLE 0 (R i) [∀ i, IsLocalRing (R i)] [IsLocalization M S'] [Finite ι] : Surjective (algebraMap (Π i, R i) S') := by intro s - set S := fun (i : ι) => Localization (M.map (Pi.evalRingHom R i)) + set S := fun (i : ι) => Localization (M.map (MonoidHomClass.toMonoidHom (Pi.evalRingHom R i))) obtain ⟨r, hr⟩ := surjective_piRingHom_algebraMap_comp_piEvalRingHom S M ((lift (isUnit_piRingHom_algebraMap_comp_piEvalRingHom R S M)) s) diff --git a/Mathlib/RingTheory/MvPolynomial/Localization.lean b/Mathlib/RingTheory/MvPolynomial/Localization.lean index 2cfb986b34adc7..20b478aa9624cb 100644 --- a/Mathlib/RingTheory/MvPolynomial/Localization.lean +++ b/Mathlib/RingTheory/MvPolynomial/Localization.lean @@ -41,13 +41,13 @@ If `S` is the localization of `R` at a submonoid `M`, then `MvPolynomial σ S` is the localization of `MvPolynomial σ R` at `M.map MvPolynomial.C`. See also `Polynomial.isLocalization` for the univariate case. -/ -instance isLocalization : IsLocalization (M.map <| C (σ := σ)) (MvPolynomial σ S) := +instance isLocalization : IsLocalization (M.map (C (σ := σ)).toMonoidHom) (MvPolynomial σ S) := isLocalizedModule_iff_isLocalization.mp <| (isLocalizedModule_iff_isBaseChange M S _).mpr <| .of_equiv (algebraTensorAlgEquiv _ _).toLinearEquiv fun _ ↦ by simp lemma isLocalization_C_mk' (a : R) (m : M) : C (IsLocalization.mk' S a m) = IsLocalization.mk' (MvPolynomial σ S) (C (σ := σ) a) - ⟨C m, Submonoid.mem_map_of_mem C m.property⟩ := by + ⟨C m, Submonoid.mem_map_of_mem C.toMonoidHom m.property⟩ := by simp_rw [IsLocalization.eq_mk'_iff_mul_eq, algebraMap_def, map_C, ← map_mul, IsLocalization.mk'_spec] diff --git a/Mathlib/RingTheory/OrderOfVanishing/Noetherian.lean b/Mathlib/RingTheory/OrderOfVanishing/Noetherian.lean index 341293419432f4..7d368a187f3659 100644 --- a/Mathlib/RingTheory/OrderOfVanishing/Noetherian.lean +++ b/Mathlib/RingTheory/OrderOfVanishing/Noetherian.lean @@ -197,7 +197,7 @@ lemma isUnit_iff_ordFrac_one_of_isDiscreteValuationRing {x : R} : simp [ordFrac_eq_valuation_inv, IsDiscreteValuationRing.maximalIdeal] lemma mker_ordFrac_eq_isUnitSubmonoid : - MonoidHom.mker (ordFrac R) = (IsUnit.submonoid R).map (algebraMap R K) := by + (ordFrac R).toMonoidHom.mker = (IsUnit.submonoid R).map (algebraMap R K).toMonoidHom := by rw [ordFrac_eq_inverse_comp_valuation, ← MonoidWithZeroHom.comap_mker, MonoidWithZeroHom.mker_inverse] exact IsDiscreteValuationRing.mker_valuation_eq_isUnitSubmonoid diff --git a/Mathlib/RingTheory/QuasiFinite/Basic.lean b/Mathlib/RingTheory/QuasiFinite/Basic.lean index 05073ce268ad00..50581656b4824f 100644 --- a/Mathlib/RingTheory/QuasiFinite/Basic.lean +++ b/Mathlib/RingTheory/QuasiFinite/Basic.lean @@ -270,13 +270,14 @@ omit [Algebra S T] in lemma of_forall_exists_mul_mem_range [QuasiFinite R S] (f : S →ₐ[R] T) (H : ∀ x : T, ∃ s : S, IsUnit (f s) ∧ x * f s ∈ f.range) : QuasiFinite R T := by - let φ : Localization ((IsUnit.submonoid T).comap f) →ₐ[R] T := - IsLocalization.liftAlgHom (M := (IsUnit.submonoid T).comap f) (f := f) - (by simp [IsUnit.mem_submonoid_iff]) + let φ : Localization ((IsUnit.submonoid T).comap (MonoidHomClass.toMonoidHom f)) →ₐ[R] T := + IsLocalization.liftAlgHom (M := (IsUnit.submonoid T).comap (MonoidHomClass.toMonoidHom f)) + (f := f) (by simp [IsUnit.mem_submonoid_iff]) suffices Function.Surjective φ from .of_surjective_algHom φ this intro x obtain ⟨s, hs, t, ht⟩ := H x - refine ⟨IsLocalization.mk' (M := (IsUnit.submonoid T).comap f) _ t ⟨s, hs⟩, ?_⟩ + refine ⟨IsLocalization.mk' (M := (IsUnit.submonoid T).comap (MonoidHomClass.toMonoidHom f)) _ t + ⟨s, hs⟩, ?_⟩ simpa [φ, IsLocalization.lift_mk', Units.mul_inv_eq_iff_eq_mul, IsUnit.coe_liftRight] omit [Algebra S T] in diff --git a/Mathlib/RingTheory/RingHom/Finite.lean b/Mathlib/RingTheory/RingHom/Finite.lean index d1cb1140d4587e..4d90f2ce1e3ea8 100644 --- a/Mathlib/RingTheory/RingHom/Finite.lean +++ b/Mathlib/RingTheory/RingHom/Finite.lean @@ -90,12 +90,12 @@ theorem RingHom.finite_ofLocalizationSpan : RingHom.OfLocalizationSpan @RingHom. -- We first setup the instances let := f.toAlgebra let := fun r : s => (Localization.awayMap f r).toAlgebra - have (r : s) : IsLocalization ((Submonoid.powers (r : R)).map (algebraMap R S)) + have (r : s) : IsLocalization ((Submonoid.powers (r : R)).map (algebraMap R S).toMonoidHom) (Localization.Away (f r)) := by rw [Submonoid.map_powers]; exact Localization.isLocalization have : ∀ r : s, IsScalarTower R (Localization.Away (r : R)) (Localization.Away (f r)) := fun r => IsScalarTower.of_algebraMap_eq' - (IsLocalization.map_comp (Submonoid.powers (r : R)).le_comap_map).symm + (IsLocalization.map_comp ((Submonoid.powers (r : R)).le_comap_map (f := f.toMonoidHom))).symm -- By the hypothesis, we may find a finite generating set for each `Sᵣ`. This set can then be -- lifted into `R` by multiplying a sufficiently large power of `r`. I claim that the union of -- these generates `S`. diff --git a/Mathlib/RingTheory/RingHom/Locally.lean b/Mathlib/RingTheory/RingHom/Locally.lean index f85c8a54f243bc..c34a1d32c43e1d 100644 --- a/Mathlib/RingTheory/RingHom/Locally.lean +++ b/Mathlib/RingTheory/RingHom/Locally.lean @@ -183,8 +183,11 @@ lemma locally_respectsIso (hPi : RespectsIso P) : RespectsIso (Locally P) where refine ⟨e '' s, ?_, ?_⟩ · rw [← Ideal.map_span, hsone, Ideal.map_top] · rintro - ⟨a, ha, rfl⟩ + have : IsLocalization (Submonoid.powers (e.toMonoidHom a)) (Localization.Away (e a)) := + inferInstanceAs <| IsLocalization (Submonoid.powers (e a)) (Localization.Away (e a)) + -- synthesis works on `master`, TODO! let e' : Localization.Away a ≃+* Localization.Away (e a) := - IsLocalization.ringEquivOfRingEquiv _ _ e (Submonoid.map_powers e a) + IsLocalization.ringEquivOfRingEquiv _ _ e (Submonoid.map_powers e.toMonoidHom a) have : (algebraMap T (Localization.Away (e a))).comp e.toRingHom = e'.toRingHom.comp (algebraMap S (Localization.Away a)) := by ext x @@ -243,7 +246,7 @@ lemma locally_stableUnderComposition (hPi : RespectsIso P) (hPl : LocalizationPr simp only [this, a'] apply hPc _ _ (hsf a.val a.property) apply @hPl _ _ _ _ g' _ _ _ _ _ _ _ _ ?_ (hsg b.val b.property) - exact IsLocalization.Away.instMapRingHomPowersOfCoe (Localization.Away (g' a.val)) a.val + exact IsLocalization.Away.map_toMonoidHom_powers (Localization.Away (g' a.val)) a.val /-- If `P` is stable under composition with localization away maps on the right, then so is `Locally P`. -/ @@ -309,7 +312,7 @@ lemma locally_localizationAwayPreserves (hPl : LocalizationAwayPreserves P) : IsLocalization.Away (((algebraMap S (Localization.Away a.val)).comp f) r) (Sₐ a) := inferInstanceAs (IsLocalization.Away (rₐ a) (Sₐ a)) have (a : s) : IsLocalization (Algebra.algebraMapSubmonoid (Localization.Away a.val) - (Submonoid.map f (Submonoid.powers r))) (Sₐ a) := by + (Submonoid.map (MonoidHomClass.toMonoidHom f) (Submonoid.powers r))) (Sₐ a) := by convert! (inferInstance : IsLocalization.Away (rₐ a) (Sₐ a)) simp [rₐ, Algebra.algebraMapSubmonoid] have H (a : s) : Submonoid.powers (f r) ≤ @@ -322,9 +325,9 @@ lemma locally_localizationAwayPreserves (hPl : LocalizationAwayPreserves P) : refine ⟨s, fun a ↦ algebraMap S S' a.val, ?_, Sₐ, inferInstance, inferInstance, fun a ↦ ?_, fun a ↦ ?_⟩ · rw [← Set.image_eq_range, ← Ideal.map_span, hsone, Ideal.map_top] - · convert! - IsLocalization.commutes (T := Sₐ a) (M₁ := (Submonoid.powers r).map f) (S₁ := S') (S₂ := - Localization.Away a.val) (M₂ := Submonoid.powers a.val) + · convert! IsLocalization.commutes (T := Sₐ a) (M₁ := (Submonoid.powers r).map + (MonoidHomClass.toMonoidHom f)) (S₁ := S') + (S₂ := Localization.Away a.val) (M₂ := Submonoid.powers a.val) simp [Algebra.algebraMapSubmonoid] · rw [algebraMap_toAlgebra, IsLocalization.Away.map, IsLocalization.map_comp_map] exact hPl ((algebraMap _ (Localization.Away a.val)).comp f) r R' (Sₐ a) (hs _ a.2) @@ -336,22 +339,26 @@ lemma locally_localizationPreserves (hPl : LocalizationPreserves P) : obtain ⟨s, hsone, hs⟩ := hf rw [locally_iff_exists hPl.away.respectsIso] let Mₐ (a : s) : Submonoid (Localization.Away a.val) := - (M.map f).map (algebraMap S (Localization.Away a.val)) + (M.map f).map (MonoidHomClass.toMonoidHom (algebraMap S (Localization.Away a.val))) let Sₐ (a : s) := Localization (Mₐ a) - have hM (a : s) : M.map ((algebraMap S (Localization.Away a.val)).comp f) = Mₐ a := - (M.map_map _ _).symm - have (a : s) : - IsLocalization (M.map ((algebraMap S (Localization.Away a.val)).comp f)) (Sₐ a) := by + have hM (a : s) : M.map (MonoidHomClass.toMonoidHom + ((algebraMap S (Localization.Away a.val)).comp f)) = Mₐ a := by + symm + exact (M.map_map _ _) + have (a : s) : IsLocalization (M.map (MonoidHomClass.toMonoidHom + ((algebraMap S (Localization.Away a.val)).comp f))) (Sₐ a) := by rw [hM] infer_instance have (a : s) : - IsLocalization (Algebra.algebraMapSubmonoid (Localization.Away a.val) (M.map f)) (Sₐ a) := + IsLocalization (Algebra.algebraMapSubmonoid (Localization.Away a.val) + (M.map (MonoidHomClass.toMonoidHom f))) (Sₐ a) := inferInstanceAs <| IsLocalization (Mₐ a) (Sₐ a) let (a : s) : Algebra S' (Sₐ a) := (IsLocalization.map (Sₐ a) (algebraMap S (Localization.Away a.val)) - (M.map f).le_comap_map).toAlgebra + (M.map (MonoidHomClass.toMonoidHom f)).le_comap_map).toAlgebra have (a : s) : IsScalarTower S S' (Sₐ a) := - IsScalarTower.of_algebraMap_eq' (IsLocalization.map_comp (M.map f).le_comap_map).symm + IsScalarTower.of_algebraMap_eq' (IsLocalization.map_comp (M.map + (MonoidHomClass.toMonoidHom f)).le_comap_map).symm refine ⟨s, fun a ↦ algebraMap S S' a.val, ?_, Sₐ, inferInstance, inferInstance, fun a ↦ ?_, fun a ↦ ?_⟩ · rw [← Set.image_eq_range, ← Ideal.map_span, hsone, Ideal.map_top] diff --git a/Mathlib/RingTheory/RingHom/Surjective.lean b/Mathlib/RingTheory/RingHom/Surjective.lean index dd49cb4106671f..9802641da25ea4 100644 --- a/Mathlib/RingTheory/RingHom/Surjective.lean +++ b/Mathlib/RingTheory/RingHom/Surjective.lean @@ -58,10 +58,11 @@ theorem surjective_isStableUnderBaseChange : IsStableUnderBaseChange surjective theorem surjective_localizationPreserves : LocalizationPreserves surjective := by introv R H x - obtain ⟨x, ⟨_, s, hs, rfl⟩, rfl⟩ := IsLocalization.exists_mk'_eq (M.map f) x + obtain ⟨x, ⟨_, s, hs, rfl⟩, rfl⟩ := + IsLocalization.exists_mk'_eq (M.map (MonoidHomClass.toMonoidHom f)) x obtain ⟨y, rfl⟩ := H x use IsLocalization.mk' R' y ⟨s, hs⟩ - rw [IsLocalization.map_mk'] + simp [IsLocalization.map_mk'] /-- `R →+* S` is surjective if there exists a set `{ r }` that spans `R` such that `Rᵣ →+* Sᵣ` is surjective. -/ @@ -87,7 +88,8 @@ for every prime ideal `P` of `S`. -/ theorem surjective_localRingHom_of_surjective {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) (h : Function.Surjective f) (P : Ideal S) [P.IsPrime] : Function.Surjective (Localization.localRingHom (P.comap f) P f rfl) := - have : IsLocalization (Submonoid.map f (Ideal.comap f P).primeCompl) (Localization.AtPrime P) := + have : IsLocalization (Submonoid.map (MonoidHomClass.toMonoidHom f) (Ideal.comap f P).primeCompl) + (Localization.AtPrime P) := (Submonoid.map_comap_eq_of_surjective h P.primeCompl).symm ▸ Localization.isLocalization surjective_localizationPreserves _ _ _ _ h diff --git a/Mathlib/RingTheory/Smooth/Basic.lean b/Mathlib/RingTheory/Smooth/Basic.lean index f95a1ed39a7b70..e5d7783c6e1d0b 100644 --- a/Mathlib/RingTheory/Smooth/Basic.lean +++ b/Mathlib/RingTheory/Smooth/Basic.lean @@ -476,7 +476,7 @@ variable {R A Rₘ Sₘ : Type*} [CommRing R] [CommRing A] [CommRing Rₘ] [Comm variable (M : Submonoid R) variable [Algebra R A] [Algebra R Sₘ] [Algebra A Sₘ] [Algebra R Rₘ] [Algebra Rₘ Sₘ] variable [IsScalarTower R Rₘ Sₘ] [IsScalarTower R A Sₘ] -variable [IsLocalization M Rₘ] [IsLocalization (M.map (algebraMap R A)) Sₘ] +variable [IsLocalization M Rₘ] [IsLocalization (M.map (algebraMap R A).toMonoidHom) Sₘ] include M theorem of_isLocalization : FormallySmooth R Rₘ := by @@ -520,7 +520,8 @@ theorem localization_base [FormallySmooth R Sₘ] : FormallySmooth Rₘ Sₘ := simp [f] theorem localization_map [FormallySmooth R A] : FormallySmooth Rₘ Sₘ := by - have : FormallySmooth A Sₘ := FormallySmooth.of_isLocalization (M.map (algebraMap R A)) + have : FormallySmooth A Sₘ := + FormallySmooth.of_isLocalization (M.map (algebraMap R A).toMonoidHom) have : FormallySmooth R Sₘ := FormallySmooth.comp R A Sₘ exact FormallySmooth.localization_base M diff --git a/Mathlib/RingTheory/Smooth/Fiber.lean b/Mathlib/RingTheory/Smooth/Fiber.lean index 31ebf51a52f70d..3f9ab1e04ee6b0 100644 --- a/Mathlib/RingTheory/Smooth/Fiber.lean +++ b/Mathlib/RingTheory/Smooth/Fiber.lean @@ -154,7 +154,7 @@ lemma FormallySmooth.of_formallySmooth_residueField_tensor (M : Submonoid P) -/ obtain ⟨n, f₀, hf₀⟩ := Algebra.FiniteType.iff_quotient_mvPolynomial''.mp (inferInstance : Algebra.FiniteType R P) - let M' := M.comap f₀ + let M' := M.comap f₀.toMonoidHom let P' := Localization M' let fP : P' →ₐ[R] S := IsLocalization.liftAlgHom (M := M') (f := (IsScalarTower.toAlgHom R P S).comp f₀) fun x ↦ by diff --git a/Mathlib/RingTheory/Spectrum/Prime/FreeLocus.lean b/Mathlib/RingTheory/Spectrum/Prime/FreeLocus.lean index a52be8b7ec9824..0bb09ebdc667b7 100644 --- a/Mathlib/RingTheory/Spectrum/Prime/FreeLocus.lean +++ b/Mathlib/RingTheory/Spectrum/Prime/FreeLocus.lean @@ -117,7 +117,7 @@ lemma freeLocus_localization (S : Submonoid R) : have : IsLocalization.AtPrime Rₚ p.asIdeal := by have := IsLocalization.isLocalization_of_submonoid_le (Localization S) Rₚ _ _ hp' apply IsLocalization.isLocalization_of_is_exists_mul_mem _ - (Submonoid.map (algebraMap R (Localization S)) p'.primeCompl) + (Submonoid.map (algebraMap R (Localization S)).toMonoidHom p'.primeCompl) · rintro _ ⟨x, hx, rfl⟩; exact hx · rintro ⟨x, hx⟩ obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq S x diff --git a/Mathlib/RingTheory/Unramified/Basic.lean b/Mathlib/RingTheory/Unramified/Basic.lean index f28b28d1e42a3a..7fa20e47d3e7d5 100644 --- a/Mathlib/RingTheory/Unramified/Basic.lean +++ b/Mathlib/RingTheory/Unramified/Basic.lean @@ -294,7 +294,7 @@ variable {R S Rₘ Sₘ : Type*} [CommRing R] [CommRing S] [CommRing Rₘ] [Comm variable (M : Submonoid R) variable [Algebra R S] [Algebra R Sₘ] [Algebra S Sₘ] [Algebra R Rₘ] [Algebra Rₘ Sₘ] variable [IsScalarTower R Rₘ Sₘ] [IsScalarTower R S Sₘ] -variable [IsLocalization (M.map (algebraMap R S)) Sₘ] +variable [IsLocalization (M.map (algebraMap R S).toMonoidHom) Sₘ] include M /-- This holds in general for epimorphisms. -/ @@ -323,7 +323,7 @@ theorem localization_base [FormallyUnramified R Sₘ] : FormallyUnramified Rₘ theorem localization_map [FormallyUnramified R S] : FormallyUnramified Rₘ Sₘ := by have : FormallyUnramified S Sₘ := - FormallyUnramified.of_isLocalization (M.map (algebraMap R S)) + FormallyUnramified.of_isLocalization (M.map (algebraMap R S).toMonoidHom) have : FormallyUnramified R Sₘ := FormallyUnramified.comp R S Sₘ exact FormallyUnramified.localization_base M diff --git a/Mathlib/RingTheory/Valuation/Archimedean.lean b/Mathlib/RingTheory/Valuation/Archimedean.lean index a022faeaed0692..dad2f629dae2bb 100644 --- a/Mathlib/RingTheory/Valuation/Archimedean.lean +++ b/Mathlib/RingTheory/Valuation/Archimedean.lean @@ -21,7 +21,7 @@ variable {F Γ₀ O : Type*} [Field F] [LinearOrderedCommGroupWithZero Γ₀] [CommRing O] [Algebra O F] {v : Valuation F Γ₀} instance MonoidWithZeroHom.instLinearOrderedCommGroupWithZeroMrange (v : F →*₀ Γ₀) : - LinearOrderedCommGroupWithZero (MonoidHom.mrange v) where + LinearOrderedCommGroupWithZero v.toMonoidHom.mrange where bot := ⟨⊥, by simp [bot_eq_zero]⟩ bot_le a := by simp [bot_eq_zero, ← Subtype.coe_le_coe] isBot_zero a := by simp [← Subtype.coe_le_coe] @@ -32,8 +32,8 @@ instance MonoidWithZeroHom.instLinearOrderedCommGroupWithZeroMrange (v : F →* gcongr instance Valuation.instLinearOrderedCommGroupWithZeroMrange : - LinearOrderedCommGroupWithZero (MonoidHom.mrange v) := - inferInstanceAs (LinearOrderedCommGroupWithZero (MonoidHom.mrange (.ofClass v : F →*₀ Γ₀))) + LinearOrderedCommGroupWithZero v.toMonoidHom.mrange := + inferInstanceAs (LinearOrderedCommGroupWithZero v.toMonoidHom.mrange) namespace Valuation.Integers @@ -44,10 +44,10 @@ lemma wfDvdMonoid_iff_wellFounded_gt_on_v (hv : Integers v O) : simp [Function.onFun, hv.dvdNotUnit_iff_lt] open scoped Function WithZero in -lemma wellFounded_gt_on_v_iff_discrete_mrange [Nontrivial (MonoidHom.mrange v)ˣ] +lemma wellFounded_gt_on_v_iff_discrete_mrange [Nontrivial (v.toMonoidHom.mrange)ˣ] (hv : Integers v O) : WellFounded ((· > ·) on (v ∘ algebraMap O F)) ↔ - Nonempty (MonoidHom.mrange v ≃*o ℤᵐ⁰) := by + Nonempty (v.toMonoidHom.mrange ≃*o ℤᵐ⁰) := by rw [← LinearOrderedCommGroupWithZero.wellFoundedOn_setOfPred_ge_gt_iff_nonempty_discrete_of_ne_zero one_ne_zero, ← Set.wellFoundedOn_range] @@ -59,7 +59,7 @@ lemma wellFounded_gt_on_v_iff_discrete_mrange [Nontrivial (MonoidHom.mrange v)ˣ intro hx obtain ⟨y, rfl⟩ := hv.exists_of_le_one hx exact ⟨y, by simp⟩ - · exact fun x ↦ if hx : x ∈ MonoidHom.mrange v then ⟨x, hx⟩ else 1 + · exact fun x ↦ if hx : x ∈ v.toMonoidHom.mrange then ⟨x, hx⟩ else 1 · intro simp only [Set.mem_range, Function.comp_apply, MonoidHom.mem_mrange, Set.mem_ofPred_eq, forall_exists_index] @@ -67,11 +67,11 @@ lemma wellFounded_gt_on_v_iff_discrete_mrange [Nontrivial (MonoidHom.mrange v)ˣ simp [← Subtype.coe_le_coe, hv.map_le_one] · simp [Function.onFun] -lemma isPrincipalIdealRing_iff_not_denselyOrdered [MulArchimedean (MonoidHom.mrange v)] +lemma isPrincipalIdealRing_iff_not_denselyOrdered [MulArchimedean v.toMonoidHom.mrange] (hv : Integers v O) : IsPrincipalIdealRing O ↔ ¬ DenselyOrdered (Set.range v) := by refine ⟨fun _ ↦ not_denselyOrdered_of_isPrincipalIdealRing hv, fun H ↦ ?_⟩ - rcases subsingleton_or_nontrivial (MonoidHom.mrange v)ˣ with hs | _ + rcases subsingleton_or_nontrivial (v.toMonoidHom.mrange)ˣ with hs | _ · have := bijective_algebraMap_of_subsingleton_units_mrange hv exact .of_surjective _ (RingEquiv.ofBijective _ this).symm.surjective have : IsDomain O := hv.hom_inj.isDomain @@ -81,9 +81,9 @@ lemma isPrincipalIdealRing_iff_not_denselyOrdered [MulArchimedean (MonoidHom.mra LinearOrderedCommGroupWithZero.discrete_iff_not_denselyOrdered] exact H -lemma isPrincipalIdealRing_iff_not_denselyOrdered_mrange [MulArchimedean (MonoidHom.mrange v)] +lemma isPrincipalIdealRing_iff_not_denselyOrdered_mrange [MulArchimedean v.toMonoidHom.mrange] (hv : Integers v O) : - IsPrincipalIdealRing O ↔ ¬ DenselyOrdered (MonoidHom.mrange v) := + IsPrincipalIdealRing O ↔ ¬ DenselyOrdered v.toMonoidHom.mrange := isPrincipalIdealRing_iff_not_denselyOrdered hv end Valuation.Integers diff --git a/Mathlib/RingTheory/Valuation/Basic.lean b/Mathlib/RingTheory/Valuation/Basic.lean index ed8b787f132fa3..4efffa05d360bc 100644 --- a/Mathlib/RingTheory/Valuation/Basic.lean +++ b/Mathlib/RingTheory/Valuation/Basic.lean @@ -1404,16 +1404,16 @@ theorem ofAddValuation_apply (v : AddValuation R (Additive Γ₀)ᵒᵈ) (r : R) ofAddValuation v r = Additive.toMul (OrderDual.ofDual (v r)) := rfl -instance (v : Valuation R Γ₀) : CommMonoidWithZero (MonoidHom.mrange (.ofClass v : R →*₀ _)) := - inferInstanceAs (CommMonoidWithZero (MonoidHom.mrange (MonoidWithZeroHom.ofClass v))) +instance (v : Valuation R Γ₀) : CommMonoidWithZero (MonoidHomClass.toMonoidHom v).mrange := + inferInstanceAs (CommMonoidWithZero v.toMonoidHom.mrange) @[simp] lemma val_mrange_zero (v : Valuation R Γ₀) : - ((0 : MonoidHom.mrange (.ofClass v : R →*₀ _)) : Γ₀) = 0 := + ((0 : (MonoidHomClass.toMonoidHom v).mrange) : Γ₀) = 0 := rfl instance {Γ₀} [LinearOrderedCommGroupWithZero Γ₀] [DivisionRing K] (v : Valuation K Γ₀) : - CommGroupWithZero (MonoidHom.mrange (.ofClass v : K →*₀ _)) := - inferInstanceAs (CommGroupWithZero (MonoidHom.mrange (MonoidWithZeroHom.ofClass v))) + CommGroupWithZero (MonoidHomClass.toMonoidHom v : K →* _).mrange := + inferInstanceAs (CommGroupWithZero v.toMonoidHom.mrange) end Valuation diff --git a/Mathlib/RingTheory/Valuation/Discrete/IsDiscreteValuationRing.lean b/Mathlib/RingTheory/Valuation/Discrete/IsDiscreteValuationRing.lean index e59c952ac3bca7..02b586e9b08d9b 100644 --- a/Mathlib/RingTheory/Valuation/Discrete/IsDiscreteValuationRing.lean +++ b/Mathlib/RingTheory/Valuation/Discrete/IsDiscreteValuationRing.lean @@ -104,15 +104,15 @@ theorem exists_lift_of_le_one {x : K} (H : ((maximalIdeal A).valuation K) x ≤ exact hπ.ne_zero lemma mker_valuation_eq_isUnitSubmonoid : - MonoidHom.mker ((IsDiscreteValuationRing.maximalIdeal A).valuation K) = - (IsUnit.submonoid A).map (algebraMap A K) := by + ((IsDiscreteValuationRing.maximalIdeal A).valuation K).toMonoidHom.mker = + (IsUnit.submonoid A).map (algebraMap A K).toMonoidHom := by ext a simp only [MonoidHom.mem_mker, Submonoid.mem_map] - refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩ - · obtain ⟨b, rfl⟩ := IsDiscreteValuationRing.exists_lift_of_le_one h.le - rw [valuation_eq_one_iff_notMem] at h - simp only [IsDiscreteValuationRing.maximalIdeal, IsLocalRing.mem_maximalIdeal, mem_nonunits_iff, - not_not] at h + refine ⟨?_, fun h ↦ ?_⟩ + · simp_intro h + obtain ⟨b, rfl⟩ := IsDiscreteValuationRing.exists_lift_of_le_one h.le + simp only [valuation_eq_one_iff_notMem, IsDiscreteValuationRing.maximalIdeal, + IsLocalRing.mem_maximalIdeal, mem_nonunits_iff, not_not] at h use b, h · obtain ⟨x, h, rfl⟩ := h simpa [IsDiscreteValuationRing.maximalIdeal] using! h @@ -125,11 +125,12 @@ theorem associated_of_valuation_eq (x y : K) simp_all by_cases hy : y = 0 · simp_all - have : (y / x) ∈ MonoidHom.mker (((maximalIdeal A).valuation K)) := by simp_all + have : (y / x) ∈ ((maximalIdeal A).valuation K).toMonoidHom.mker := by simp_all rw [mker_valuation_eq_isUnitSubmonoid] at this obtain ⟨u, h⟩ := this use IsUnit.unit h.1 - simp only [Units.smul_def, Algebra.smul_def, IsUnit.unit_spec h.1, h.2] + simp only [Units.smul_def, Algebra.smul_def, IsUnit.unit_spec h.1, + MonoidHom.coe_coe (algebraMap A K) ▸ h.2] field_simp theorem map_algebraMap_eq_valuationSubring : Subring.map (algebraMap A K) ⊤ = diff --git a/Mathlib/RingTheory/Valuation/Integers.lean b/Mathlib/RingTheory/Valuation/Integers.lean index 86f52ce812579f..b85a68a489a3cb 100644 --- a/Mathlib/RingTheory/Valuation/Integers.lean +++ b/Mathlib/RingTheory/Valuation/Integers.lean @@ -209,12 +209,12 @@ lemma coe_span_singleton_eq_setOfPred_le_v_algebraMap (hv : Integers v O) (x : O alias coe_span_singleton_eq_setOf_le_v_algebraMap := coe_span_singleton_eq_setOfPred_le_v_algebraMap lemma bijective_algebraMap_of_subsingleton_units_mrange (hv : Integers v O) - [Subsingleton (MonoidHom.mrange v)ˣ] : + [Subsingleton (v.toMonoidHom.mrange)ˣ] : Function.Bijective (algebraMap O F) := by refine ⟨hv.hom_inj, fun x ↦ hv.exists_of_le_one ?_⟩ rcases eq_or_ne x 0 with rfl | hx · simp - · exact (congr_arg Units.val (Subsingleton.elim (α := (MonoidHom.mrange v)ˣ) + · exact (congr_arg Units.val (Subsingleton.elim (α := (MonoidHom.mrange v.toMonoidHom)ˣ) ((isUnit_iff_ne_zero.mpr hx).unit.map v.toMonoidHom.mrangeRestrict) 1)).le lemma isPrincipal_iff_exists_isGreatest (hv : Integers v O) {I : Ideal O} : diff --git a/Mathlib/RingTheory/ZariskisMainTheorem.lean b/Mathlib/RingTheory/ZariskisMainTheorem.lean index 98122731c6ffb3..aeb7431ed1f1e9 100644 --- a/Mathlib/RingTheory/ZariskisMainTheorem.lean +++ b/Mathlib/RingTheory/ZariskisMainTheorem.lean @@ -673,8 +673,7 @@ lemma ZariskisMainProperty.exists_fg_and_exists_notMem_and_awayMap_bijective · simp only [t, Set.finite_insert] exact s.finite_toSet.image (fun x ↦ r ^ m x * x) · rintro a (rfl | ⟨x, hx, rfl⟩); exacts [hr, hm _] - refine ⟨r', hrp, - IsLocalization.map_injective_of_injective _ _ _ Subtype.val_injective, ?_⟩ + refine ⟨r', hrp, IsLocalization.map_injective_of_injective _ _ _ Subtype.val_injective, ?_⟩ have : (IsScalarTower.toAlgHom R S _).range ≤ (Localization.awayMapₐ (Algebra.adjoin R t).val r').range := by rw [← Algebra.map_top, ← hs, Subalgebra.map_le, Algebra.adjoin_le_iff] diff --git a/Mathlib/Topology/Algebra/Valued/LocallyCompact.lean b/Mathlib/Topology/Algebra/Valued/LocallyCompact.lean index b10b0450b575b7..2ced620facd135 100644 --- a/Mathlib/Topology/Algebra/Valued/LocallyCompact.lean +++ b/Mathlib/Topology/Algebra/Valued/LocallyCompact.lean @@ -169,18 +169,14 @@ section CompactDVR open Valued lemma locallyFiniteOrder_units_mrange_of_isCompact_integer (hc : IsCompact (X := K) 𝒪[K]) : - Nonempty (LocallyFiniteOrder (MonoidHom.mrange (Valued.v : Valuation K Γ₀))ˣ) := by - -- This `change` line will become unnecessary once `MonoidHom.mrange` accepts `MonoidHom` - -- directly instead of a `MonoidHomClass` instance. - change Nonempty (LocallyFiniteOrder (MonoidHom.mrange - (MonoidWithZeroHom.ofClass (Valued.v (R := K))))ˣ) + Nonempty (LocallyFiniteOrder ((Valued.v : Valuation K Γ₀).toMonoidHom.mrange)ˣ) := by -- TODO: generalize to `Valuation.Integer`, which will require showing that `IsCompact` -- pulls back across `TopologicalSpace.induced` from a `LocallyCompactSpace`. constructor refine LocallyFiniteOrder.ofFiniteIcc ?_ -- We only need to show that we can construct a finite set for some set between -- a non-zero `z : Γ₀` and 1, because we can scale/invert this set to cover the whole group. - suffices ∀ z : (MonoidHom.mrange (MonoidWithZeroHom.ofClass (Valued.v (R := K))))ˣ, + suffices ∀ z : ((Valued.v (R := K)).toMonoidHom.mrange)ˣ, (Set.Icc z 1).Finite by rintro x y rcases lt_trichotomy y x with hxy | rfl | hxy @@ -212,8 +208,8 @@ lemma locallyFiniteOrder_units_mrange_of_isCompact_integer (hc : IsCompact (X := · rw [Set.Icc_eq_empty_of_lt] · exact Set.finite_empty · simp [hz1] - have z0' : 0 < (z : MonoidHom.mrange (MonoidWithZeroHom.ofClass (Valued.v (R := K)))) := by simp - have z0 : 0 < ((z : MonoidHom.mrange (MonoidWithZeroHom.ofClass (Valued.v (R := K)))) : Γ₀) := + have z0' : 0 < (z : (Valued.v : Valuation K Γ₀).toMonoidHom.mrange) := by simp + have z0 : 0 < ((z : (Valued.v (R := K)).mrange) : Γ₀) := Subtype.coe_lt_coe.mpr z0' have a0 : 0 < v a := by simpa [← ha] using z0 -- Construct our cover, which has an inner closed ball, and spheres for each element @@ -228,7 +224,8 @@ lemma locallyFiniteOrder_units_mrange_of_isCompact_integer (hc : IsCompact (X := split_ifs with hw · obtain ⟨b, hb⟩ := MonoidHom.mem_mrange.mp z.1.2 rw [← hb] at z0 ⊢ - simp only [MonoidWithZeroHom.coe_ofClass, ← v.restrict_le_iff] + simp only [MonoidHom.coe_mk, ZeroHom.toFun_eq_coe, MonoidWithZeroHom.toZeroHom_coe, + Valuation.toMonoidWithZeroHom_coe_eq_coe, OneHom.coe_mk, ← v.restrict_le_iff] refine Valued.isOpen_closedBall _ ?_ rw [ne_eq, ← map_zero v.restrict, v.restrict_inj, map_zero] exact z0.ne' @@ -262,7 +259,8 @@ lemma locallyFiniteOrder_units_mrange_of_isCompact_integer (hc : IsCompact (X := obtain ⟨j, hj, hj'⟩ := hj use j, hj -- and this `c` is either less than or greater than (or equal to) the threshold element - simp only [MonoidWithZeroHom.coe_ofClass] at hc + simp only [MonoidHom.coe_mk, ZeroHom.toFun_eq_coe, MonoidWithZeroHom.toZeroHom_coe, + Valuation.toMonoidWithZeroHom_coe_eq_coe, OneHom.coe_mk] at hc split_ifs at hj' with hcj · simp only [Set.mem_ofPred_eq, hc, Subtype.coe_le_coe, Units.val_le_val] at hj' simp [hcj, le_antisymm hj' hzi] @@ -271,7 +269,7 @@ lemma locallyFiniteOrder_units_mrange_of_isCompact_integer (hc : IsCompact (X := simp [← hj', hc] lemma mulArchimedean_mrange_of_isCompact_integer (hc : IsCompact (X := K) 𝒪[K]) : - MulArchimedean (MonoidHom.mrange (Valued.v : Valuation K Γ₀)) := by + MulArchimedean (Valued.v : Valuation K Γ₀).toMonoidHom.mrange := by rw [← Units.mulArchimedean_iff] obtain ⟨_⟩ := locallyFiniteOrder_units_mrange_of_isCompact_integer hc exact MulArchimedean.of_locallyFiniteOrder @@ -290,7 +288,7 @@ lemma isPrincipalIdealRing_of_compactSpace [hc : CompactSpace 𝒪[K]] : -- is a PIR iff the value group is not densely ordered. refine hi.isPrincipalIdealRing_iff_not_denselyOrdered_mrange.mpr fun _ ↦ ?_ -- since we are densely ordered, we necessarily are nontrivial - exact not_subsingleton (MonoidHom.mrange (v : Valuation K Γ₀))ˣ + exact not_subsingleton ((v : Valuation K Γ₀).toMonoidHom.mrange)ˣ (LocallyFiniteOrder.denselyOrdered_iff_subsingleton.mp inferInstance) theorem _root_.Valuation.isNontrivial_iff_not_a_field {K Γ : Type*} [Field K] diff --git a/Mathlib/Topology/Sheaves/CommRingCat.lean b/Mathlib/Topology/Sheaves/CommRingCat.lean index a84c2503552679..e3e1c999cf133f 100644 --- a/Mathlib/Topology/Sheaves/CommRingCat.lean +++ b/Mathlib/Topology/Sheaves/CommRingCat.lean @@ -152,7 +152,7 @@ instance (F : X.Sheaf CommRingCat.{w}) : Mono F.presheaf.toTotalQuotientPresheaf intro x hx rw [map_zero] apply (Submonoid.mem_iInf.mp hs ⟨x, hx⟩).2 - rw [← map_mul, e, map_zero] + simp [← map_mul, e] end SubmonoidPresheaf