AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_valuation_mul_eq_one_of_finrank_le_card.ValuationSubring.CompleteSplittingE.card_add_card_le_finrank
Source context 13 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_exists_valuation_mul_eq_one_of_finrank_le_card
namespace ValuationSubring
open _root_.ValuationSubring
namespace CompleteSplittingE
open _root_.ValuationSubring
open IsLocalRing
variable {F F' : Type*} [Field F] [Field F'] [Algebra F F']
section Residue
variable (R : ValuationSubring F')
attribute [local instance] residueAlgebra
variable {R}
Lean source · full declarationtheorem card_add_card_le_finrank [FiniteDimensional F F']
(S' : Finset (ValuationSubring F'))
(hS' : ∀ P ∈ S', P.comap (algebraMap F F') = R.comap (algebraMap F F')) (hRS' : R ∈ S')
{τ : Type*} [Fintype τ] (clsR : τ → ValuationSubring F') (hclsR : ∀ t, clsR t ∈ S')
(hne : ∀ t, clsR t ≠ R) (ω : τ → F')
(hωlt : ∀ t, ∀ P ∈ S', P ≠ clsR t → P.valuation (ω t) < 1)
(hind : ∀ P ∈ S', ∀ a : τ → F, (∀ t, a t ∈ R.comap (algebraMap F F')) →
(∀ t, clsR t ≠ P → a t = 0) → (∃ t, (R.comap (algebraMap F F')).valuation (a t) = 1) →
P.valuation (∑ t, algebraMap F F' (a t) * ω t) = 1)
(s : Finset (ResidueField ↥R))
(hs : LinearIndependent (ResidueField ↥(R.comap (algebraMap F F')))
(fun i : ↥s => (i : ResidueField ↥R))) :
s.card + Fintype.card τ ≤ Module.finrank F F' := by
classical
set QR := R.comap (algebraMap F F') with hQRdef
have : Algebra.IsAlgebraic F F' := Algebra.IsAlgebraic.of_finite F F'
choose lift hlift using fun i : ↥s => residue_surjective (R := ↥R) (i : ResidueField ↥R)
obtain ⟨x', hx'mem, hx'sub, hx'lt⟩ := exists_normalized QR S' hS' (fun _ : ↥s => R)
(fun _ => hRS') (fun i => (lift i : F')) (fun i => (lift i).2)
have hx'R : ∀ i, x' i ∈ R := fun i => hx'mem i R hRS'
have hres : ∀ i, residue (↥R) ⟨x' i, hx'R i⟩ = (i : ResidueField ↥R) := by
intro i
rw [← hlift i, ← sub_eq_zero, ← map_sub, residue_eq_zero_iff, ← coe_mem_nonunits_iff,
ValuationSubring.mem_nonunits_iff]
exact hx'sub i
set vec : ↥s ⊕ τ → F' := fun o => Sum.elim x' ω o with hvecdef
suffices hli : LinearIndependent F vec by
have := hli.fintype_card_le_finrank
rwa [Fintype.card_sum, Fintype.card_coe] at this
by_contra hdep
obtain ⟨g, hrel, i₁, hi₁⟩ := Fintype.not_linearIndependent_iff.mp hdep
obtain ⟨iM, -, hiM⟩ := Finset.exists_max_image Finset.univ (fun o => QR.valuation (g o))
⟨i₁, Finset.mem_univ _⟩
have hM0 : g iM ≠ 0 := by
intro h
have := hiM i₁ (Finset.mem_univ _)
rw [h, map_zero, le_zero_iff, Valuation.zero_iff] at this
exact hi₁ this
set f : ↥s ⊕ τ → F := fun o => g o / g iM with hfdef
have hfQ : ∀ o, f o ∈ QR := by
intro o
rw [← QR.valuation_le_one_iff, hfdef, map_div₀]
exact div_le_one_of_le₀ (hiM o (Finset.mem_univ _)) zero_le
have hfM : f iM = 1 := div_self hM0
have hfrel : (∑ i, algebraMap F F' (f (Sum.inl i)) * x' i) +
∑ t, algebraMap F F' (f (Sum.inr t)) * ω t = 0 := by
have : ∑ o, f o • vec o = 0 := by
simp only [hfdef, div_eq_mul_inv, mul_comm _ (g iM)⁻¹, ← smul_smul, ← Finset.smul_sum, hrel,
smul_zero]
rw [Fintype.sum_sum_type] at this
simpa only [hvecdef, Sum.elim_inl, Sum.elim_inr, Algebra.smul_def] using this
have hle : ∀ P ∈ S', ∀ o, P.valuation (algebraMap F F' (f o)) ≤ 1 :=
fun P hP o => le_one (hS' P hP) (hfQ o)
rcases hiMcase : iM with i₀ | t₀
· rw [hiMcase] at hfM
have hB : R.valuation (∑ t, algebraMap F F' (f (Sum.inr t)) * ω t) < 1 := by
apply Valuation.map_sum_lt _ one_ne_zero
intro t _
rw [map_mul]
exact mul_lt_one_aux (hle R hRS' _) (hωlt t R hRS' (hne t).symm)
have hA : R.valuation (∑ i, algebraMap F F' (f (Sum.inl i)) * x' i) < 1 := by
rw [eq_neg_of_add_eq_zero_left hfrel, Valuation.map_neg]
exact hB
set fR : ↥s → ↥QR := fun i => ⟨f (Sum.inl i), hfQ _⟩ with hfRdef
set AR : ↥R := ∑ i, resHom R (fR i) * ⟨x' i, hx'R i⟩ with hARdef
have hAcoe : (AR : F') = ∑ i, algebraMap F F' (f (Sum.inl i)) * x' i := by
rw [hARdef, ← R.coe_subtype, map_sum]
rfl
have hAres : residue (↥R) AR = 0 := by
rw [residue_eq_zero_iff, ← coe_mem_nonunits_iff, ValuationSubring.mem_nonunits_iff, hAcoe]
exact hA
have hsum : ∑ i, (residue (↥QR) (fR i)) • (i : ResidueField ↥R) = 0 := by
rw [← hAres, hARdef, map_sum]
refine Finset.sum_congr rfl fun i _ => ?_
rw [map_mul, hres, Algebra.smul_def, algebraMap_residue]
have h1 : residue (↥QR) (fR i₀) = 1 := by
have : fR i₀ = 1 := Subtype.ext hfM
rw [this, map_one]
have := Fintype.linearIndependent_iff.mp hs (fun i => residue (↥QR) (fR i)) hsum i₀
rw [h1] at this
exact one_ne_zero this
· rw [hiMcase] at hfM
set P' := clsR t₀ with hP'def
have hP'S : P' ∈ S' := hclsR t₀
have hA : P'.valuation (∑ i, algebraMap F F' (f (Sum.inl i)) * x' i) < 1 := by
apply Valuation.map_sum_lt _ one_ne_zero
intro i _
rw [map_mul]
exact mul_lt_one_aux (hle P' hP'S _) (hx'lt i P' hP'S (hne t₀))
have hB₁ : P'.valuation
(∑ t, algebraMap F F' (if clsR t = P' then f (Sum.inr t) else 0) * ω t) = 1 := by
refine hind P' hP'S _ (fun t => ?_) (fun t ht => ite_eq_right ht) ⟨t₀, ?_⟩
· split_ifs
· exact hfQ _
· exact ValuationSubring.zero_mem _
· rw [ite_eq_left rfl, hfM, map_one]
have hB₂ : P'.valuation
(∑ t, algebraMap F F' (if clsR t = P' then 0 else f (Sum.inr t)) * ω t) < 1 := by
apply Valuation.map_sum_lt _ one_ne_zero
intro t _
split_ifs with h
· rw [map_zero, zero_mul, map_zero]; exact zero_lt_one
· rw [map_mul]
exact mul_lt_one_aux (hle P' hP'S _) (hωlt t P' hP'S (Ne.symm h))
have hBsplit : ∑ t, algebraMap F F' (f (Sum.inr t)) * ω t =
(∑ t, algebraMap F F' (if clsR t = P' then f (Sum.inr t) else 0) * ω t) +
∑ t, algebraMap F F' (if clsR t = P' then 0 else f (Sum.inr t)) * ω t := by
rw [← Finset.sum_add_distrib]
refine Finset.sum_congr rfl fun t _ => ?_
split_ifs <;> simp
have hB : P'.valuation (∑ t, algebraMap F F' (f (Sum.inr t)) * ω t) = 1 := by
rw [hBsplit, Valuation.map_add_eq_of_lt_left]
· exact hB₁
· rw [hB₁]; exact hB₂
have hAB : P'.valuation ((∑ i, algebraMap F F' (f (Sum.inl i)) * x' i) +
∑ t, algebraMap F F' (f (Sum.inr t)) * ω t) = 1 := by
rw [Valuation.map_add_eq_of_lt_right]
· exact hB
· rw [hB]; exact hA
rw [hfrel, map_zero] at hAB
exact zero_ne_one hAB