AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_mapDomain_eq_ord_div_map_of_primitive.Ws14Port.exists_eq_C_mul_monic_mul_of_valuationSubring
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_mapDomain_eq_ord_div_map_of_primitive
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open Polynomial AlgebraicCurve AlgebraicCurve.RationalFunctionField
namespace Ws14Port
Lean source · full declarationtheorem exists_eq_C_mul_monic_mul_of_valuationSubring
{L : Type*} [Field L] [IsAlgClosed L] {A : ValuationSubring L}
(P : Polynomial A) :
∃ (c : A) (Pint Pout : Polynomial A),
P = Polynomial.C c * Pint * Pout ∧
Pint.Monic ∧
(∀ i : ℕ, Pout.coeff i - (if i = 0 then 1 else 0) ∈ IsLocalRing.maximalIdeal A) ∧
(∀ β ∈ (Pout.map (algebraMap A L)).roots, β ∉ A) ∧
(c ∈ IsLocalRing.maximalIdeal A ↔ ∀ i, P.coeff i ∈ IsLocalRing.maximalIdeal A) := by
classical
have hinj : Function.Injective (algebraMap A L) := fun x y h => Subtype.ext h
set R : Multiset L := (P.map (algebraMap A L)).roots with hRdef
set Rin : Multiset L := R.filter (· ∈ A) with hRin
set Rout : Multiset L := R.filter (fun a => ¬ a ∈ A) with hRout
have hR : R = Rin + Rout := (Multiset.filter_add_not _ R).symm
have hin : ∀ α ∈ Rin, α ∈ A := fun α hα => (Multiset.mem_filter.mp hα).2
have hout : ∀ β ∈ Rout, β ∉ A := fun β hβ => (Multiset.mem_filter.mp hβ).2
set sin : Multiset A := Rin.attach.map fun r => (⟨r.1, hin r.1 r.2⟩ : A) with hsin
set Pint : Polynomial A := (sin.map fun t => X - C t).prod with hPintdef
have hPint_monic : Pint.Monic := monic_multisetProd_X_sub_C sin
have hPint_map : Pint.map (algebraMap A L) = (Rin.map fun a => X - C a).prod := by
rw [hPintdef, Polynomial.map_multiset_prod, Multiset.map_map, hsin, Multiset.map_map]
conv_rhs => rw [← Multiset.attach_map_val' Rin]
refine congrArg _ (Multiset.map_congr rfl fun r _ => ?_)
simp [Polynomial.map_sub, ValuationSubring.algebraMap_apply]
set sout : Multiset A := Rout.attach.map fun r =>
(⟨r.1⁻¹, (ValuationSubring.inv_mem_maximalIdeal_of_not_mem (hout r.1 r.2)).1⟩ : A)
with hsout
have hsout_mem : ∀ t ∈ sout, t ∈ IsLocalRing.maximalIdeal A := by
intro t ht
obtain ⟨r, -, rfl⟩ := Multiset.mem_map.mp ht
exact (ValuationSubring.inv_mem_maximalIdeal_of_not_mem (hout r.1 r.2)).2
set Pout : Polynomial A := (sout.map fun t => 1 - C t * X).prod with hPoutdef
have hPout_map : Pout.map (algebraMap A L) = (Rout.map fun b => (1 : L[X]) - C b⁻¹ * X).prod := by
rw [hPoutdef, Polynomial.map_multiset_prod, Multiset.map_map, hsout, Multiset.map_map]
conv_rhs => rw [← Multiset.attach_map_val' Rout]
refine congrArg _ (Multiset.map_congr rfl fun r _ => ?_)
simp [Polynomial.map_sub, Polynomial.map_mul, ValuationSubring.algebraMap_apply]
have hPout_res : Pout.map (IsLocalRing.residue A) = 1 := by
rw [hPoutdef, Polynomial.map_multiset_prod, Multiset.map_map]
refine Multiset.prod_eq_one fun q hq => ?_
obtain ⟨t, ht, rfl⟩ := Multiset.mem_map.mp hq
have : IsLocalRing.residue A t = 0 := (IsLocalRing.residue_eq_zero_iff t).mpr (hsout_mem t ht)
simp [Polynomial.map_sub, Polynomial.map_mul, this]
set c' : L := (P.map (algebraMap A L)).leadingCoeff * (Rout.map fun b => -b).prod with hc'
have hfac : P.map (algebraMap A L) = C c' * (Pint * Pout).map (algebraMap A L) := by
have hsplit := C_leadingCoeff_mul_prod_multiset_X_sub_C
(IsAlgClosed.splits (P.map (algebraMap A L))).natDegree_eq_card_roots.symm
have hlin : ∀ b ∈ Rout, (X : L[X]) - C b = C (-b) * (1 - C b⁻¹ * X) := by
intro b hb
have hb0 : b ≠ 0 := fun h => hout b hb (h ▸ A.zero_mem)
rw [mul_sub, mul_one, ← mul_assoc, ← C_mul, neg_mul, mul_inv_cancel₀ hb0, C_neg, C_neg,
C_1]
ring
have hRout_prod : (Rout.map fun b => (X : L[X]) - C b).prod
= C (Rout.map fun b => -b).prod * (Rout.map fun b => (1 : L[X]) - C b⁻¹ * X).prod := by
rw [Multiset.map_congr rfl hlin, Multiset.prod_map_mul, map_multiset_prod C, Multiset.map_map]
rfl
conv_lhs => rw [← hsplit, ← hRdef, hR, Multiset.map_add, Multiset.prod_add, hRout_prod]
rw [Polynomial.map_mul, hPint_map, hPout_map, hc', C_mul]
ring
set d : ℕ := Pint.natDegree with hd
set u : A := (Pint * Pout).coeff d with hu
have hu_unit : IsUnit u := by
rw [← IsLocalRing.residue_ne_zero_iff_isUnit, hu, ← Polynomial.coeff_map, Polynomial.map_mul,
hPout_res, mul_one, hd, ← hPint_monic.natDegree_map (IsLocalRing.residue A),
(hPint_monic.map _).coeff_natDegree]
exact one_ne_zero
set c : A := P.coeff d * ↑(hu_unit.unit⁻¹) with hcdef
have hcu : c * u = P.coeff d := by
rw [hcdef, mul_assoc, IsUnit.val_inv_mul, mul_one]
have hc' : algebraMap A L c = c' := by
have h1 : algebraMap A L (P.coeff d) = c' * algebraMap A L u := by
rw [← Polynomial.coeff_map, hfac, Polynomial.coeff_C_mul, Polynomial.coeff_map]
have hu0 : algebraMap A L u ≠ 0 := (map_ne_zero_iff _ hinj).mpr hu_unit.ne_zero
apply mul_right_cancel₀ hu0
rw [← map_mul, hcu, h1]
have hP : P = C c * Pint * Pout := by
apply Polynomial.map_injective (algebraMap A L) hinj
rw [mul_assoc, Polynomial.map_mul, Polynomial.map_C, hc', ← hfac]
refine ⟨c, Pint, Pout, hP, hPint_monic, ?_, ?_, ?_⟩
· intro i
rw [← IsLocalRing.residue_eq_zero_iff, map_sub, sub_eq_zero, ← Polynomial.coeff_map, hPout_res,
Polynomial.coeff_one]
split_ifs <;> simp
· intro β hβ
have heval := (Polynomial.mem_roots'.mp hβ).2
rw [Polynomial.IsRoot.def, hPout_map, Polynomial.eval_multiset_prod, Multiset.map_map,
Multiset.prod_eq_zero_iff] at heval
obtain ⟨b, hb, h0⟩ := Multiset.mem_map.mp heval
have hb0 : b ≠ 0 := fun h => hout b hb (h ▸ A.zero_mem)
simp only [Function.comp_apply, eval_sub, eval_one, eval_mul, eval_C, eval_X] at h0
rw [sub_eq_zero, eq_comm, inv_mul_eq_one₀ hb0] at h0
exact h0 ▸ hout b hb
· constructor
· intro hcm i
rw [hP, mul_assoc, Polynomial.coeff_C_mul]
exact Ideal.mul_mem_right _ _ hcm
· intro hall
rw [hcdef]
exact Ideal.mul_mem_right _ _ (hall d)