English
The matrix representing commMap on stdBasis is diagonal with a standard 2×2 conjugation block, after reindexing.
Русский
Матрица, представляющая отображение commMap на stdBasis, диагональная с блоком сопряжения 2×2 после перекодирования индексов.
LaTeX
$$$ \text{stdBasis_repr_eq_matrixToStdBasis_mul} $$$
Lean4
theorem latticeBasis_repr_apply (x : K) (i : ChooseBasisIndex ℤ (𝓞 K)) :
(latticeBasis K).repr (mixedEmbedding K x) i = (integralBasis K).repr x i :=
by
rw [← Basis.restrictScalars_repr_apply ℚ _ ⟨_, mem_rat_span_latticeBasis K x⟩, eq_ratCast, Rat.cast_inj]
let f := (mixedEmbedding K).toRatAlgHom.toLinearMap.codRestrict _ (fun x ↦ mem_rat_span_latticeBasis K x)
suffices ((latticeBasis K).restrictScalars ℚ).repr.toLinearMap ∘ₗ f = (integralBasis K).repr.toLinearMap from
DFunLike.congr_fun (LinearMap.congr_fun this x) i
refine Basis.ext (integralBasis K) (fun i ↦ ?_)
have : f (integralBasis K i) = ((latticeBasis K).restrictScalars ℚ) i :=
by
apply Subtype.val_injective
rw [LinearMap.codRestrict_apply, AlgHom.toLinearMap_apply, Basis.restrictScalars_apply, latticeBasis_apply]
rfl
simp_rw [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, this, Basis.repr_self]
