instIsFractionRingQuotientIdealResidueField

English

For a prime ideal I, the residue field I.ResidueField is the fraction field of R/I.

Русский

Для простого идеала I поле остатка I.ResidueField является полем дробей над R/I.

LaTeX

$$$\forall \{R\} [\mathrm{CommRing}\ R] \{I : \mathrm{Ideal}\ R\} [I.\mathrm{IsPrime}],\; \mathrm{IsFractionRing}(R/\!I)\ I.\mathrm{ResidueField}$$$

Lean4

instance : IsFractionRing (R ⧸ I) I.ResidueField
    where
  map_units
    y := isUnit_iff_ne_zero.mpr (map_ne_zero_of_mem_nonZeroDivisors _ I.injective_algebraMap_quotient_residueField y.2)
  surj
    x := by
    obtain ⟨x, rfl⟩ := IsLocalRing.residue_surjective x
    obtain ⟨x, ⟨s, hs⟩, rfl⟩ := IsLocalization.mk'_surjective I.primeCompl x
    refine ⟨⟨Ideal.Quotient.mk _ x, ⟨Ideal.Quotient.mk _ s, ?_⟩⟩, ?_⟩
    · rwa [mem_nonZeroDivisors_iff_ne_zero, ne_eq, Ideal.Quotient.eq_zero_iff_mem]
    · simp [IsScalarTower.algebraMap_eq R (Localization.AtPrime I) I.ResidueField, ← map_mul]
  exists_of_eq {x y}
    e := by
    obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
    obtain ⟨y, rfl⟩ := Ideal.Quotient.mk_surjective y
    rw [← sub_eq_zero, ← map_sub, ← map_sub] at e
    simp only [IsLocalRing.ResidueField.algebraMap_eq, IsLocalRing.residue_eq_zero_iff,
      IsScalarTower.algebraMap_apply R (Localization.AtPrime I) I.ResidueField, algebraMap_mk,
      IsLocalization.AtPrime.to_map_mem_maximal_iff _ I, ← Ideal.Quotient.mk_eq_mk_iff_sub_mem] at e
    use 1
    simp [e]

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