AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_ringHom_extend_of_isAlgClosed.ChevalleyHom.mem_dom_of_hom
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_ringHom_extend_of_isAlgClosed
namespace ChevalleyHom
variable {L Ω : Type*} [Field L] [Field Ω]
section Extend
variable {Γ₀ Γ : Subring (L × Ω)} (hmax : Maximal (· ∈ Above Γ₀) Γ)
include hmax
open IsGraph Polynomial in
Lean source · full declarationtheorem mem_dom_of_hom [IsAlgClosed Ω] (z : L) {F : Type*} [Field F]
(θ : Polynomial (dom Γ) →+* F)
(hθm : haveI := isLocalRing hmax; ∀ b ∈ IsLocalRing.maximalIdeal (dom Γ), θ (C b) = 0)
(hθz : ∀ p : Polynomial (dom Γ), aeval z p = 0 → θ p = 0) :
z ∈ dom Γ := by
classical
have := isLocalRing hmax
have hΓ := isGraph_of_maximal hmax
let B := dom Γ
let m := IsLocalRing.maximalIdeal B
let k := B ⧸ m
let : Field k := Ideal.Quotient.field m
let π : Polynomial B →+* Polynomial k := mapRingHom (Ideal.Quotient.mk m)
have hπ : Function.Surjective π := map_surjective _ Ideal.Quotient.mk_surjective
let ev : Polynomial B →+* L := (aeval z : Polynomial B →ₐ[B] L).toRingHom
let K₀ : Ideal (Polynomial B) := RingHom.ker ev
let Jk : Ideal (Polynomial k) := K₀.map π
have hθker : ∀ q, π q = 0 → θ q = 0 := by
intro q hq
have hq' : q ∈ RingHom.ker π := hq
rw [ker_mapRingHom, Ideal.mk_ker] at hq'
have hle : Ideal.map (C : B →+* Polynomial B) m ≤ RingHom.ker θ :=
Ideal.map_le_iff_le_comap.mpr fun b hb => Ideal.mem_comap.mpr (RingHom.mem_ker.mpr (hθm b hb))
exact hle hq'
have hJk : Jk ≠ ⊤ := by
intro htop
have h1 : (1 : Polynomial k) ∈ Jk := htop ▸ Submodule.mem_top
obtain ⟨q, hq, hq1⟩ := (Ideal.mem_map_iff_of_surjective π hπ).mp h1
have hq0 : θ q = 0 := hθz q hq
have h1q : θ (1 - q) = 0 := hθker _ (by rw [map_sub, map_one, hq1, sub_self])
rw [map_sub, map_one, hq0, sub_zero] at h1q
exact one_ne_zero h1q
obtain ⟨h, hh⟩ := (IsPrincipalIdealRing.principal Jk).principal
have hhu : ¬ IsUnit h := fun hu => hJk (by
rw [hh, Ideal.submodule_span_eq, Ideal.span_singleton_eq_top]
exact hu)
have hker : ∀ b ∈ m, hΓ.hom b = 0 := fun b hb => (mem_maximalIdeal_iff hmax b).mp hb
let ι : k →+* Ω := Ideal.Quotient.lift m hΓ.hom hker
obtain ⟨ω, hω⟩ : ∃ ω : Ω, (h.map ι).eval ω = 0 := by
by_cases h0 : h = 0
· exact ⟨0, by simp [h0]⟩
· have hdeg : (h.map ι).degree ≠ 0 := by
rw [degree_map]
exact fun hd => hhu (isUnit_iff_degree_eq_zero.mpr hd)
obtain ⟨ω, hω⟩ := IsAlgClosed.exists_root (h.map ι) hdeg
exact ⟨ω, hω⟩
let G : Polynomial B →+* Ω := eval₂RingHom (ι.comp (Ideal.Quotient.mk m)) ω
have hG : ∀ q ∈ K₀, G q = 0 := by
intro q hq
have hπq : π q ∈ Jk := Ideal.mem_map_of_mem π hq
rw [hh, Ideal.submodule_span_eq, Ideal.mem_span_singleton] at hπq
obtain ⟨r, hr⟩ := hπq
have : G q = (π q).eval₂ ι ω := by
simp only [G, π, coe_eval₂RingHom, coe_mapRingHom, eval₂_map]
rw [this, hr, eval₂_mul, ← eval_map, hω, zero_mul]
let S : Subring L := ev.range
let e := RingHom.quotientKerEquivRange ev
let g' : S →+* Ω := (Ideal.Quotient.lift K₀ G hG).comp e.symm.toRingHom
have hg' : ∀ q : Polynomial B, g' ⟨ev q, ⟨q, rfl⟩⟩ = G q := by
intro q
have he : e (Ideal.Quotient.mk K₀ q) = ⟨ev q, ⟨q, rfl⟩⟩ := rfl
change (Ideal.Quotient.lift K₀ G hG) (e.symm ⟨ev q, ⟨q, rfl⟩⟩) = G q
rw [← he, RingEquiv.symm_apply_apply, Ideal.Quotient.lift_mk]
let Γ' : Subring (L × Ω) := (S.subtype.prod g').range
have hΓ' : IsGraph Γ' := by
rintro a ⟨s, hs⟩
simp only [RingHom.prod_apply, Prod.mk.injEq, Subring.coe_subtype] at hs
obtain ⟨hs1, hs2⟩ := hs
have : s = 0 := Subtype.ext hs1
rw [← hs2, this, map_zero]
have evC : ∀ b : B, ev (C b) = (b : L) := fun b => by
change aeval z (C b) = (b : L)
rw [aeval_C]
rfl
have hle : Γ ≤ Γ' := by
rintro ⟨x, a⟩ hxa
have hx : x ∈ B := mem_dom.mpr ⟨a, hxa⟩
have hmemS : x ∈ S := ⟨C ⟨x, hx⟩, evC ⟨x, hx⟩⟩
refine ⟨⟨x, hmemS⟩, ?_⟩
simp only [RingHom.prod_apply, Prod.mk.injEq, Subring.coe_subtype, true_and]
have h1 : g' ⟨x, hmemS⟩ = G (C ⟨x, hx⟩) := by
have h2 := hg' (C ⟨x, hx⟩)
have h3 : (⟨ev (C ⟨x, hx⟩), ⟨C ⟨x, hx⟩, rfl⟩⟩ : S) = ⟨x, hmemS⟩ := Subtype.ext (evC ⟨x, hx⟩)
rw [h3] at h2
exact h2
rw [h1]
simp only [G, coe_eval₂RingHom, eval₂_C, RingHom.comp_apply]
change ι (Ideal.Quotient.mk m ⟨x, hx⟩) = a
rw [Ideal.Quotient.lift_mk]
exact hΓ.hom_eq_of_mem hxa
have heq := eq_of_le hmax Γ' hΓ' hle
have evX : ev X = z := by change aeval z (X : Polynomial B) = z; exact aeval_X z
have hz : ((z, g' ⟨z, ⟨X, evX⟩⟩) : L × Ω) ∈ Γ' := ⟨⟨z, ⟨X, evX⟩⟩, rfl⟩
rw [heq] at hz
exact mem_dom.mpr ⟨_, hz⟩