Theorems · Definition · commutative algebra

Localization.mapToFractionRing

{A : Type u_1} →
  (K : Type u_2) →
    [inst : CommRing A] →
      (S : Submonoid A) →
        [inst_1 : CommRing K] →
          [inst_2 : Algebra A K] →
            [IsFractionRing A K] →
              (B : Type u_3) →
                [inst_4 : CommRing B] →
                  [inst_5 : Algebra A B] → [IsLocalization S B] → S ≤ nonZeroDivisors A → B →ₐ[A] K

The canonical map from a localization of A at S to the fraction ring of A, given that S ≤ A⁰.

Defined in

Mathlib.RingTheory.Localization.AsSubring

Cited by

5 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraIsFractionRingCommRingAlgebraIsLocalization