English
The coordinate map (repr) of the constructed K-basis agrees with the coordinate map of the original ℤ-basis on L.
Русский
Координатная карта (repr) у построенной K-базы совпадает с координатной картой исходной ℤ-базы на L.
LaTeX
$$$\\text{repr}_{(b.\\text{ofZLatticeBasis})}(x) = \\text{repr}_{b}(x) \\quad (x\\in L)$$$
Lean4
@[simp]
theorem ofZLatticeBasis_repr_apply (x : L) (i : ι) : (b.ofZLatticeBasis K L).repr x i = b.repr x i :=
by
suffices
((b.ofZLatticeBasis K L).repr.toLinearMap.restrictScalars ℤ) ∘ₗ L.subtype =
Finsupp.mapRange.linearMap (Algebra.linearMap ℤ K) ∘ₗ b.repr.toLinearMap
by exact DFunLike.congr_fun (LinearMap.congr_fun this x) i
refine Basis.ext b fun i ↦ ?_
simp_rw [LinearMap.coe_comp, Function.comp_apply, LinearMap.coe_restrictScalars, LinearEquiv.coe_coe, coe_subtype, ←
b.ofZLatticeBasis_apply K, repr_self, Finsupp.mapRange.linearMap_apply, Finsupp.mapRange_single,
Algebra.linearMap_apply, map_one]
