discr_eq_discr_of_algEquiv — Mathlib

English

If f is a ℚ-algebra equivalence between K and L, then discr K equals discr L.

Русский

Если f — эквивалентность ℚ-алгебр между K и L, то discr K = discr L.

LaTeX

$$$$\\operatorname{discr} K = \\operatorname{discr} L$$$$

Lean4

theorem discr_eq_discr_of_algEquiv {L : Type*} [Field L] [NumberField L] (f : K ≃ₐ[ℚ] L) : discr K = discr L :=
  by
  let f₀ : 𝓞 K ≃ₗ[ℤ] 𝓞 L := (f.restrictScalars ℤ).mapIntegralClosure.toLinearEquiv
  rw [← Rat.intCast_inj, coe_discr, Algebra.discr_eq_discr_of_algEquiv (integralBasis K) f, ←
    discr_eq_discr L ((RingOfIntegers.basis K).map f₀)]
  change _ = algebraMap ℤ ℚ _
  rw [← Algebra.discr_localizationLocalization ℤ (nonZeroDivisors ℤ) L]
  congr 1
  ext
  simp only [Function.comp_apply, integralBasis_apply, Basis.localizationLocalization_apply, Basis.map_apply]
  rfl

Похожие утверждения