awayToSection_apply — Mathlib

English

The denominator not mem condition implies the ideal is not top.

Русский

Условие denom_notMem влечет, что I ≠ ⊤.

LaTeX

$$$\text{denom\_notMem}(f_{deg},hm,q) \Rightarrow I \neq \top$$$

Lean4

theorem awayToSection_apply (f : A) (x p) :
    (((ProjectiveSpectrum.Proj.awayToSection 𝒜 f).1 x).val p).val =
      IsLocalization.map (M := Submonoid.powers f) (T := p.1.1.toIdeal.primeCompl) _ (RingHom.id _)
        (Submonoid.powers_le.mpr p.2) x.val :=
  by
  obtain ⟨x, rfl⟩ := HomogeneousLocalization.mk_surjective x
  change (HomogeneousLocalization.mapId 𝒜 _ _).val = _
  dsimp [HomogeneousLocalization.mapId, HomogeneousLocalization.map]
  rw [Localization.mk_eq_mk', Localization.mk_eq_mk', IsLocalization.map_mk']
  rfl

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