Theorems · Theorem · commutative algebra

IsLocalization.AtPrime.coe_primeSpectrumOrderIso_symm_apply_asIdeal

∀ {R : Type u_1} [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (I : Ideal R)
  [hI : I.IsPrime] [inst_3 : IsLocalization.AtPrime S I] (a : ↑(Set.Iic { asIdeal := I, isPrime := hI })),
  ↑((RelIso.symm (IsLocalization.AtPrime.primeSpectrumOrderIso S I)) a).asIdeal =
    ⋂ s,
      ⋂ (_ :
        ↑↑((OrderIso.setCongr (fun p => p.IsPrime ∧ Disjoint ↑I.primeCompl ↑p) (fun p => p.IsPrime ∧ p ≤ I) ⋯).symm
                ⟨(↑a).asIdeal, ⋯⟩) ⊆
          ⇑(algebraMap R S) ⁻¹' ↑s),
        ↑s

Defined in

Mathlib.RingTheory.Localization.AtPrime.Basic

Cited by

0 results in Mathlib

Foundations

Depth 89 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringCommSemiringAlgebraIdeal.IsPrimeIsLocalization.AtPrime