bijective_algebraMap_quotient_residueField

English

If I is maximal, the canonical map from R/I to I.ResidueField is an isomorphism.

Русский

Если I максимален, каноническое отображение R/I в I.ResidueField является изоморфизмом.

LaTeX

$$$\forall {R} [\mathrm{CommRing}\ R] (I : \mathrm{Ideal}\ R) [I.\mathrmIsMaximal],\\\; \operatorname{algebraMap}(R/\!I)\ I.\mathrmResidueField \text{ is bijective}$$$

Lean4

theorem bijective_algebraMap_quotient_residueField (I : Ideal R) [I.IsMaximal] :
    Function.Bijective (algebraMap (R ⧸ I) I.ResidueField) :=
  ⟨I.injective_algebraMap_quotient_residueField,
    IsFractionRing.surjective_iff_isField.mpr ((Quotient.maximal_ideal_iff_isField_quotient I).mp inferInstance)⟩

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