English
If a perfect pairing over a field L takes values in a subfield K along K-subspaces whose L-span is top, there exists a finite basis transformation aligning the K-structure with the L-structure.
Русский
Если совершенное парирование над полем L принимает значения в подполе K вдоль подпространств над K, чья L-область порождает всю систему, существует база, переводящая структуру K в структуру L.
LaTeX
$$exists_basis_basis_of_span_eq_top_of_mem_algebraMap$$
Lean4
/-- Simultaneously restrict both the domains and scalars of a perfect pairing with coefficients in a
field. -/
theorem restrictScalars_of_field (hij : p.IsPerfectCompl (span L <| LinearMap.range i) (span L <| LinearMap.range j))
(hp : ∀ m n, p (i m) (j n) ∈ (algebraMap K L).range) :
(LinearMap.restrictScalarsRange₂ i j (Algebra.linearMap K L) (FaithfulSMul.algebraMap_injective K L) p
hp).IsPerfPair :=
by
have : (p.compl₁₂ (span L <| .range i).subtype (span L <| .range j).subtype).IsPerfPair :=
.restrict _ _ _ (by simp) (by simp) (by simpa)
exact
restrictScalars_field_aux (p.compl₁₂ (span L <| .range i).subtype (span L <| .range j).subtype)
((LinearMap.range i).inclusionSpan L ∘ₗ i.rangeRestrict) ((LinearMap.range j).inclusionSpan L ∘ₗ j.rangeRestrict)
(((LinearMap.range i).injective_inclusionSpan L).comp (by simpa))
(((LinearMap.range j).injective_inclusionSpan L).comp (by simpa))
(by
rw [LinearMap.range_comp_of_range_eq_top _ (LinearMap.range_rangeRestrict _)]
exact (LinearMap.range i).span_range_inclusionSpan L)
(by
rw [LinearMap.range_comp_of_range_eq_top _ (LinearMap.range_rangeRestrict _)]
exact (LinearMap.range j).span_range_inclusionSpan L)
fun x y ↦
LinearMap.BilinMap.apply_apply_mem_of_mem_span (LinearMap.range <| Algebra.linearMap K L) (range i) (range j)
((LinearMap.restrictScalarsₗ K L _ _ _).comp (p.restrictScalars K)) (by simpa) (i x) (j y)
(subset_span <| by simp) (subset_span <| by simp)
