AlgebraicCurves.Places.Proofs.Place_eq_of_comap_toValuationSubring_eq_of_isRational.RationalPlaceDescent.exists_mem_span_div
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_eq_of_comap_toValuationSubring_eq_of_isRational
noncomputable section
open AlgebraicCurve
namespace RationalPlaceDescent
section RegionF
Lean source · full declarationtheorem exists_mem_span_div {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
[Algebra K F] [Algebra K' F'] [Algebra F F']
(hgen : IntermediateField.adjoin K' (Set.range (algebraMap F F')) = ⊤) (V : Place K F) (g : F')
:
∃ b ∈ Submodule.span K' (Set.range (fun f : V.toValuationSubring => algebraMap F F' (f : F))),
∃ b' ∈ Submodule.span K' (Set.range (fun f : V.toValuationSubring => algebraMap F F' (f :
F))),
b' ≠ 0 ∧ g = b / b' := by
have hmul := mul_mem_span_range_of_mem (K' := K') (F' := F') V
have h1S : (1 : F') ∈
Submodule.span K' (Set.range (fun f : V.toValuationSubring => algebraMap F F' (f : F))) :=
Submodule.subset_span ⟨1, by simp⟩
have hg : g ∈ IntermediateField.adjoin K' (Set.range (algebraMap F F')) := by
rw [hgen]
exact IntermediateField.mem_top
change g ∈ Subfield.closure (Set.range (algebraMap K' F') ∪ Set.range (algebraMap F F')) at hg
induction hg using Subfield.closure_induction with
| mem y hy =>
rcases hy with ⟨c, rfl⟩ | ⟨f, rfl⟩
· refine ⟨algebraMap K' F' c, ?_, 1, h1S, one_ne_zero, (div_one _).symm⟩
rw [Algebra.algebraMap_eq_smul_one]
exact Submodule.smul_mem _ c h1S
· by_cases hf : f ∈ V.toValuationSubring
· exact ⟨algebraMap F F' f, Submodule.subset_span ⟨⟨f, hf⟩, rfl⟩, 1, h1S, one_ne_zero,
(div_one _).symm⟩
· have hf0 : f ≠ 0 := fun h0 => hf (h0 ▸ zero_mem _)
have hfi : f⁻¹ ∈ V.toValuationSubring := (V.toValuationSubring.mem_or_inv_mem
f).resolve_left hf
refine ⟨1, h1S, algebraMap F F' f⁻¹, Submodule.subset_span ⟨⟨f⁻¹, hfi⟩, rfl⟩,
(map_ne_zero (algebraMap F F')).mpr (inv_ne_zero hf0), ?_⟩
rw [map_inv₀, one_div, inv_inv]
| one => exact ⟨1, h1S, 1, h1S, one_ne_zero, (div_one 1).symm⟩
| add x y _ _ hx hy =>
obtain ⟨b, hb, b', hb', hb'0, rfl⟩ := hx
obtain ⟨c, hc, c', hc', hc'0, rfl⟩ := hy
exact ⟨b * c' + b' * c, add_mem (hmul b hb c' hc') (hmul b' hb' c hc), b' * c', hmul b' hb'
c' hc',
mul_ne_zero hb'0 hc'0, div_add_div b c hb'0 hc'0⟩
| neg x _ hx =>
obtain ⟨b, hb, b', hb', hb'0, rfl⟩ := hx
exact ⟨-b, neg_mem hb, b', hb', hb'0, by ring⟩
| inv x _ hx =>
obtain ⟨b, hb, b', hb', hb'0, rfl⟩ := hx
by_cases hb0 : b = 0
· subst hb0
exact ⟨0, zero_mem _, 1, h1S, one_ne_zero, by simp⟩
· exact ⟨b', hb', b, hb, hb0, by rw [inv_div]⟩
| mul x y _ _ hx hy =>
obtain ⟨b, hb, b', hb', hb'0, rfl⟩ := hx
obtain ⟨c, hc, c', hc', hc'0, rfl⟩ := hy
exact ⟨b * c, hmul b hb c hc, b' * c', hmul b' hb' c' hc', mul_ne_zero hb'0 hc'0,
by rw [div_mul_div_comm]⟩