Skip to content

Commit 1825e17

Browse files
xroblotxroblot
committed
chore(Trace/Quotient): move isomorphism to Localization.AtPrime.Basic (leanprover-community#32045)
This PR move isomorphisms previously defined in `Trace.Quotient` into `Localization.AtPrime.Basic`. The change is purely organizational: `Localization.AtPrime.Basic` is the canonical place for lemmas and constructions about localization at a prime. The isomorphisms are also renamed to match their new namespace: - `equivQuotMaximalIdealOfIsLocalization` -> `IsLocalization.AtPrime.equivQuotMaximalIdeal` - `quotMapEquivQuotMapMaximalIdealOfIsLocalization` -> `IsLocalization.AtPrime.equivQuotMapMaximalIdeal`
1 parent ec195f6 commit 1825e17

File tree

2 files changed

+142
-108
lines changed

2 files changed

+142
-108
lines changed

‎Mathlib/RingTheory/Localization/AtPrime/Basic.lean‎

Lines changed: 129 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -364,8 +364,137 @@ theorem map_eq_maximalIdeal : p.map (algebraMap R Rₚ) = maximalIdeal Rₚ := b
364364
convert congr_arg (Ideal.map (algebraMap R Rₚ)) (comap_maximalIdeal Rₚ p).symm
365365
rw [map_comap p.primeCompl]
366366

367+
instance isMaximal_map : (p.map (algebraMap R Rₚ)).IsMaximal := by
368+
rw [map_eq_maximalIdeal]
369+
exact maximalIdeal.isMaximal Rₚ
370+
367371
theorem comap_map_of_isMaximal [P.IsMaximal] [P.LiesOver p] :
368372
Ideal.comap (algebraMap S Sₚ) (Ideal.map (algebraMap S Sₚ) P) = P :=
369373
comap_map_eq_self_of_isMaximal _ (isPrime_map_of_liesOver S p Sₚ P).ne_top
370374

375+
section isomorphisms
376+
377+
attribute [local instance] Ideal.Quotient.field
378+
379+
variable {S R : Type*} [CommRing R] (p : Ideal R) [p.IsMaximal]
380+
variable (Rₚ : Type*) [CommRing Rₚ] [Algebra R Rₚ] [IsLocalization.AtPrime Rₚ p] [IsLocalRing Rₚ]
381+
382+
open IsLocalRing
383+
384+
/-- The isomorphism `R ⧸ p ≃+* Rₚ ⧸ maximalIdeal Rₚ`, where `Rₚ` satisfies
385+
`IsLocalization.AtPrime Rₚ p`. In particular, localization preserves the residue field. -/
386+
noncomputable
387+
def equivQuotMaximalIdeal : R ⧸ p ≃+* Rₚ ⧸ maximalIdeal Rₚ := by
388+
refine (Ideal.quotEquivOfEq ?_).trans
389+
(RingHom.quotientKerEquivOfSurjective (f := algebraMap R (Rₚ ⧸ maximalIdeal Rₚ)) ?_)
390+
· rw [IsScalarTower.algebraMap_eq R Rₚ, ← RingHom.comap_ker,
391+
Ideal.Quotient.algebraMap_eq, Ideal.mk_ker, IsLocalization.AtPrime.comap_maximalIdeal Rₚ p]
392+
· intro x
393+
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
394+
obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq p.primeCompl x
395+
obtain ⟨s', hs⟩ := Ideal.Quotient.mk_surjective (I := p) (Ideal.Quotient.mk p s)⁻¹
396+
simp only [IsScalarTower.algebraMap_eq R Rₚ (Rₚ ⧸ _),
397+
Ideal.Quotient.algebraMap_eq, RingHom.comp_apply]
398+
use x * s'
399+
rw [← sub_eq_zero, ← map_sub, Ideal.Quotient.eq_zero_iff_mem]
400+
have : algebraMap R Rₚ s ∉ maximalIdeal Rₚ := by
401+
rw [← Ideal.mem_comap, IsLocalization.AtPrime.comap_maximalIdeal Rₚ p]
402+
exact s.prop
403+
refine ((inferInstanceAs <| (maximalIdeal Rₚ).IsPrime).mem_or_mem ?_).resolve_left this
404+
rw [mul_sub, IsLocalization.mul_mk'_eq_mk'_of_mul, IsLocalization.mk'_mul_cancel_left,
405+
← map_mul, ← map_sub, ← Ideal.mem_comap, IsLocalization.AtPrime.comap_maximalIdeal Rₚ p,
406+
mul_left_comm, ← Ideal.Quotient.eq_zero_iff_mem, map_sub, map_mul, map_mul, hs,
407+
mul_inv_cancel₀, mul_one, sub_self]
408+
rw [Ne, Ideal.Quotient.eq_zero_iff_mem]
409+
exact s.prop
410+
411+
@[deprecated (since := "2025-11-13")] alias _root_.equivQuotMaximalIdealOfIsLocalization :=
412+
equivQuotMaximalIdeal
413+
414+
variable {Sₚ : Type*} [CommRing S] [Algebra R S] [CommRing Sₚ] [Algebra S Sₚ] [Algebra R Sₚ]
415+
variable [Algebra Rₚ Sₚ] [IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ]
416+
variable [IsScalarTower R S Sₚ]
417+
418+
local notation "pS" => Ideal.map (algebraMap R S) p
419+
local notation "pSₚ" => Ideal.map (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)
420+
421+
lemma comap_map_eq_map :
422+
(Ideal.map (algebraMap R Sₚ) p).comap (algebraMap S Sₚ) = pS := by
423+
rw [IsScalarTower.algebraMap_eq R S Sₚ, ← Ideal.map_map, eq_comm]
424+
apply Ideal.le_comap_map.antisymm
425+
intro x hx
426+
obtain ⟨α, hα, hαx⟩ : ∃ α ∉ p, α • x ∈ pS := by
427+
have ⟨⟨y, s⟩, hy⟩ := (IsLocalization.mem_map_algebraMap_iff
428+
(Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ).mp hx
429+
rw [← map_mul,
430+
IsLocalization.eq_iff_exists (Algebra.algebraMapSubmonoid S p.primeCompl)] at hy
431+
obtain ⟨c, hc⟩ := hy
432+
obtain ⟨α, hα, e⟩ := (c * s).prop
433+
refine ⟨α, hα, ?_⟩
434+
rw [Algebra.smul_def, e, Submonoid.coe_mul, mul_assoc, mul_comm _ x, hc]
435+
exact Ideal.mul_mem_left _ _ y.prop
436+
obtain ⟨β, γ, hγ, hβ⟩ : ∃ β γ, γ ∈ p ∧ β * α = 1 + γ := by
437+
obtain ⟨β, hβ⟩ := Ideal.Quotient.mk_surjective (I := p) (Ideal.Quotient.mk p α)⁻¹
438+
refine ⟨β, β * α - 1, ?_, ?_⟩
439+
· rw [← Ideal.Quotient.eq_zero_iff_mem, map_sub, map_one,
440+
map_mul, hβ, inv_mul_cancel₀, sub_self]
441+
rwa [Ne, Ideal.Quotient.eq_zero_iff_mem]
442+
· rw [add_sub_cancel]
443+
have := Ideal.mul_mem_left _ (algebraMap _ _ β) hαx
444+
rw [← Algebra.smul_def, smul_smul, hβ, add_smul, one_smul] at this
445+
refine (Submodule.add_mem_iff_left pS ?_).mp this
446+
rw [Algebra.smul_def]
447+
apply Ideal.mul_mem_right
448+
exact Ideal.mem_map_of_mem _ hγ
449+
450+
@[deprecated (since := "2025-07-31")] alias
451+
_root_.comap_map_eq_map_of_isLocalization_algebraMapSubmonoid := comap_map_eq_map
452+
453+
variable [IsScalarTower R Rₚ Sₚ]
454+
455+
variable (S Sₚ) in
456+
/--
457+
The isomorphism `S ⧸ pS ≃+* Sₚ ⧸ p·Sₚ`, where `Sₚ` is the localization of `S` at the (image) of
458+
the complement of `p`
459+
-/
460+
noncomputable def equivQuotientMapMaximalIdeal [p.IsMaximal] :
461+
S ⧸ pS ≃+* Sₚ ⧸ pSₚ := by
462+
haveI h : pSₚ = Ideal.map (algebraMap S Sₚ) pS := by
463+
rw [← map_eq_maximalIdeal p, Ideal.map_map,
464+
← IsScalarTower.algebraMap_eq, Ideal.map_map, ← IsScalarTower.algebraMap_eq]
465+
refine (Ideal.quotEquivOfEq ?_).trans
466+
(RingHom.quotientKerEquivOfSurjective (f := algebraMap S (Sₚ ⧸ pSₚ)) ?_)
467+
· rw [IsScalarTower.algebraMap_eq S Sₚ, Ideal.Quotient.algebraMap_eq, ← RingHom.comap_ker,
468+
Ideal.mk_ker, h, Ideal.map_map, ← IsScalarTower.algebraMap_eq, comap_map_eq_map]
469+
· intro x
470+
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
471+
obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq
472+
(Algebra.algebraMapSubmonoid S p.primeCompl) x
473+
obtain ⟨α, hα : α ∉ p, e⟩ := s.prop
474+
obtain ⟨β, γ, hγ, hβ⟩ : ∃ β γ, γ ∈ p ∧ α * β = 1 + γ := by
475+
obtain ⟨β, hβ⟩ := Ideal.Quotient.mk_surjective (I := p) (Ideal.Quotient.mk p α)⁻¹
476+
refine ⟨β, α * β - 1, ?_, ?_⟩
477+
· rw [← Ideal.Quotient.eq_zero_iff_mem, map_sub, map_one,
478+
map_mul, hβ, mul_inv_cancel₀, sub_self]
479+
rwa [Ne, Ideal.Quotient.eq_zero_iff_mem]
480+
· rw [add_sub_cancel]
481+
use β • x
482+
rw [IsScalarTower.algebraMap_eq S Sₚ (Sₚ ⧸ pSₚ), Ideal.Quotient.algebraMap_eq,
483+
RingHom.comp_apply, ← sub_eq_zero, ← map_sub, Ideal.Quotient.eq_zero_iff_mem]
484+
rw [h, IsLocalization.mem_map_algebraMap_iff
485+
(Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ]
486+
refine ⟨⟨⟨γ • x, ?_⟩, s⟩, ?_⟩
487+
· rw [Algebra.smul_def]
488+
apply Ideal.mul_mem_right
489+
exact Ideal.mem_map_of_mem _ hγ
490+
simp only
491+
rw [mul_comm, mul_sub, IsLocalization.mul_mk'_eq_mk'_of_mul,
492+
IsLocalization.mk'_mul_cancel_left, ← map_mul, ← e, ← Algebra.smul_def, smul_smul,
493+
hβ, ← map_sub, add_smul, one_smul, add_comm x, add_sub_cancel_right]
494+
495+
@[deprecated (since := "2025-07-31")] alias
496+
_root_.quotMapEquivQuotMapMaximalIdealOfIsLocalization := equivQuotientMapMaximalIdeal
497+
498+
end isomorphisms
499+
371500
end IsLocalization.AtPrime

‎Mathlib/RingTheory/Trace/Quotient.lean‎

Lines changed: 13 additions & 108 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,7 @@ module
88
public import Mathlib.RingTheory.DedekindDomain.Dvr
99
public import Mathlib.RingTheory.IntegralClosure.IntegralRestrict
1010
public import Mathlib.RingTheory.LocalRing.Quotient
11+
public import Mathlib.RingTheory.Localization.AtPrime.Basic
1112

1213
/-!
1314
@@ -25,7 +26,7 @@ quotients and localizations.
2526

2627
variable {R S : Type*} [CommRing R] [CommRing S] [Algebra R S]
2728

28-
open IsLocalRing FiniteDimensional Submodule
29+
open IsLocalRing FiniteDimensional Submodule IsLocalization.AtPrime
2930

3031
section IsLocalRing
3132

@@ -54,130 +55,34 @@ end IsLocalRing
5455
section IsDedekindDomain
5556

5657
variable (p : Ideal R) [p.IsMaximal]
57-
variable {Rₚ Sₚ : Type*} [CommRing Rₚ] [CommRing Sₚ] [Algebra R Rₚ] [IsLocalization.AtPrime Rₚ p]
58+
variable (Rₚ Sₚ : Type*) [CommRing Rₚ] [CommRing Sₚ] [Algebra R Rₚ] [IsLocalization.AtPrime Rₚ p]
5859
variable [IsLocalRing Rₚ] [Algebra S Sₚ] [Algebra R Sₚ] [Algebra Rₚ Sₚ]
5960
variable [IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ]
6061
variable [IsScalarTower R S Sₚ] [IsScalarTower R Rₚ Sₚ]
6162

62-
variable (Rₚ)
63-
6463
attribute [local instance] Ideal.Quotient.field
6564

66-
/-- The isomorphism `R ⧸ p ≃+* Rₚ ⧸ maximalIdeal Rₚ`, where `Rₚ` satisfies
67-
`IsLocalization.AtPrime Rₚ p`. In particular, localization preserves the residue field. -/
68-
noncomputable
69-
def equivQuotMaximalIdealOfIsLocalization : R ⧸ p ≃+* Rₚ ⧸ maximalIdeal Rₚ := by
70-
refine (Ideal.quotEquivOfEq ?_).trans
71-
(RingHom.quotientKerEquivOfSurjective (f := algebraMap R (Rₚ ⧸ maximalIdeal Rₚ)) ?_)
72-
· rw [IsScalarTower.algebraMap_eq R Rₚ, ← RingHom.comap_ker,
73-
Ideal.Quotient.algebraMap_eq, Ideal.mk_ker, IsLocalization.AtPrime.comap_maximalIdeal Rₚ p]
74-
· intro x
75-
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
76-
obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq p.primeCompl x
77-
obtain ⟨s', hs⟩ := Ideal.Quotient.mk_surjective (I := p) (Ideal.Quotient.mk p s)⁻¹
78-
simp only [IsScalarTower.algebraMap_eq R Rₚ (Rₚ ⧸ _),
79-
Ideal.Quotient.algebraMap_eq, RingHom.comp_apply]
80-
use x * s'
81-
rw [← sub_eq_zero, ← map_sub, Ideal.Quotient.eq_zero_iff_mem]
82-
have : algebraMap R Rₚ s ∉ maximalIdeal Rₚ := by
83-
rw [← Ideal.mem_comap, IsLocalization.AtPrime.comap_maximalIdeal Rₚ p]
84-
exact s.prop
85-
refine ((inferInstanceAs <| (maximalIdeal Rₚ).IsPrime).mem_or_mem ?_).resolve_left this
86-
rw [mul_sub, IsLocalization.mul_mk'_eq_mk'_of_mul, IsLocalization.mk'_mul_cancel_left,
87-
← map_mul, ← map_sub, ← Ideal.mem_comap, IsLocalization.AtPrime.comap_maximalIdeal Rₚ p,
88-
mul_left_comm, ← Ideal.Quotient.eq_zero_iff_mem, map_sub, map_mul, map_mul, hs,
89-
mul_inv_cancel₀, mul_one, sub_self]
90-
rw [Ne, Ideal.Quotient.eq_zero_iff_mem]
91-
exact s.prop
92-
9365
local notation "pS" => Ideal.map (algebraMap R S) p
9466
local notation "pSₚ" => Ideal.map (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)
9567

96-
lemma comap_map_eq_map_of_isLocalization_algebraMapSubmonoid :
97-
(Ideal.map (algebraMap R Sₚ) p).comap (algebraMap S Sₚ) = pS := by
98-
rw [IsScalarTower.algebraMap_eq R S Sₚ, ← Ideal.map_map, eq_comm]
99-
apply Ideal.le_comap_map.antisymm
100-
intro x hx
101-
obtain ⟨α, hα, hαx⟩ : ∃ α ∉ p, α • x ∈ pS := by
102-
have ⟨⟨y, s⟩, hy⟩ := (IsLocalization.mem_map_algebraMap_iff
103-
(Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ).mp hx
104-
rw [← map_mul,
105-
IsLocalization.eq_iff_exists (Algebra.algebraMapSubmonoid S p.primeCompl)] at hy
106-
obtain ⟨c, hc⟩ := hy
107-
obtain ⟨α, hα, e⟩ := (c * s).prop
108-
refine ⟨α, hα, ?_⟩
109-
rw [Algebra.smul_def, e, Submonoid.coe_mul, mul_assoc, mul_comm _ x, hc]
110-
exact Ideal.mul_mem_left _ _ y.prop
111-
obtain ⟨β, γ, hγ, hβ⟩ : ∃ β γ, γ ∈ p ∧ β * α = 1 + γ := by
112-
obtain ⟨β, hβ⟩ := Ideal.Quotient.mk_surjective (I := p) (Ideal.Quotient.mk p α)⁻¹
113-
refine ⟨β, β * α - 1, ?_, ?_⟩
114-
· rw [← Ideal.Quotient.eq_zero_iff_mem, map_sub, map_one,
115-
map_mul, hβ, inv_mul_cancel₀, sub_self]
116-
rwa [Ne, Ideal.Quotient.eq_zero_iff_mem]
117-
· rw [add_sub_cancel]
118-
have := Ideal.mul_mem_left _ (algebraMap _ _ β) hαx
119-
rw [← Algebra.smul_def, smul_smul, hβ, add_smul, one_smul] at this
120-
refine (Submodule.add_mem_iff_left _ ?_).mp this
121-
rw [Algebra.smul_def]
122-
apply Ideal.mul_mem_right
123-
exact Ideal.mem_map_of_mem _ hγ
124-
125-
variable (S Sₚ)
126-
127-
/-- The isomorphism `S ⧸ pS ≃+* Sₚ ⧸ pSₚ`. -/
128-
noncomputable
129-
def quotMapEquivQuotMapMaximalIdealOfIsLocalization : S ⧸ pS ≃+* Sₚ ⧸ pSₚ := by
130-
haveI h : pSₚ = Ideal.map (algebraMap S Sₚ) pS := by
131-
rw [← IsLocalization.AtPrime.map_eq_maximalIdeal p Rₚ, Ideal.map_map,
132-
← IsScalarTower.algebraMap_eq, Ideal.map_map, ← IsScalarTower.algebraMap_eq]
133-
refine (Ideal.quotEquivOfEq ?_).trans
134-
(RingHom.quotientKerEquivOfSurjective (f := algebraMap S (Sₚ ⧸ pSₚ)) ?_)
135-
· rw [IsScalarTower.algebraMap_eq S Sₚ, Ideal.Quotient.algebraMap_eq, ← RingHom.comap_ker,
136-
Ideal.mk_ker, h, Ideal.map_map, ← IsScalarTower.algebraMap_eq,
137-
comap_map_eq_map_of_isLocalization_algebraMapSubmonoid]
138-
· intro x
139-
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
140-
obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq
141-
(Algebra.algebraMapSubmonoid S p.primeCompl) x
142-
obtain ⟨α, hα : α ∉ p, e⟩ := s.prop
143-
obtain ⟨β, γ, hγ, hβ⟩ : ∃ β γ, γ ∈ p ∧ α * β = 1 + γ := by
144-
obtain ⟨β, hβ⟩ := Ideal.Quotient.mk_surjective (I := p) (Ideal.Quotient.mk p α)⁻¹
145-
refine ⟨β, α * β - 1, ?_, ?_⟩
146-
· rw [← Ideal.Quotient.eq_zero_iff_mem, map_sub, map_one,
147-
map_mul, hβ, mul_inv_cancel₀, sub_self]
148-
rwa [Ne, Ideal.Quotient.eq_zero_iff_mem]
149-
· rw [add_sub_cancel]
150-
use β • x
151-
rw [IsScalarTower.algebraMap_eq S Sₚ (Sₚ ⧸ pSₚ), Ideal.Quotient.algebraMap_eq,
152-
RingHom.comp_apply, ← sub_eq_zero, ← map_sub, Ideal.Quotient.eq_zero_iff_mem]
153-
rw [h, IsLocalization.mem_map_algebraMap_iff
154-
(Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ]
155-
refine ⟨⟨⟨γ • x, ?_⟩, s⟩, ?_⟩
156-
· rw [Algebra.smul_def]
157-
apply Ideal.mul_mem_right
158-
exact Ideal.mem_map_of_mem _ hγ
159-
simp only
160-
rw [mul_comm, mul_sub, IsLocalization.mul_mk'_eq_mk'_of_mul,
161-
IsLocalization.mk'_mul_cancel_left, ← map_mul, ← e, ← Algebra.smul_def, smul_smul,
162-
hβ, ← map_sub, add_smul, one_smul, add_comm x, add_sub_cancel_right]
68+
variable (S)
16369

16470
lemma trace_quotient_eq_trace_localization_quotient (x) :
16571
Algebra.trace (R ⧸ p) (S ⧸ pS) (Ideal.Quotient.mk pS x) =
166-
(equivQuotMaximalIdealOfIsLocalization p Rₚ).symm
72+
(equivQuotMaximalIdeal p Rₚ).symm
16773
(Algebra.trace (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ) (algebraMap S _ x)) := by
16874
have : IsScalarTower R (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ) := by
16975
apply IsScalarTower.of_algebraMap_eq'
17076
rw [IsScalarTower.algebraMap_eq R Rₚ (Rₚ ⧸ _), IsScalarTower.algebraMap_eq R Rₚ (Sₚ ⧸ _),
17177
← RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq Rₚ]
172-
rw [Algebra.trace_eq_of_equiv_equiv (equivQuotMaximalIdealOfIsLocalization p Rₚ)
173-
(quotMapEquivQuotMapMaximalIdealOfIsLocalization S p Rₚ Sₚ)]
78+
rw [Algebra.trace_eq_of_equiv_equiv (equivQuotMaximalIdeal p Rₚ)
79+
(equivQuotientMapMaximalIdeal S p Rₚ Sₚ)]
17480
· congr
17581
· ext x
176-
simp only [equivQuotMaximalIdealOfIsLocalization, RingHom.quotientKerEquivOfSurjective,
82+
simp only [equivQuotMaximalIdeal, RingHom.quotientKerEquivOfSurjective,
17783
RingEquiv.coe_ringHom_trans, RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply,
17884
Ideal.quotEquivOfEq_mk, RingHom.quotientKerEquivOfRightInverse.apply, RingHom.kerLift_mk,
179-
quotMapEquivQuotMapMaximalIdealOfIsLocalization,
180-
Ideal.Quotient.algebraMap_quotient_map_quotient]
85+
equivQuotientMapMaximalIdeal, Ideal.Quotient.algebraMap_quotient_map_quotient]
18186
rw [← IsScalarTower.algebraMap_apply, ← IsScalarTower.algebraMap_apply]
18287

18388
open nonZeroDivisors in
@@ -210,14 +115,14 @@ lemma Algebra.trace_quotient_eq_of_isDedekindDomain (x) [IsDedekindDomain R] [Is
210115
· have := (IsDedekindDomain.isDedekindDomainDvr R).2 p hp inferInstance
211116
infer_instance
212117
haveI : Module.Free Rₚ Sₚ := Module.free_of_finite_type_torsion_free'
213-
apply (equivQuotMaximalIdealOfIsLocalization p Rₚ).injective
118+
apply (equivQuotMaximalIdeal p Rₚ).injective
214119
rw [trace_quotient_eq_trace_localization_quotient S p Rₚ Sₚ, IsScalarTower.algebraMap_eq S Sₚ,
215120
RingHom.comp_apply, Ideal.Quotient.algebraMap_eq, Algebra.trace_quotient_mk,
216121
RingEquiv.apply_symm_apply, ← Algebra.intTrace_eq_trace,
217122
← Algebra.intTrace_eq_of_isLocalization R S p.primeCompl (Aₘ := Rₚ) (Bₘ := Sₚ) x,
218123
← Ideal.Quotient.algebraMap_eq, ← IsScalarTower.algebraMap_apply]
219-
simp only [equivQuotMaximalIdealOfIsLocalization, RingHom.quotientKerEquivOfSurjective,
220-
RingEquiv.coe_trans, Function.comp_apply, Ideal.quotEquivOfEq_mk,
221-
RingHom.quotientKerEquivOfRightInverse.apply, RingHom.kerLift_mk]
124+
simp only [equivQuotMaximalIdeal, RingHom.quotientKerEquivOfSurjective, RingEquiv.coe_trans,
125+
Function.comp_apply, Ideal.quotEquivOfEq_mk, RingHom.quotientKerEquivOfRightInverse.apply,
126+
RingHom.kerLift_mk]
222127

223128
end IsDedekindDomain

0 commit comments

Comments
 (0)