NYLL
Module

SubalgebraPreimage.lean

Nyll.SchemeTheory.Normalization.SubalgebraPreimage
26 declarations indexed from sourceView source ↗

Module documentation

Native normalization preimages of subalgebras

The normalization objects and their preimage are constructed from the native carriers and inherited actions. Their ring maps and coefficient equations are established before any fraction-field, Galois, or inertia data appear.

Imports6
  • Mathlib.Algebra.Algebra.Hom
  • Mathlib.Algebra.Algebra.Subalgebra.Basic
  • Mathlib.Algebra.Category.CommAlgCat.Basic
  • Mathlib.Algebra.Ring.Hom.Defs
  • Mathlib.Algebra.Ring.Subsemiring.Basic
  • Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Imported by69

Declarations

def

subalgebraCommAlgCat

L29 ↗
SchemeTheory.subalgebraCommAlgCat
Documentation

A subalgebra with its native ring and coefficient action.

Source context 3 commands

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

noncomputable section
namespace SchemeTheory
universe u v w
Lean source · statement
def subalgebraCommAlgCat {A : Type u} {R : Type v}
    [CommRing A] [CommRing R] [Algebra A R]
    (S : Subalgebra A R) : CommAlgCat.{v} A
def

subalgebraBaseMap

L35 ↗
SchemeTheory.subalgebraBaseMap
Documentation

The native coefficient map, retained as a RingHom.

Source context 3 commands

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

noncomputable section
namespace SchemeTheory
universe u v w
Lean source · statement
def subalgebraBaseMap {A : Type u} {R : Type v}
    [CommRing A] [CommRing R] [Algebra A R]
    (S : Subalgebra A R) : A →+* subalgebraCommAlgCat S
theorem

subalgebraBaseMap_eq_algebraMap

L41 ↗
SchemeTheory.subalgebraBaseMap_eq_algebraMap
Documentation

The base map uses exactly the action in the returned native object.

Source context 3 commands

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

noncomputable section
namespace SchemeTheory
universe u v w
Lean source · statement
theorem subalgebraBaseMap_eq_algebraMap {A : Type u} {R : Type v}
    [CommRing A] [CommRing R] [Algebra A R]
    (S : Subalgebra A R) :
    subalgebraBaseMap S = algebraMap A (subalgebraCommAlgCat S)
def

subalgebraRingMap

L47 ↗
SchemeTheory.subalgebraRingMap
Documentation

The literal subtype inclusion, without opening an algebra on its source.

Source context 3 commands

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

noncomputable section
namespace SchemeTheory
universe u v w
Lean source · statement
def subalgebraRingMap {A : Type u} {R : Type v}
    [CommRing A] [CommRing R] [Algebra A R]
    (S : Subalgebra A R) : subalgebraCommAlgCat S →+* R
theorem

subalgebraRingMap_injective

L53 ↗
SchemeTheory.subalgebraRingMap_injective
Documentation

The native subtype inclusion is injective.

Source context 3 commands

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

noncomputable section
namespace SchemeTheory
universe u v w
Lean source · statement
theorem subalgebraRingMap_injective {A : Type u} {R : Type v}
    [CommRing A] [CommRing R] [Algebra A R]
    (S : Subalgebra A R) : Function.Injective (subalgebraRingMap S).toFun
theorem

subalgebraRingMap_comp_base

L59 ↗
SchemeTheory.subalgebraRingMap_comp_base
Documentation

The subtype inclusion preserves the original coefficients.

Source context 3 commands

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

noncomputable section
namespace SchemeTheory
universe u v w
Lean source · statement
theorem subalgebraRingMap_comp_base {A : Type u} {R : Type v}
    [CommRing A] [CommRing R] [Algebra A R]
    (S : Subalgebra A R) :
    (subalgebraRingMap S).comp (subalgebraBaseMap S) = algebraMap A R
def

subalgebraPreimageCommAlgCat

L71 ↗
SchemeTheory.subalgebraPreimageCommAlgCat
Documentation

The actual preimage subalgebra, with its native coefficient action.

Source context 5 commands

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

noncomputable section
namespace SchemeTheory
universe u v w
section Preimage
variable {A : Type u} {R : Type v} {C : Type w}
    [CommRing A] [CommRing R] [CommRing C] [Algebra A R] [Algebra A C]
Lean source · statement
def subalgebraPreimageCommAlgCat (f : R →ₐ[A] C) (T : Subalgebra A C) :
    CommAlgCat.{v} A
def

subalgebraPreimageRingMap

L76 ↗
SchemeTheory.subalgebraPreimageRingMap
Documentation

The actual restriction of the given map to its preimage.

Source context 5 commands

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

noncomputable section
namespace SchemeTheory
universe u v w
section Preimage
variable {A : Type u} {R : Type v} {C : Type w}
    [CommRing A] [CommRing R] [CommRing C] [Algebra A R] [Algebra A C]
Lean source · statement
def subalgebraPreimageRingMap (f : R →ₐ[A] C) (T : Subalgebra A C) :
    subalgebraPreimageCommAlgCat f T →+* subalgebraCommAlgCat T
def

subalgebraPreimageBaseMap

L81 ↗
SchemeTheory.subalgebraPreimageBaseMap
Documentation

The original coefficients in the actual preimage algebra.

Source context 5 commands

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

noncomputable section
namespace SchemeTheory
universe u v w
section Preimage
variable {A : Type u} {R : Type v} {C : Type w}
    [CommRing A] [CommRing R] [CommRing C] [Algebra A R] [Algebra A C]
Lean source · statement
def subalgebraPreimageBaseMap (f : R →ₐ[A] C) (T : Subalgebra A C) :
    A →+* subalgebraPreimageCommAlgCat f T
theorem

subalgebraPreimageBaseMap_eq_algebraMap

L86 ↗
SchemeTheory.subalgebraPreimageBaseMap_eq_algebraMap
Documentation

The coefficient map is the native algebraMap of the constructed object.

Source context 5 commands

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

noncomputable section
namespace SchemeTheory
universe u v w
section Preimage
variable {A : Type u} {R : Type v} {C : Type w}
    [CommRing A] [CommRing R] [CommRing C] [Algebra A R] [Algebra A C]
Lean source · statement
theorem subalgebraPreimageBaseMap_eq_algebraMap
    (f : R →ₐ[A] C) (T : Subalgebra A C) :
    subalgebraPreimageBaseMap f T =
      algebraMap A (subalgebraPreimageCommAlgCat f T)
theorem

subalgebraPreimageRingMap_comp_coefficient

L93 ↗
SchemeTheory.subalgebraPreimageRingMap_comp_coefficient
Documentation

The restriction square is supplied by the native RingHom restriction.

Source context 5 commands

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

noncomputable section
namespace SchemeTheory
universe u v w
section Preimage
variable {A : Type u} {R : Type v} {C : Type w}
    [CommRing A] [CommRing R] [CommRing C] [Algebra A R] [Algebra A C]
Lean source · statement
theorem subalgebraPreimageRingMap_comp_coefficient
    (f : R →ₐ[A] C) (T : Subalgebra A C) :
    (subalgebraRingMap T).comp (subalgebraPreimageRingMap f T) =
      f.toRingHom.comp (subalgebraRingMap (T.comap f))
theorem

subalgebraPreimageRingMap_comp_base

L101 ↗
SchemeTheory.subalgebraPreimageRingMap_comp_base
Documentation

The preimage ring map preserves the original base map. All equations used here are supplied by the native maps; no compatibility is assumed.

Source context 5 commands

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

noncomputable section
namespace SchemeTheory
universe u v w
section Preimage
variable {A : Type u} {R : Type v} {C : Type w}
    [CommRing A] [CommRing R] [CommRing C] [Algebra A R] [Algebra A C]
Lean source · statement
theorem subalgebraPreimageRingMap_comp_base
    (f : R →ₐ[A] C) (T : Subalgebra A C) :
    (subalgebraPreimageRingMap f T).comp (subalgebraPreimageBaseMap f T) =
      subalgebraBaseMap T
def

normalizationCommAlgCat

L133 ↗
SchemeTheory.normalizationCommAlgCat
Documentation

The actual normalization in the ambient algebra.

Source context 3 commands

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

noncomputable section
namespace SchemeTheory
universe u v w
Lean source · statement
def normalizationCommAlgCat (A : Type u) (L : Type v)
    [CommRing A] [CommRing L] [Algebra A L] : CommAlgCat.{v} A
def

subalgebraNormalizationCommAlgCat

L142 ↗
SchemeTheory.subalgebraNormalizationCommAlgCat
Documentation

Construct the actual normalization inside the given subalgebra before exposing it as an object to later preimage constructions.

Source context 4 commands

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

noncomputable section
namespace SchemeTheory
universe u v w
variable {A : Type u} {L : Type v}
    [CommRing A] [CommRing L] [Algebra A L]
Lean source · statement
def subalgebraNormalizationCommAlgCat (S : Subalgebra A L) : CommAlgCat.{v} A
def

subalgebraNormalizationMap

L146 ↗
SchemeTheory.subalgebraNormalizationMap
Documentation

The native normalization map induced by the literal subtype inclusion.

Source context 4 commands

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

noncomputable section
namespace SchemeTheory
universe u v w
variable {A : Type u} {L : Type v}
    [CommRing A] [CommRing L] [Algebra A L]
Lean source · statement
def subalgebraNormalizationMap (S : Subalgebra A L) :
    subalgebraNormalizationCommAlgCat S →ₐ[A] normalizationCommAlgCat A L
def

subalgebraNormalizationRingMap

L151 ↗
SchemeTheory.subalgebraNormalizationRingMap
Documentation

The same actual normalization inclusion, retained as a RingHom.

Source context 4 commands

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

noncomputable section
namespace SchemeTheory
universe u v w
variable {A : Type u} {L : Type v}
    [CommRing A] [CommRing L] [Algebra A L]
Lean source · statement
def subalgebraNormalizationRingMap (S : Subalgebra A L) :
    subalgebraNormalizationCommAlgCat S →+* normalizationCommAlgCat A L
theorem

subalgebraNormalizationRingMap_comp_base

L156 ↗
SchemeTheory.subalgebraNormalizationRingMap_comp_base
Documentation

The normalization inclusion preserves the native coefficient maps.

Source context 4 commands

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

noncomputable section
namespace SchemeTheory
universe u v w
variable {A : Type u} {L : Type v}
    [CommRing A] [CommRing L] [Algebra A L]
Lean source · statement
theorem subalgebraNormalizationRingMap_comp_base (S : Subalgebra A L) :
    (subalgebraNormalizationRingMap S).comp
        (algebraMap A (subalgebraNormalizationCommAlgCat S)) =
      algebraMap A (normalizationCommAlgCat A L)
def

normalizationPreimageCommAlgCat

L163 ↗
SchemeTheory.normalizationPreimageCommAlgCat
Documentation

The actual preimage in the native subalgebra normalization.

Source context 4 commands

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

noncomputable section
namespace SchemeTheory
universe u v w
variable {A : Type u} {L : Type v}
    [CommRing A] [CommRing L] [Algebra A L]
Lean source · statement
def normalizationPreimageCommAlgCat (S : Subalgebra A L)
    (T : Subalgebra A (normalizationCommAlgCat A L)) : CommAlgCat.{v} A
def

normalizationPreimageRingMap

L169 ↗
SchemeTheory.normalizationPreimageRingMap
Documentation

The literal inclusion of the normalization preimage into the given upper subalgebra, exposed without opening the preimage coefficient action.

Source context 4 commands

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

noncomputable section
namespace SchemeTheory
universe u v w
variable {A : Type u} {L : Type v}
    [CommRing A] [CommRing L] [Algebra A L]
Lean source · statement
def normalizationPreimageRingMap (S : Subalgebra A L)
    (T : Subalgebra A (normalizationCommAlgCat A L)) :
    normalizationPreimageCommAlgCat S T →+* subalgebraCommAlgCat T
def

normalizationPreimageBaseMap

L175 ↗
SchemeTheory.normalizationPreimageBaseMap
Documentation

The original coefficient map in the actual normalization preimage.

Source context 4 commands

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

noncomputable section
namespace SchemeTheory
universe u v w
variable {A : Type u} {L : Type v}
    [CommRing A] [CommRing L] [Algebra A L]
Lean source · statement
def normalizationPreimageBaseMap (S : Subalgebra A L)
    (T : Subalgebra A (normalizationCommAlgCat A L)) :
    A →+* normalizationPreimageCommAlgCat S T
theorem

normalizationPreimageRingMap_comp_base

L181 ↗
SchemeTheory.normalizationPreimageRingMap_comp_base
Documentation

The actual preimage RingHom satisfies its original coefficient square.

Source context 4 commands

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

noncomputable section
namespace SchemeTheory
universe u v w
variable {A : Type u} {L : Type v}
    [CommRing A] [CommRing L] [Algebra A L]
Lean source · statement
theorem normalizationPreimageRingMap_comp_base (S : Subalgebra A L)
    (T : Subalgebra A (normalizationCommAlgCat A L)) :
    (normalizationPreimageRingMap S T).comp (normalizationPreimageBaseMap S T) =
      subalgebraBaseMap T
theorem

normalizationPreimageBaseMap_eq_algebraMap

L188 ↗
SchemeTheory.normalizationPreimageBaseMap_eq_algebraMap
Documentation

The preimage base map is the native algebraMap on the actual object.

Source context 4 commands

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

noncomputable section
namespace SchemeTheory
universe u v w
variable {A : Type u} {L : Type v}
    [CommRing A] [CommRing L] [Algebra A L]
Lean source · statement
theorem normalizationPreimageBaseMap_eq_algebraMap (S : Subalgebra A L)
    (T : Subalgebra A (normalizationCommAlgCat A L)) :
    normalizationPreimageBaseMap S T =
      algebraMap A (normalizationPreimageCommAlgCat S T)
theorem

subalgebraCommAlgCat_isDomain

L196 ↗
SchemeTheory.subalgebraCommAlgCat_isDomain
Documentation

The native subalgebra object retains the canonical domain property of its ambient ring. Only the existing Prop instance is exposed.

Source context 4 commands

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

noncomputable section
namespace SchemeTheory
universe u v w
variable {A : Type u} {L : Type v}
    [CommRing A] [CommRing L] [Algebra A L]
Lean source · statement
theorem subalgebraCommAlgCat_isDomain {A : Type u} {R : Type v}
    [CommRing A] [CommRing R] [IsDomain R] [Algebra A R]
    (S : Subalgebra A R) : IsDomain (subalgebraCommAlgCat S)
theorem

subalgebraPreimageRingMap_injective

L204 ↗
SchemeTheory.subalgebraPreimageRingMap_injective
Documentation

The actual preimage restriction retains injectivity of the given coefficient map. The proof uses its already proved restriction square.

Source context 4 commands

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

noncomputable section
namespace SchemeTheory
universe u v w
variable {A : Type u} {L : Type v}
    [CommRing A] [CommRing L] [Algebra A L]
Lean source · statement
theorem subalgebraPreimageRingMap_injective
    {A : Type u} {R : Type v} {C : Type w}
    [CommRing A] [CommRing R] [CommRing C] [Algebra A R] [Algebra A C]
    (f : R →ₐ[A] C) (T : Subalgebra A C)
    (hf : Function.Injective f.toRingHom.toFun) :
    Function.Injective (subalgebraPreimageRingMap f T).toFun
theorem

subalgebraNormalizationRingMap_injective

L221 ↗
SchemeTheory.subalgebraNormalizationRingMap_injective
Documentation

The literal normalization inclusion is injective by its two subtype projections. No field, fraction-ring, or Galois hypothesis is needed.

Source context 4 commands

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

noncomputable section
namespace SchemeTheory
universe u v w
variable {A : Type u} {L : Type v}
    [CommRing A] [CommRing L] [Algebra A L]
Lean source · statement
theorem subalgebraNormalizationRingMap_injective (S : Subalgebra A L) :
    Function.Injective (subalgebraNormalizationRingMap S).toFun
theorem

normalizationPreimageRingMap_injective

L230 ↗
SchemeTheory.normalizationPreimageRingMap_injective
Documentation

The actual normalization preimage embeds into the given upper subalgebra, using the native normalization injection just proved.

Source context 4 commands

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

noncomputable section
namespace SchemeTheory
universe u v w
variable {A : Type u} {L : Type v}
    [CommRing A] [CommRing L] [Algebra A L]
Lean source · statement
theorem normalizationPreimageRingMap_injective (S : Subalgebra A L)
    (T : Subalgebra A (normalizationCommAlgCat A L)) :
    Function.Injective (normalizationPreimageRingMap S T).toFun

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