English
A ring isomorphism between quotient constructions is established (as in quotAdjoinEquivQuotMap).
Русский
Существует изоморфизм колец между квотами конструированными через adjoin и сопутствующие модули.
LaTeX
$$$\\text{quotAdjoinEquivQuotMap}(hx,h\\_alg): (R / I.map( R )) \\cong+* (S / I.map(R S))$$$
Lean4
/-- The canonical morphism of rings from `R<x> ⧸ (I*R<x>)` to `S ⧸ (I*S)` is an isomorphism
when `I` and `(conductor R x) ∩ R` are coprime. -/
noncomputable def quotAdjoinEquivQuotMap (hx : (conductor R x).comap (algebraMap R S) ⊔ I = ⊤)
(h_alg : Function.Injective (algebraMap R<x> S)) :
R<x> ⧸ I.map (algebraMap R R<x>) ≃+* S ⧸ I.map (algebraMap R S) :=
by
let f : R<x> ⧸ I.map (algebraMap R R<x>) →+* S ⧸ I.map (algebraMap R S) :=
(Ideal.Quotient.lift (I.map (algebraMap R R<x>))
((Ideal.Quotient.mk (I.map (algebraMap R S))).comp (algebraMap R<x> S))
(fun r hr => by
have : algebraMap R S = (algebraMap R<x> S).comp (algebraMap R R<x>) := by ext; rfl
rw [RingHom.comp_apply, Ideal.Quotient.eq_zero_iff_mem, this, ← Ideal.map_map]
exact Ideal.mem_map_of_mem _ hr))
refine RingEquiv.ofBijective f ⟨?_, ?_⟩
· --the kernel of the map is clearly `(I * S) ∩ R<x>`. To get injectivity, we need to show that
--this is contained in `I * R<x>`, which is the content of the previous lemma.
refine RingHom.lift_injective_of_ker_le_ideal _ _ fun u hu => ?_
rwa [RingHom.mem_ker, RingHom.comp_apply, Ideal.Quotient.eq_zero_iff_mem, ← Ideal.mem_comap,
comap_map_eq_map_adjoin_of_coprime_conductor hx h_alg] at hu
· -- Surjectivity follows from the surjectivity of the canonical map `R<x> → S ⧸ (I * S)`,
-- which in turn follows from the fact that `I * S + (conductor R x) = S`.
refine Ideal.Quotient.lift_surjective_of_surjective _ _ fun y => ?_
obtain ⟨z, hz⟩ := Ideal.Quotient.mk_surjective y
have : z ∈ conductor R x ⊔ I.map (algebraMap R S) :=
by
suffices conductor R x ⊔ I.map (algebraMap R S) = ⊤ by simp only [this, Submodule.mem_top]
rw [Ideal.eq_top_iff_one] at hx ⊢
replace hx := Ideal.mem_map_of_mem (algebraMap R S) hx
rw [Ideal.map_sup, RingHom.map_one] at hx
exact
(sup_le_sup
(show ((conductor R x).comap (algebraMap R S)).map (algebraMap R S) ≤ conductor R x from Ideal.map_comap_le)
(le_refl (I.map (algebraMap R S))))
hx
rw [← Ideal.mem_quotient_iff_mem_sup, hz, Ideal.mem_map_iff_of_surjective] at this
· obtain ⟨u, hu, hu'⟩ := this
use ⟨u, conductor_subset_adjoin hu⟩
simp only [← hu']
rfl
· exact Ideal.Quotient.mk_surjective
