Theorems · Definition · commutative algebra

Localization.subalgebra.ofField

{A : Type u_1} →
  (K : Type u_2) →
    [inst : CommRing A] →
      (S : Submonoid A) →
        S ≤ nonZeroDivisors A → [inst_1 : Field K] → [inst_2 : Algebra A K] → [IsFractionRing A K] → Subalgebra A K

Given a domain A with fraction field K, and a submonoid S of A which contains no zero divisor, this is the localization of A at S, considered as a subalgebra of K over A. The carrier of this subalgebra is defined as the set of all x : K of the form algebraMap A K a * (algebraMap A K s)⁻¹ where a s : A and s ∈ S.

Defined in

Mathlib.RingTheory.Localization.AsSubring

Cited by

8 results in Mathlib

Foundations

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

Assumes

CommRingFieldAlgebraIsFractionRing