English
If a perfect pairing takes values in a subfield and both domain and codomain are restricted compatibly, the restricted map remains a perfect pairing.
Русский
Если совершенное парирование принимает значения в подполе и домен и кодомен ограничиваются совместимо, ограниченная форма остаётся совершенным парированием.
LaTeX
$$restrictScalars_of_field : IsPerfPair$$
Lean4
/-- If a perfect pairing over a field `L` takes values in a subfield `K` along two `K`-subspaces
whose `L` span is full, then these subspaces induce a `K`-structure in the sense of
[*Algebra I*, Bourbaki : Chapter II, §8.1 Definition 1][bourbaki1989]. -/
theorem exists_basis_basis_of_span_eq_top_of_mem_algebraMap (M' : Submodule K M) (N' : Submodule K N)
(hM : span L (M' : Set M) = ⊤) (hN : span L (N' : Set N) = ⊤)
(hp : ∀ᵉ (x ∈ M') (y ∈ N'), p x y ∈ (algebraMap K L).range) :
∃ (n : ℕ) (b : Basis (Fin n) L M) (b' : Basis (Fin n) K M'), ∀ i, b i = b' i := by
classical
have : IsReflexive L M := .of_isPerfPair p
have : IsReflexive L N := .of_isPerfPair p.flip
obtain ⟨v, hv₁, hv₂, hv₃⟩ := exists_linearIndependent L (M' : Set M)
rw [hM] at hv₂
let b : Basis _ L M := Basis.mk hv₃ <| by rw [← hv₂, Subtype.range_coe_subtype, Set.setOf_mem_eq]
have : Fintype v := Set.Finite.fintype <| Module.Finite.finite_basis b
set v' : v → M' := fun i ↦ ⟨i, hv₁ (Subtype.coe_prop i)⟩
have hv' : LinearIndependent K v' :=
by
replace hv₃ :=
hv₃.restrict_scalars (R := K) <| by
simp_rw [← Algebra.algebraMap_eq_smul_one]
exact FaithfulSMul.algebraMap_injective K L
rw [show ((↑) : v → M) = M'.subtype ∘ v' by ext; simp [v']] at hv₃
exact hv₃.of_comp
suffices span K (Set.range v') = ⊤
by
let e := (Module.Finite.finite_basis b).equivFin
let b' : Basis _ K M' := Basis.mk hv' (by rw [this])
exact ⟨_, b.reindex e, b'.reindex e, fun i ↦ by simp [b, b', v']⟩
suffices span K v = M' by
apply Submodule.map_injective_of_injective M'.injective_subtype
rw [Submodule.map_span, ← Set.image_univ, Set.image_image]
simpa [v']
refine le_antisymm (Submodule.span_le.mpr hv₁) fun m hm ↦ ?_
obtain ⟨w, hw₁, hw₂, hw₃⟩ := exists_linearIndependent L (N' : Set N)
rw [hN] at hw₂
let bN : Basis _ L N := Basis.mk hw₃ <| by rw [← hw₂, Subtype.range_coe_subtype, Set.setOf_mem_eq]
have : Fintype w := Set.Finite.fintype <| Module.Finite.finite_basis bN
have e : v ≃ w :=
Fintype.equivOfCardEq <| by
rw [← Module.finrank_eq_card_basis b, ← Module.finrank_eq_card_basis bN, Module.finrank_of_isPerfPair p]
let bM := bN.dualBasis.map p.toPerfPair.symm
have hbM (j : w) (x : M) (hx : x ∈ M') : bM.repr x j = p x (j : N) := by simp [bM, bN]
have hj (j : w) : bM.repr m j ∈ (algebraMap K L).range := (hbM _ _ hm) ▸ hp m hm j (hw₁ j.2)
replace hp (i : w) (j : v) : (bN.dualBasis.map p.toPerfPair.symm).toMatrix b i j ∈ (algebraMap K L).fieldRange :=
by
simp only [Basis.toMatrix, Basis.map_repr, LinearEquiv.symm_symm, LinearEquiv.trans_apply, Basis.dualBasis_repr]
exact hp (b j) (by simpa [b] using hv₁ j.2) (bN i) (by simpa [bN] using hw₁ i.2)
have hA (i j) : b.toMatrix bM i j ∈ (algebraMap K L).range :=
Matrix.mem_subfield_of_mul_eq_one_of_mem_subfield_left e _ (by simp [bM]) hp i j
have h_span : span K v = span K (Set.range b) := by simp [b]
rw [h_span, Basis.mem_span_iff_repr_mem, ← Basis.toMatrix_mulVec_repr bM b m]
exact fun i ↦ Subring.sum_mem _ fun j _ ↦ Subring.mul_mem _ (hA i j) (hj j)
