AlgebraicCurves.FunctionFields.Proofs.FinrankAlong_eq_and_trace_eq_of_constantFieldExtension_of_isAlgClosed.TRGBody.linearIndependent_algebraMap
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs
namespace FinrankAlong_eq_and_trace_eq_of_constantFieldExtension_of_isAlgClosed
open AlgebraicCurve
namespace TRGBody
Lean source · full declarationtheorem linearIndependent_algebraMap
(K F : Type*) [Field K] [Field F] [Algebra K F] [IsAlgClosed K]
(_hfg : ∃ x : F, Transcendental K x ∧
FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
(F' : Type*) [Field F'] [Algebra K F']
(hfg' : ∃ x' : F', Transcendental K x' ∧
FiniteDimensional (IntermediateField.adjoin K ({x'} : Set F')) F')
(φ : F →ₐ[K] F')
(E FE : Type*) [Field E] [Field FE] [Algebra K E] [Algebra E FE] [Algebra F FE] [Algebra K FE]
[IsScalarTower K E FE] [IsScalarTower K F FE]
(_hfgE : ∃ x : FE, Transcendental E x ∧
FiniteDimensional (IntermediateField.adjoin E ({x} : Set FE)) FE)
(hgen : IntermediateField.adjoin E (Set.range (algebraMap F FE)) = ⊤)
(F'E : Type*) [Field F'E] [Algebra E F'E] [Algebra F' F'E] [Algebra K F'E]
[IsScalarTower K E F'E] [IsScalarTower K F' F'E]
(hfgE' : ∃ x' : F'E, Transcendental E x' ∧
FiniteDimensional (IntermediateField.adjoin E ({x'} : Set F'E)) F'E)
(hgen' : IntermediateField.adjoin E (Set.range (algebraMap F' F'E)) = ⊤)
(φE : FE →ₐ[E] F'E) (hφcomm : ∀ f : F, φE (algebraMap F FE f) = algebraMap F' F'E (φ f))
{ι : Type*} (b : ι → F') (hb : letI := algebraAlong φ; LinearIndependent F b) :
letI := algebraAlong φE
LinearIndependent FE (fun i => algebraMap F' F'E (b i)) := by
classical
let iφ : Algebra F F' := algebraAlong φ
have hKFF' : IsScalarTower K F F' := isScalarTower_along φ
let iφE : Algebra FE F'E := algebraAlong φE
have hEFE : IsScalarTower E FE F'E := IsScalarTower.of_algebraMap_eq (fun e => (φE.commutes
e).symm)
let R₀ : Subalgebra F FE := Algebra.adjoin F (Set.range (algebraMap E FE))
have hR₀frac : ∀ z : FE, ∃ x y : R₀, z = algebraMap R₀ FE x / algebraMap R₀ FE y := by
intro z
have hz : z ∈ IntermediateField.adjoin E (Set.range (algebraMap F FE)) := by rw [hgen]; trivial
obtain ⟨r, hr, s, hs, h⟩ := IntermediateField.mem_adjoin_iff_div.mp hz
have hsw : ∀ x, x ∈ Algebra.adjoin E (Set.range (algebraMap F FE)) → x ∈ R₀ := by
intro x hx
rw [← Subalgebra.mem_toSubring, Algebra.adjoin_eq_ring_closure] at hx ⊢
rwa [Set.union_comm]
exact ⟨⟨r, hsw r hr⟩, ⟨s, hsw s hs⟩, h⟩
have : IsFractionRing R₀ FE := IsFractionRing.of_field R₀ FE hR₀frac
rw [← LinearIndependent.iff_fractionRing R₀ FE]
let ε := Module.Free.chooseBasis K E
have hR₀span : ∀ r : R₀, ∃ g : Module.Free.ChooseBasisIndex K E →₀ F,
(r : FE) = g.sum (fun a c => c • algebraMap E FE (ε a)) := by
intro r
have hr : (r : FE) ∈ Subalgebra.toSubmodule R₀ := r.2
rw [Algebra.adjoin_eq_span] at hr
have hcl : ((Submonoid.closure (Set.range (algebraMap E FE)) : Submonoid FE) : Set FE) =
Set.range (algebraMap E FE) := by
have : Set.range (algebraMap E FE) = ((MonoidHom.mrange (algebraMap E FE : E →* FE)) : Set
FE) := by
ext; simp
rw [this, Submonoid.closure_eq]
rw [hcl] at hr
have hle : Submodule.span F (Set.range (algebraMap E FE)) ≤
Submodule.span F (Set.range (fun a => algebraMap E FE (ε a))) := by
rw [Submodule.span_le]
rintro _ ⟨e, rfl⟩
rw [← ε.linearCombination_repr e, Finsupp.linearCombination_apply, map_finsuppSum,
Finsupp.sum]
refine Submodule.sum_mem _ fun a _ => ?_
rw [Algebra.smul_def, map_mul, ← IsScalarTower.algebraMap_apply K E FE,
IsScalarTower.algebraMap_apply K F FE, ← Algebra.smul_def]
exact Submodule.smul_mem _ _ (Submodule.subset_span ⟨a, rfl⟩)
obtain ⟨g, hg⟩ := Finsupp.mem_span_range_iff_exists_finsupp.mp (hle hr)
exact ⟨g, hg.symm⟩
choose g hg using hR₀span
let f₀ : F' →ₐ[K] F'E := IsScalarTower.toAlgHom K F' F'E
let A' : IntermediateField K F'E := f₀.fieldRange
have hmemA' : ∀ x : F', f₀ x ∈ A' := fun x => f₀.mem_fieldRange.mpr ⟨x, rfl⟩
let toA' : F' →ₗ[K] A' :=
{ toFun := fun x => ⟨f₀ x, hmemA' x⟩
map_add' := fun x y => Subtype.ext (map_add f₀ x y)
map_smul' := fun c x => Subtype.ext (by simp) }
have htoA' : Function.Bijective toA' := by
refine ⟨fun x y hxy => f₀.toRingHom.injective (congrArg Subtype.val hxy), fun y => ?_⟩
obtain ⟨x, hx⟩ := f₀.mem_fieldRange.mp y.2
exact ⟨x, Subtype.ext hx⟩
let β := (Module.Free.chooseBasis K F').map (LinearEquiv.ofBijective toA' htoA')
have h73 := AlgebraicCurve.linearIndependent_of_constantFieldExtension_of_isAlgClosed K F' E F'E
hfg' hfgE' hgen' (Module.Free.chooseBasis K F').linearIndependent
have hLD : A'.LinearDisjoint E := by
refine IntermediateField.LinearDisjoint.of_basis_left β ?_
convert h73 using 1
rfl
have hεind : LinearIndependent A' (fun a => algebraMap E F'E (ε a)) :=
hLD.linearIndependent_right' ε.linearIndependent
rw [linearIndependent_iff']
intro s r hrel i hi
let T : Finset (Module.Free.ChooseBasisIndex K E) := s.biUnion (fun j => (g (r j)).support)
let κF : Module.Free.ChooseBasisIndex K E → F' := fun a => ∑ j ∈ s, φ (g (r j) a) * b j
have hexp : ∀ j ∈ s, (r j : FE) = ∑ a ∈ T, g (r j) a • algebraMap E FE (ε a) := by
intro j hj
rw [hg (r j), Finsupp.sum_of_support_subset _ (Finset.subset_biUnion_of_mem (fun j => (g (r
j)).support) hj) _ (fun a _ => by simp)]
have key : ∑ j ∈ s, r j • algebraMap F' F'E (b j) =
∑ a ∈ T, (⟨f₀ (κF a), hmemA' (κF a)⟩ : A') • algebraMap E F'E (ε a) := by
calc ∑ j ∈ s, r j • algebraMap F' F'E (b j)
= ∑ j ∈ s, φE (r j : FE) * algebraMap F' F'E (b j) := by
exact Finset.sum_congr rfl fun j _ => rfl
_ = ∑ j ∈ s, ∑ a ∈ T, algebraMap F' F'E (φ (g (r j) a)) * algebraMap E F'E (ε a) *
algebraMap F' F'E (b j) := by
refine Finset.sum_congr rfl fun j hj => ?_
rw [hexp j hj, map_sum, Finset.sum_mul]
refine Finset.sum_congr rfl fun a _ => ?_
rw [Algebra.smul_def, map_mul, hφcomm, φE.commutes]
_ = ∑ a ∈ T, ∑ j ∈ s, algebraMap F' F'E (φ (g (r j) a)) * algebraMap E F'E (ε a) *
algebraMap F' F'E (b j) := Finset.sum_comm
_ = ∑ a ∈ T, (⟨f₀ (κF a), hmemA' (κF a)⟩ : A') • algebraMap E F'E (ε a) := by
refine Finset.sum_congr rfl fun a _ => ?_
rw [Algebra.smul_def]
change _ = f₀ (κF a) * _
simp only [κF, map_sum, map_mul, Finset.sum_mul]
refine Finset.sum_congr rfl fun j _ => ?_
change _ = algebraMap F' F'E (φ (g (r j) a)) * algebraMap F' F'E (b j) * algebraMap E F'E
(ε a)
ring
rw [key] at hrel
have hκ : ∀ a ∈ T, κF a = 0 := by
intro a ha
have h := linearIndependent_iff'.mp hεind T _ hrel a ha
have h' : f₀ (κF a) = 0 := congrArg Subtype.val h
exact f₀.toRingHom.injective (h'.trans (map_zero _).symm)
have hg0 : ∀ j ∈ s, ∀ a, g (r j) a = 0 := by
intro j hj a
by_cases ha : a ∈ T
· have hsum : ∑ j ∈ s, g (r j) a • b j = 0 := by
have := hκ a ha
simp only [κF] at this
simp only [Algebra.smul_def] at this ⊢
exact this
exact linearIndependent_iff'.mp hb s (fun j => g (r j) a) hsum j hj
· by_contra hne
exact ha (Finset.mem_biUnion.mpr ⟨j, hj, Finsupp.mem_support_iff.mpr hne⟩)
have hri : (r i : FE) = 0 := by
rw [hexp i hi]
exact Finset.sum_eq_zero fun a _ => by rw [hg0 i hi a, zero_smul]
exact Subtype.ext hri