English
A real basis of the mixed space that is simultaneously a Z-basis of the image of 𝓞K is constructed from the lattice basis.
Русский
Реальная база смешанного пространства одновременно является базисом по целым числам образа 𝓞K.
LaTeX
$$$ latticeBasis : Basis (Module.Free.ChooseBasisIndex Int (NumberField.RingOfIntegers K)) Real (NumberField.mixedEmbedding.mixedSpace K) $$$
Lean4
/-- A `ℝ`-basis of the mixed space that is also a `ℤ`-basis of the image of `𝓞 K`. -/
def latticeBasis : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K) := by
classical
-- We construct an `ℝ`-linear independent family from the image of
-- `canonicalEmbedding.lattice_basis` by `commMap`
have :=
LinearIndependent.map
(LinearIndependent.restrict_scalars
(by { simpa only [Complex.real_smul, mul_one] using Complex.ofReal_injective
})
(canonicalEmbedding.latticeBasis K).linearIndependent)
(disjoint_span_commMap_ker K)
-- and it's a basis since it has the right cardinality
refine basisOfLinearIndependentOfCardEqFinrank this ?_
rw [← finrank_eq_card_chooseBasisIndex, RingOfIntegers.rank, finrank_prod, finrank_pi, finrank_pi_fintype,
Complex.finrank_real_complex, sum_const, card_univ, ← nrRealPlaces, ← nrComplexPlaces, ← card_real_embeddings,
Algebra.id.smul_eq_mul, mul_comm, ← card_complex_embeddings, ← NumberField.Embeddings.card K ℂ,
Fintype.card_subtype_compl, Nat.add_sub_of_le (Fintype.card_subtype_le _)]
