Theorems · Theorem · commutative algebra

IsLocalization.AtPrime.coe_orderIsoOfPrime_symm_apply_coe

∀ {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 : { p // p.IsPrime ∧ p ≤ I }),
  ↑↑((RelIso.symm (IsLocalization.AtPrime.orderIsoOfPrime S I)) a) =
    ⋂ s,
      ⋂ (_ :
        ↑↑((OrderIso.setCongr (fun p => p.IsPrime ∧ Disjoint ↑I.primeCompl ↑p) (fun p => p.IsPrime ∧ p ≤ I) ⋯).symm a) ⊆
          ⇑(algebraMap R S) ⁻¹' ↑s),
        ↑s

Defined in

Mathlib.RingTheory.Localization.AtPrime.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiringAlgebraIdeal.IsPrimeIsLocalization.AtPrime