English
Restriction of scalars yields a root system and maintains the root/ coroot span properties.
Русский
Ограничение скаляров порождает корневую систему и сохраняет свойства оболочек корня/короя.
LaTeX
$$RootPairing.restrictScalars' ...$$
Lean4
/-- Restriction of scalars for a root pairing taking values in a subfield.
Note that we obtain a root system (not just a root pairing). See also
`RootPairing.restrictScalars`. -/
def restrictScalars' : RootSystem ι K (span K (range P.root)) (span K (range P.coroot))
where
toLinearMap :=
.restrictScalarsRange₂ (R := L) (span K (range P.root)).subtype (span K (range P.coroot)).subtype
(Algebra.linearMap K L) (FaithfulSMul.algebraMap_injective K L) P.toLinearMap fun x y ↦
LinearMap.BilinMap.apply_apply_mem_of_mem_span (LinearMap.range (Algebra.linearMap K L)) (range P.root)
(range P.coroot) (LinearMap.restrictScalarsₗ K L _ _ _ ∘ₗ P.toLinearMap.restrictScalars K)
(by rintro - ⟨i, rfl⟩ - ⟨j, rfl⟩; exact hP i j) _ _ x.property y.property
isPerfPair_toLinearMap :=
.restrictScalars_of_field P.toLinearMap _ _ (injective_subtype _) (injective_subtype _)
(by simpa using IsBalanced.isPerfectCompl) _
root := ⟨fun i ↦ ⟨_, subset_span (mem_range_self i)⟩, fun i j h ↦ by simpa using h⟩
coroot := ⟨fun i ↦ ⟨_, subset_span (mem_range_self i)⟩, fun i j h ↦ by simpa using h⟩
root_coroot_two
i := by
have : algebraMap K L 2 = 2 := by rw [← Int.cast_two (R := K), ← Int.cast_two (R := L), map_intCast]
exact FaithfulSMul.algebraMap_injective K L <| by simp [this]
reflectionPerm := P.reflectionPerm
reflectionPerm_root i j := by ext; simpa [algebra_compatible_smul L] using P.reflectionPerm_root i j
reflectionPerm_coroot i j := by ext; simpa [algebra_compatible_smul L] using P.reflectionPerm_coroot i j
span_root_eq_top := by
rw [← span_setOf_mem_eq_top]
congr
ext ⟨x, hx⟩
simp
span_coroot_eq_top := by
rw [← span_setOf_mem_eq_top]
congr
ext ⟨x, hx⟩
simp
