algebraMap_injective — Mathlib

English

The natural algebra map from F_q[X] into ringOfIntegers Fq F is injective.

Русский

Естественное отображение-algebraMap из F_q[X] в ringOfIntegers Fq F инъективно.

LaTeX

$$$\operatorname{algebraMap}_{F_q[X]}\colon F_q[X] \to \mathrm{ringOfIntegers}_{F_q}F \text{ is injective.}$$$

Lean4

theorem algebraMap_injective : Function.Injective (⇑(algebraMap Fq[X] (ringOfIntegers Fq F))) :=
  by
  have hinj : Function.Injective (⇑(algebraMap Fq[X] F)) :=
    by
    rw [IsScalarTower.algebraMap_eq Fq[X] (RatFunc Fq) F]
    exact (algebraMap (RatFunc Fq) F).injective.comp (IsFractionRing.injective Fq[X] (RatFunc Fq))
  rw [injective_iff_map_eq_zero (algebraMap Fq[X] (↥(ringOfIntegers Fq F)))]
  intro p hp
  rw [← Subtype.coe_inj, Subalgebra.coe_zero] at hp
  rw [injective_iff_map_eq_zero (algebraMap Fq[X] F)] at hinj
  exact hinj p hp

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