NYLL
Module

SubalgebraPrime.lean

Nyll.SchemeTheory.RingTheory.Localization.SubalgebraPrime
13 declarations indexed from sourceView source ↗

Module documentation

Native subalgebra-prime localization maps with closed coefficient squares

The ring objects are the actual native prime localizations. Their coefficient maps are the native algebra maps, retained as RingHoms. The localization map is Localization.localRingHom; its native coefficient equation is proved in the ring-only scope before specializing to a subalgebra.

The subalgebra base maps are the literal composites of these coefficient maps with the original algebra maps. Their proved square mentions only the computed RingHoms. No comparison, localization compatibility, alternate algebra dictionary, or independent local model is assumed.

Imports8
  • Mathlib.Algebra.Algebra.Hom
  • Mathlib.Algebra.Algebra.Subalgebra.Basic
  • Mathlib.Algebra.Category.Ring.Basic
  • Mathlib.Algebra.Category.CommAlgCat.Basic
  • Mathlib.Algebra.Algebra.Tower
  • Mathlib.Algebra.Ring.Hom.Defs
  • Mathlib.RingTheory.Ideal.Maps
  • Mathlib.RingTheory.Localization.AtPrime.Basic
Imported by5

Declarations

def

primeLocalizationCommRingCat

L37 ↗
SchemeTheory.primeLocalizationCommRingCat
Documentation

The actual native prime localization, bundled with its native ring.

Source context 3 commands

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

noncomputable section
namespace SchemeTheory
universe u v
Lean source · statement
def primeLocalizationCommRingCat (C : Type v) [CommRing C]
    (Q : Ideal C) [Q.IsPrime] : CommRingCat.{v}
def

primeLocalizationComapCommRingCat

L43 ↗
SchemeTheory.primeLocalizationComapCommRingCat
Documentation

The actual native localization at the contracted prime. The comap-prime proof is constructed here, rather than requested from a caller.

Source context 3 commands

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

noncomputable section
namespace SchemeTheory
universe u v
Lean source · statement
def primeLocalizationComapCommRingCat
    {R : Type u} {C : Type v} [CommRing R] [CommRing C]
    (f : R →+* C) (Q : Ideal C) [Q.IsPrime] : CommRingCat.{u}
def

primeLocalizationCoefficientMap

L50 ↗
SchemeTheory.primeLocalizationCoefficientMap
Documentation

The native coefficient map into the actual prime localization.

Source context 3 commands

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

noncomputable section
namespace SchemeTheory
universe u v
Lean source · statement
def primeLocalizationCoefficientMap (C : Type v) [CommRing C]
    (Q : Ideal C) [Q.IsPrime] : C →+* primeLocalizationCommRingCat C Q
def

primeLocalizationComapCoefficientMap

L55 ↗
SchemeTheory.primeLocalizationComapCoefficientMap
Documentation

The native coefficient map into the actual contracted-prime localization.

Source context 3 commands

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

noncomputable section
namespace SchemeTheory
universe u v
Lean source · statement
def primeLocalizationComapCoefficientMap
    {R : Type u} {C : Type v} [CommRing R] [CommRing C]
    (f : R →+* C) (Q : Ideal C) [Q.IsPrime] :
    R →+* primeLocalizationComapCommRingCat f Q
def

primeLocalizationComapMap

L63 ↗
SchemeTheory.primeLocalizationComapMap
Documentation

The actual map between the native prime localizations.

Source context 3 commands

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

noncomputable section
namespace SchemeTheory
universe u v
Lean source · statement
def primeLocalizationComapMap
    {R : Type u} {C : Type v} [CommRing R] [CommRing C]
    (f : R →+* C) (Q : Ideal C) [Q.IsPrime] :
    primeLocalizationComapCommRingCat f Q →+* primeLocalizationCommRingCat C Q
theorem

primeLocalizationComapMap_comp_coefficient

L72 ↗
SchemeTheory.primeLocalizationComapMap_comp_coefficient
Documentation

The native localization coefficient equation, with both coefficient maps retained as the actual constructed RingHoms in its public statement.

Source context 3 commands

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

noncomputable section
namespace SchemeTheory
universe u v
Lean source · statement
theorem primeLocalizationComapMap_comp_coefficient
    {R : Type u} {C : Type v} [CommRing R] [CommRing C]
    (f : R →+* C) (Q : Ideal C) [Q.IsPrime] :
    (primeLocalizationComapMap f Q).comp (primeLocalizationComapCoefficientMap f Q) =
      (primeLocalizationCoefficientMap C Q).comp f
def

primeLocalizationBaseMap

L83 ↗
SchemeTheory.primeLocalizationBaseMap
Documentation

The original base-ring map into the actual ambient prime localization.

Source context 3 commands

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

noncomputable section
namespace SchemeTheory
universe u v
Lean source · statement
def primeLocalizationBaseMap (A : Type u) (C : Type v)
    [CommRing A] [CommRing C] [Algebra A C]
    (Q : Ideal C) [Q.IsPrime] : A →+* primeLocalizationCommRingCat C Q
def

subalgebraPrimeLocalizationSource

L92 ↗
SchemeTheory.subalgebraPrimeLocalizationSource
Documentation

The source is exactly the native localization of the actual subalgebra at the contraction of the original prime.

Source context 4 commands

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

noncomputable section
namespace SchemeTheory
universe u v
variable {A : Type u} {C : Type v} [CommRing A] [CommRing C] [Algebra A C]
Lean source · statement
def subalgebraPrimeLocalizationSource (S : Subalgebra A C)
    (Q : Ideal C) [Q.IsPrime] : CommRingCat.{v}
def

subalgebraPrimeLocalizationMap

L97 ↗
SchemeTheory.subalgebraPrimeLocalizationMap
Documentation

The literal localized inclusion of the actual subalgebra.

Source context 4 commands

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

noncomputable section
namespace SchemeTheory
universe u v
variable {A : Type u} {C : Type v} [CommRing A] [CommRing C] [Algebra A C]
Lean source · statement
def subalgebraPrimeLocalizationMap (S : Subalgebra A C)
    (Q : Ideal C) [Q.IsPrime] :
    subalgebraPrimeLocalizationSource S Q →+* primeLocalizationCommRingCat C Q
def

subalgebraPrimeLocalizationBaseMap

L103 ↗
SchemeTheory.subalgebraPrimeLocalizationBaseMap
Documentation

The original base-ring map into the actual subalgebra localization.

Source context 4 commands

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

noncomputable section
namespace SchemeTheory
universe u v
variable {A : Type u} {C : Type v} [CommRing A] [CommRing C] [Algebra A C]
Lean source · statement
def subalgebraPrimeLocalizationBaseMap (S : Subalgebra A C)
    (Q : Ideal C) [Q.IsPrime] : A →+* subalgebraPrimeLocalizationSource S Q
theorem

subalgebraPrimeLocalizationMap_comp_base

L109 ↗
SchemeTheory.subalgebraPrimeLocalizationMap_comp_base
Documentation

The literal subalgebra localization map preserves the original base map. Its public equation contains only the computed native RingHoms.

Source context 4 commands

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

noncomputable section
namespace SchemeTheory
universe u v
variable {A : Type u} {C : Type v} [CommRing A] [CommRing C] [Algebra A C]
Lean source · statement
theorem subalgebraPrimeLocalizationMap_comp_base
    (S : Subalgebra A C) (Q : Ideal C) [Q.IsPrime] :
    (subalgebraPrimeLocalizationMap S Q).comp (subalgebraPrimeLocalizationBaseMap S Q) =
      primeLocalizationBaseMap A C Q
def

subalgebraPrimeLocalizationAlgebra

L137 ↗
SchemeTheory.subalgebraPrimeLocalizationAlgebra
Documentation

The same actual source localization with its native coefficient algebra. No alternate algebra action is installed.

Source context 4 commands

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

noncomputable section
namespace SchemeTheory
universe u v
variable {A : Type u} {C : Type v} [CommRing A] [CommRing C] [Algebra A C]
Lean source · statement
def subalgebraPrimeLocalizationAlgebra (S : Subalgebra A C)
    (Q : Ideal C) [Q.IsPrime] : CommAlgCat.{v} A
theorem

subalgebraPrimeLocalizationBaseMap_eq_algebraMap

L144 ↗
SchemeTheory.subalgebraPrimeLocalizationBaseMap_eq_algebraMap
Documentation

The computed coefficient composite is the native base-algebra map on that exact localization, by the existing native scalar tower.

Source context 4 commands

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

noncomputable section
namespace SchemeTheory
universe u v
variable {A : Type u} {C : Type v} [CommRing A] [CommRing C] [Algebra A C]
Lean source · statement
theorem subalgebraPrimeLocalizationBaseMap_eq_algebraMap
    (S : Subalgebra A C) (Q : Ideal C) [Q.IsPrime] :
    (subalgebraPrimeLocalizationBaseMap S Q :
        A →+* subalgebraPrimeLocalizationAlgebra S Q) =
      algebraMap A (subalgebraPrimeLocalizationAlgebra S Q)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.