English
If K is totally complex, then a specific discriminant bound implies the ring of integers is a PID.
Русский
Если K полностью комплексно, то по определённому ограничению дискриминант кольцо целых является ПИД.
LaTeX
$$$[IsTotallyComplex K] \Rightarrow \mathrm{abs\_discr\_ge'}(K) \Rightarrow \mathrm{IsPrincipalIdealRing}(\mathcal{O}_K)$$$
Lean4
theorem _root_.NumberField.mixedEmbedding.volume_fundamentalDomain_latticeBasis :
volume (fundamentalDomain (latticeBasis K)) = (2 : ℝ≥0∞)⁻¹ ^ nrComplexPlaces K * sqrt ‖discr K‖₊ :=
by
let f : Module.Free.ChooseBasisIndex ℤ (𝓞 K) ≃ (K →+* ℂ) :=
(canonicalEmbedding.latticeBasis K).indexEquiv (Pi.basisFun ℂ _)
let e : (index K) ≃ Module.Free.ChooseBasisIndex ℤ (𝓞 K) := (indexEquiv K).trans f.symm
let M := (mixedEmbedding.stdBasis K).toMatrix ((latticeBasis K).reindex e.symm)
let N := Algebra.embeddingsMatrixReindex ℚ ℂ (integralBasis K ∘ f.symm) RingHom.equivRatAlgHom
suffices M.map ofRealHom = matrixToStdBasis K * (Matrix.reindex (indexEquiv K).symm (indexEquiv K).symm N).transpose
by
calc
volume (fundamentalDomain (latticeBasis K))
_ = ‖((mixedEmbedding.stdBasis K).toMatrix ((latticeBasis K).reindex e.symm)).det‖₊ :=
by
rw [← fundamentalDomain_reindex _ e.symm, ← norm_toNNReal,
measure_fundamentalDomain ((latticeBasis K).reindex e.symm), volume_fundamentalDomain_stdBasis, mul_one]
rfl
_ = ‖(matrixToStdBasis K).det * N.det‖₊ := by
rw [← nnnorm_real, ← ofRealHom_eq_coe, RingHom.map_det, RingHom.mapMatrix_apply, this, det_mul, det_transpose,
det_reindex_self]
_ = (2 : ℝ≥0∞)⁻¹ ^ Fintype.card { w : InfinitePlace K // IsComplex w } * sqrt ‖N.det ^ 2‖₊ :=
by
have : ‖Complex.I‖₊ = 1 := by rw [← norm_toNNReal, norm_I, Real.toNNReal_one]
rw [det_matrixToStdBasis, nnnorm_mul, nnnorm_pow, nnnorm_mul, this, mul_one, nnnorm_inv, coe_mul,
ENNReal.coe_pow, ← norm_toNNReal, RCLike.norm_two, Real.toNNReal_ofNat, coe_inv two_ne_zero, coe_ofNat,
nnnorm_pow, NNReal.sqrt_sq]
_ = (2 : ℝ≥0∞)⁻¹ ^ Fintype.card { w // IsComplex w } * NNReal.sqrt ‖discr K‖₊ := by
rw [← Algebra.discr_eq_det_embeddingsMatrixReindex_pow_two, Algebra.discr_reindex, ← coe_discr, map_intCast, ←
Complex.nnnorm_intCast]
ext : 2
dsimp only [M]
rw [Matrix.map_apply, Basis.toMatrix_apply, Basis.coe_reindex, Function.comp_apply, Equiv.symm_symm,
latticeBasis_apply, ← commMap_canonical_eq_mixed, Complex.ofRealHom_eq_coe,
stdBasis_repr_eq_matrixToStdBasis_mul K _ (fun _ => rfl)]
rfl
