Module

AwayAlgebra.lean

Nyll.SchemeTheory.RingTheory.Localization.AwayAlgebra

2 declarations indexed from sourceView source ↗

Module documentation

Principal localization as a commutative algebra

Bundles localization away from an element as a commutative algebra over the coefficient ring and proves its localization witness.

Imports3

Mathlib.Algebra.Category.CommAlgCat.Basic
Mathlib.RingTheory.Localization.Away.Basic
Mathlib.RingTheory.OreLocalization.Ring

Imported by8

def

localizationAwayCommAlgCat

L28 ↗

SchemeTheory.localizationAwayCommAlgCat

Documentation

The principal localization with its native commutative ring and coefficient algebra, bundled once as a commutative algebra. The constructor works with abstract ring inputs before specializing to normalization stages.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace SchemeTheory
universe u w

Lean source · statement

def localizationAwayCommAlgCat (A : Type u) (R : Type w)
    [CommRing A] [CommRing R] [Algebra A R] (f : R) : CommAlgCat.{w} A

theorem

localizationAwayCommAlgCat_isLocalization

L36 ↗

SchemeTheory.localizationAwayCommAlgCat_isLocalization