diff --git a/Mathlib/Algebra/Ring/CompTypeclasses.lean b/Mathlib/Algebra/Ring/CompTypeclasses.lean index eeeedb7218e34f..930b2f215fc7fe 100644 --- a/Mathlib/Algebra/Ring/CompTypeclasses.lean +++ b/Mathlib/Algebra/Ring/CompTypeclasses.lean @@ -120,11 +120,8 @@ def toRingEquiv : R₁ ≃+* R₂ := .ofRingHom σ σ' comp_eq₂ comp_eq This is not an instance, as for equivalences that are involutions, a better instance would be `RingHomInvPair e e`. - -This declaration should not be used as an instance to state a theorem, -but it may be useful sometimes in the middle of a proof. -/ -theorem of_ringEquiv (e : R₁ ≃+* R₂) : RingHomInvPair (↑e : R₁ →+* R₂) ↑e.symm := +lemma of_ringEquiv (e : R₁ ≃+* R₂) : RingHomInvPair (↑e : R₁ →+* R₂) ↑e.symm := ⟨e.symm_toRingHom_comp_toRingHom, e.symm.symm_toRingHom_comp_toRingHom⟩ /-- Construct a `RingHomInvPair` from both directions of a ring equiv. diff --git a/Mathlib/RingTheory/ClassGroup.lean b/Mathlib/RingTheory/ClassGroup.lean index d39be3cd05f639..6bba7a37bb83da 100644 --- a/Mathlib/RingTheory/ClassGroup.lean +++ b/Mathlib/RingTheory/ClassGroup.lean @@ -414,3 +414,43 @@ theorem card_classGroup_eq_one_iff [IsDedekindDomain R] [Fintype (ClassGroup R)] by_cases hI : I = ⊥ · rw [hI]; exact bot_isPrincipal · exact (ClassGroup.mk0_eq_one_iff (mem_nonZeroDivisors_iff_ne_zero.mpr hI)).mp (eq_one _) + +section MulEquiv + +theorem FractionalIdeal.map_ringEquivOfRingEquiv_toPrincipalIdeal {S L : Type*} [CommRing S] + [IsDomain S] [Field L] [Algebra S L] [IsFractionRing S L] (f : R ≃+* S) : + Subgroup.map ((Units.mapEquiv (ringEquivOfRingEquiv K L f))).toMonoidHom + (toPrincipalIdeal R K).range = (toPrincipalIdeal S L).range := by + ext I + simp only [MulEquiv.toMonoidHom_eq_coe, Subgroup.mem_map, MonoidHom.mem_range, + toPrincipalIdeal_eq_iff, MonoidHom.coe_coe] + refine ⟨fun ⟨u, ⟨v, huv⟩, hu⟩ ↦ ?_, fun ⟨u, hu⟩ ↦ ?_⟩ + · use Units.map (IsFractionRing.ringEquivOfRingEquiv f (K := K) + (L := L)).toRingHom v + rw [← hu] + simp only [RingEquiv.toRingHom_eq_coe, Units.coe_map, MonoidHom.coe_coe, RingHom.coe_coe, + Units.coe_mapEquiv, ← huv, RingEquiv.coe_toMulEquiv] + rw [FractionalIdeal.ringEquivOfRingEquiv_spanSingleton] + · use Units.mapEquiv (FractionalIdeal.ringEquivOfRingEquiv _ _ f).symm.toMulEquiv I + refine ⟨?_, by simp [← Units.val_inj]⟩ + · use Units.map (IsFractionRing.ringEquivOfRingEquiv f (K := K) + (L := L)).symm.toRingHom u + simp only [IsFractionRing.ringEquivOfRingEquiv_symm, RingEquiv.toRingHom_eq_coe, + Units.coe_map, MonoidHom.coe_coe, RingHom.coe_coe, RingEquiv.toMulEquiv_eq_coe, + RingEquiv.coe_toMulEquiv_symm, Units.coe_mapEquiv] + rw [← FractionalIdeal.ringEquivOfRingEquiv_spanSingleton, + ← FractionalIdeal.ringEquivOfRingEquiv_symm_eq, hu] + rfl + +/-- A ring isomorphism `R ≃+* R'` induces an isomorphism on their class groups. -/ +@[simps!] +noncomputable def ClassGroup.mulEquiv {R' : Type*} [CommRing R'] [IsDomain R'] (g : R ≃+* R') : + ClassGroup R ≃* ClassGroup R' := + (ClassGroup.equiv (R := R) (FractionRing R)).trans + ((QuotientGroup.congr (toPrincipalIdeal R (FractionRing R)).range + (toPrincipalIdeal R' (FractionRing R')).range + (Units.mapEquiv (FractionalIdeal.ringEquivOfRingEquiv (FractionRing R) (FractionRing R') g)) + (FractionalIdeal.map_ringEquivOfRingEquiv_toPrincipalIdeal g)).trans + (ClassGroup.equiv (FractionRing R')).symm) + +end MulEquiv diff --git a/Mathlib/RingTheory/FractionalIdeal/Operations.lean b/Mathlib/RingTheory/FractionalIdeal/Operations.lean index 850d72496b7d4f..74119c26b13972 100644 --- a/Mathlib/RingTheory/FractionalIdeal/Operations.lean +++ b/Mathlib/RingTheory/FractionalIdeal/Operations.lean @@ -907,4 +907,124 @@ theorem mem_adjoinIntegral_self (hx : IsIntegral R x) : x ∈ adjoinIntegral S x end Adjoin +section RingEquiv + +open IsFractionRing + +variable {R S : Type*} (K L : Type*) [CommRing R] [IsDomain R] [CommRing S] [IsDomain S] + [CommRing K] [CommRing L] [Algebra R K] [Algebra S L] [IsFractionRing R K] [IsFractionRing S L] + (f : R ≃+* S) + +local instance (f : R ≃+* S) : RingHomInvPair (f : R →+* S) f.symm := + RingHomInvPair.of_ringEquiv f + +/-- If `f : R ≃+* S` is a ring isomorphism and `I : Submodule R K` is fractional with respect to +`R⁰`, then `I.map (IsFractionRing.semilinearEquivOfRingEquiv K L f).toLinearMap` +is fractional with respect to `S⁰`. + +Do not confuse with `IsFractional.map`. -/ +theorem _root_.IsFractional.mapEquiv {I : Submodule R K} (hI : IsFractional R⁰ I) : + IsFractional S⁰ (I.map (semilinearEquivOfRingEquiv K L f).toLinearMap) := by + simp only [IsFractional, mem_nonZeroDivisors_iff_ne_zero, ne_eq, Submodule.mem_map, + forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] at hI ⊢ + obtain ⟨r, hr0, hr⟩ := hI + use f r + refine ⟨by simp [hr0], ?_⟩ + intro x hx + specialize hr x hx + simp only [IsLocalization.IsInteger, RingHom.mem_rangeS] at hr ⊢ + obtain ⟨r', hr'⟩ := hr + use f r' + simp only [semilinearEquivOfRingEquiv, RingEquiv.toEquiv_eq_coe, Equiv.toFun_as_coe, + EquivLike.coe_coe, Equiv.invFun_as_coe, LinearMap.coe_mk, AddHom.coe_mk] + rw [Algebra.smul_def, ← ringEquivOfRingEquiv_algebraMap f (K := K) (L := L) r, + ← map_mul, ← Algebra.smul_def, ← hr', ringEquivOfRingEquiv_algebraMap] + +/-- The equiv `FractionalIdeal R⁰ K ≃+* FractionalIdeal S⁰ L` + induced by a ring isomorphism `f : R ≃+* S`. -/ +@[simps -isSimp] +noncomputable def ringEquivOfRingEquiv : + FractionalIdeal R⁰ K ≃+* FractionalIdeal S⁰ L := + { toFun I := ⟨Submodule.map (semilinearEquivOfRingEquiv _ _ f).toLinearMap I.val, + IsFractional.mapEquiv K L f I.prop⟩ + invFun J := ⟨J.val.map (semilinearEquivOfRingEquiv _ _ f.symm).toLinearMap, + IsFractional.mapEquiv L K f.symm J.prop⟩ + map_add' I J := by ext x; simp [← mem_coe] + map_mul' I J := by + simp only [FractionalIdeal.coe_ext_iff, val_eq_coe, coe_mul, coe_mk] + apply le_antisymm <;> simp only [map_le_iff_le_comap, Submodule.mul_le, mem_coe, mem_comap, + semilinearEquivOfRingEquiv_apply, map_mul, mem_map_equiv, + semilinearEquivOfRingEquiv_symm_apply, LinearEquiv.coe_coe] + · exact fun m hm n hn ↦ Submodule.mul_mem_mul (mem_map_of_mem hm) (mem_map_of_mem hn) + · exact fun m hm n hn ↦ Submodule.mul_mem_mul hm hn + left_inv I := by + simp only [RingEquiv.symm_symm, val_eq_coe, ← Submodule.map_comp, LinearEquiv.comp_coe, + coe_ext_iff, coe_mk] + convert Submodule.map_id _ + ext; simp [semilinearEquivOfRingEquiv, IsLocalization.map_map] + right_inv I := by + simp only [RingEquiv.symm_symm, val_eq_coe, ← Submodule.map_comp, LinearEquiv.comp_coe, + coe_ext_iff, coe_mk] + convert Submodule.map_id _ + ext; simp [semilinearEquivOfRingEquiv, IsLocalization.map_map]} + +lemma ringEquivOfRingEquiv_apply (f : R ≃+* S) (I : FractionalIdeal (nonZeroDivisors R) K) : + ringEquivOfRingEquiv K L f I = + ⟨Submodule.map (semilinearEquivOfRingEquiv _ _ f).toLinearMap I.val, + IsFractional.mapEquiv K L f I.prop⟩ := rfl + +lemma ringEquivOfRingEquiv_apply_val (f : R ≃+* S) (I : FractionalIdeal R⁰ K) : + (ringEquivOfRingEquiv K L f I).val = + I.val.map (semilinearEquivOfRingEquiv _ _ f).toLinearMap := rfl + +lemma ringEquivOfRingEquiv_trans {T : Type*} [CommRing T] [IsDomain T] (M : Type*) [CommRing M] + [Algebra T M] [IsFractionRing T M] (f : R ≃+* S) (g : S ≃+* T) : + ringEquivOfRingEquiv K M (f.trans g) = + (ringEquivOfRingEquiv K L f).trans (ringEquivOfRingEquiv L M g) := by + have : RingHomCompTriple f (g : S →+* T) (f.trans g : R →+* T) := ⟨rfl⟩ + ext1 I + simp only [ringEquivOfRingEquiv, RingEquiv.coe_ringHom_trans, Function.comp_apply, + semilinearEquivOfRingEquiv_comp K L f M, LinearEquiv.coe_trans, + Submodule.map_comp, RingEquiv.coe_mk, Equiv.coe_fn_mk, RingEquiv.coe_trans] + +lemma ringEquivOfRingEquiv_trans_apply {T : Type*} [CommRing T] [IsDomain T] (M : Type*) + [CommRing M] [Algebra T M] [IsFractionRing T M] + (f : R ≃+* S) (g : S ≃+* T) (I : FractionalIdeal R⁰ K) : + ringEquivOfRingEquiv K M (f.trans g) I = + ringEquivOfRingEquiv L M g (ringEquivOfRingEquiv K L f I) := by + simp [ringEquivOfRingEquiv_trans K L M] + +lemma ringEquivOfRingEquiv_refl : + ringEquivOfRingEquiv K K (RingEquiv.refl R) = RingEquiv.refl (FractionalIdeal R⁰ K) := by + ext I x + simp only [ringEquivOfRingEquiv_apply, RingEquiv.coe_ringHom_refl, RingEquiv.symm_refl, + val_eq_coe, RingEquiv.refl_apply, ← mem_coe] + simp [semilinearEquivOfRingEquiv] + +lemma ringEquivOfRingEquiv_spanSingleton (x : K) : + FractionalIdeal.ringEquivOfRingEquiv K L f (spanSingleton R⁰ x) = + spanSingleton S⁰ (IsFractionRing.ringEquivOfRingEquiv (L := L) f x) := by + simp only [ringEquivOfRingEquiv, val_eq_coe, RingEquiv.symm_symm, RingEquiv.coe_mk, + Equiv.coe_fn_mk, coe_spanSingleton, IsFractionRing.ringEquivOfRingEquiv_apply] + rw [SetLike.ext_iff] + intro y + simp only [← FractionalIdeal.mem_coe, coe_mk, mem_map_equiv, coe_spanSingleton, + Submodule.mem_span_singleton, (semilinearEquivOfRingEquiv K L f).eq_symm_apply] + constructor + · rintro ⟨r, rfl⟩ + use f r + exact .symm (map_smulₛₗ _ r x) + · rintro ⟨s, rfl⟩ + use f.symm s + simp only [Algebra.smul_def, semilinearEquivOfRingEquiv_apply, map_mul, map_eq, RingHom.coe_coe, + IsFractionRing.ringEquivOfRingEquiv_apply, RingEquiv.apply_symm_apply] + +lemma ringEquivOfRingEquiv_symm_eq : + (FractionalIdeal.ringEquivOfRingEquiv K L f).symm = + FractionalIdeal.ringEquivOfRingEquiv L K f.symm := by + exact (RingEquiv.coe_nonUnitalRingHom_inj_iff (ringEquivOfRingEquiv K L f).symm + (ringEquivOfRingEquiv L K f.symm)).mpr rfl + +end RingEquiv + end FractionalIdeal diff --git a/Mathlib/RingTheory/IntegralClosure/IsIntegral/Basic.lean b/Mathlib/RingTheory/IntegralClosure/IsIntegral/Basic.lean index fef2feb9d37219..bd50c884363e1e 100644 --- a/Mathlib/RingTheory/IntegralClosure/IsIntegral/Basic.lean +++ b/Mathlib/RingTheory/IntegralClosure/IsIntegral/Basic.lean @@ -175,8 +175,8 @@ theorem RingEquiv.isIntegral_iff {R S T : Type*} [CommRing R] [Ring S] [CommRing ⟨fun r t s ↦ by simp only [Algebra.smul_def, map_mul, ← h, mul_assoc]; rfl⟩ exact IsIntegral.tower_top ha · have h' : (algebraMap T S) = (algebraMap R S).comp φ.symm.toRingHom := by - simp only [← h, RingHom.comp_assoc, RingEquiv.toRingHom_eq_coe, RingEquiv.comp_symm, - RingHomCompTriple.comp_eq] + have : RingHomInvPair (φ : R →+* T) φ.symm := RingHomInvPair.of_ringEquiv _ + simp only [← h, RingHom.comp_assoc, RingEquiv.toRingHom_eq_coe, RingHomCompTriple.comp_eq] letI : Algebra T R := φ.symm.toRingHom.toAlgebra letI : IsScalarTower T R S := ⟨fun r t s ↦ by simp only [Algebra.smul_def, map_mul, h', mul_assoc]; rfl⟩ diff --git a/Mathlib/RingTheory/LocalProperties/Basic.lean b/Mathlib/RingTheory/LocalProperties/Basic.lean index 6ff5441e2cc22b..5ca5e25ade65c0 100644 --- a/Mathlib/RingTheory/LocalProperties/Basic.lean +++ b/Mathlib/RingTheory/LocalProperties/Basic.lean @@ -329,10 +329,11 @@ lemma RingHom.LocalizationAwayPreserves.respectsIso have : IsLocalization.Away (f 1) T := IsLocalization.away_of_isUnit_of_bijective _ (by simp) (Equiv.refl _).bijective convert hP f 1 R T hf + have : RingHomInvPair (e : R →+* S) e.symm := RingHomInvPair.of_ringEquiv _ have : (IsLocalization.Away.map R T f 1).comp e.symm.toRingHom = f := IsLocalization.map_comp .. conv_lhs => rw [← this, RingHom.comp_assoc] - simp only [RingEquiv.toRingHom_eq_coe, RingEquiv.symm_comp, RingHomCompTriple.comp_eq] + simp only [RingEquiv.toRingHom_eq_coe, RingHomCompTriple.comp_eq] lemma RingHom.StableUnderCompositionWithLocalizationAway.respectsIso (hP : StableUnderCompositionWithLocalizationAway P) : diff --git a/Mathlib/RingTheory/Localization/FractionRing.lean b/Mathlib/RingTheory/Localization/FractionRing.lean index 2a25d46dc20da6..4e5023ffa872f2 100644 --- a/Mathlib/RingTheory/Localization/FractionRing.lean +++ b/Mathlib/RingTheory/Localization/FractionRing.lean @@ -9,6 +9,7 @@ public import Mathlib.Algebra.Field.Equiv public import Mathlib.Algebra.Field.Subfield.Basic public import Mathlib.Algebra.Order.GroupWithZero.Submonoid public import Mathlib.Algebra.Order.Ring.Int +public import Mathlib.Algebra.Ring.CompTypeclasses public import Mathlib.RingTheory.Localization.Basic public import Mathlib.RingTheory.SimpleRing.Basic @@ -423,20 +424,68 @@ variable {A K B L : Type*} [CommRing A] [CommRing B] [CommRing K] [CommRing L] /-- Given rings `A, B` and localization maps to their fraction rings `f : A →+* K, g : B →+* L`, an isomorphism `h : A ≃+* B` induces an isomorphism of fraction rings `K ≃+* L`. -/ +@[simps!] noncomputable def ringEquivOfRingEquiv : K ≃+* L := IsLocalization.ringEquivOfRingEquiv K L h (MulEquivClass.map_nonZeroDivisors h) -@[simp] lemma ringEquivOfRingEquiv_algebraMap (a : A) : ringEquivOfRingEquiv h (algebraMap A K a) = algebraMap B L (h a) := by - simp [ringEquivOfRingEquiv] + simp @[simp] lemma ringEquivOfRingEquiv_symm : (ringEquivOfRingEquiv h : K ≃+* L).symm = ringEquivOfRingEquiv h.symm := rfl +variable (K L) in +theorem ringEquivOfRingEquiv_comp {C : Type*} (M : Type*) [CommRing C] + [CommRing M] [Algebra C M] [IsFractionRing C M] (f : A ≃+* B) (g : B ≃+* C) : + (ringEquivOfRingEquiv (f.trans g)) = + (ringEquivOfRingEquiv (K := K) f).trans (ringEquivOfRingEquiv (K := L) (L := M) g) := by + ext a + simp [IsLocalization.map_map] + end ringEquivOfRingEquiv +section semilinearEquivOfRingEquiv + +variable {A B : Type*} (K L : Type*) [CommRing A] [CommRing B] [CommRing K] [CommRing L] + [Algebra A K] [IsFractionRing A K] [Algebra B L] [IsFractionRing B L] (f : A ≃+* B) + +local instance : RingHomInvPair (f : A →+* B) f.symm := + RingHomInvPair.of_ringEquiv f + +/-- Given rings `A, B` and localization maps to their fraction rings +`f : A →+* K, g : B →+* L`, an isomorphism `h : A ≃+* B` induces a semilinear equivalence +fraction rings `K ≃ₛₗ[f.toRingHom] L`. -/ +noncomputable def semilinearEquivOfRingEquiv : K ≃ₛₗ[(f : A →+* B)] L := +{ ringEquivOfRingEquiv f with + map_smul' r x := by simp [Algebra.smul_def] } + +lemma semilinearEquivOfRingEquiv_apply (x : K) : + (semilinearEquivOfRingEquiv K L f) x = (ringEquivOfRingEquiv f) x := rfl + +@[simp] +lemma semilinearEquivOfRingEquiv_algebraMap (a : A) : + semilinearEquivOfRingEquiv K L f (algebraMap A K a) = algebraMap B L (f a) := by + simp [semilinearEquivOfRingEquiv, ringEquivOfRingEquiv] + +lemma semilinearEquivOfRingEquiv_symm_apply (x : L) : + (semilinearEquivOfRingEquiv K L f).symm x = (ringEquivOfRingEquiv f).symm x := rfl + +lemma semilinearEquivOfRingEquiv_comp {C : Type*} (M : Type*) [CommRing C] [CommRing M] + [Algebra C M] [IsFractionRing C M] (g : B ≃+* C) : + let : RingHomCompTriple f (g : B →+* C) (f.trans g : A →+* C) := ⟨rfl⟩ + let : RingHomCompTriple g.symm (f.symm : B →+* A) ((f.trans g).symm : C →+* A) := ⟨rfl⟩ + (semilinearEquivOfRingEquiv K M (f.trans g)) = + LinearEquiv.trans (σ₁₃ := (f.trans g)) (σ₃₁ := (f.trans g).symm) + (semilinearEquivOfRingEquiv K L f) + (semilinearEquivOfRingEquiv L M g) := by + ext a + simp [-RingEquiv.coe_ringHom_trans, semilinearEquivOfRingEquiv_apply, + semilinearEquivOfRingEquiv_apply K M, ringEquivOfRingEquiv_comp K L M] + +end semilinearEquivOfRingEquiv + section algEquivOfAlgEquiv variable {R A K B L : Type*} [CommSemiring R] [CommRing A] [CommRing B] [CommRing K] [CommRing L]