NYLL
Module

PrincipalProductEtale.lean

Nyll.SchemeTheory.RingTheory.Localization.PrincipalProductEtale
20 declarations indexed from sourceView source ↗

Module documentation

Etaleness of the actual principal-product transition

The transition is the existing native principal map from R_f to R_(f*d). Its etaleness is proved through the actual second principal localization of R_f. The product-localization equivalence and its coefficient equation are established before introducing another coefficient base.

Imports13
Imported by1

Declarations

theorem

ringHom_etale_comp

L38 ↗
SchemeTheory.ringHom_etale_comp
Documentation

Etale ring homomorphisms compose without identifying the universes of the coefficient, intermediate, and target rings.

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 ringHom_etale_comp {R : Type u} {S : Type v} {T : Type w}
    [CommRing R] [CommRing S] [CommRing T]
    (f : R →+* S) (g : S →+* T) (hf : f.Etale) (hg : g.Etale) :
    (g.comp f).Etale
def

nativePrincipalAlgebra

L48 ↗
SchemeTheory.nativePrincipalAlgebra
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 nativePrincipalAlgebra (R : Type u) [CommRing R] (f : R) :
    CommAlgCat.{u} R
theorem

nativePrincipalAlgebra_isLocalization

L52 ↗
SchemeTheory.nativePrincipalAlgebra_isLocalization
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 nativePrincipalAlgebra_isLocalization
    (R : Type u) [CommRing R] (f : R) :
    IsLocalization.Away f (nativePrincipalAlgebra R f)
def

nativePrincipalCoefficient

L57 ↗
SchemeTheory.nativePrincipalCoefficient
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 nativePrincipalCoefficient (R : Type u) [CommRing R] (f : R) :
    R →+* nativePrincipalAlgebra R f
def

nativePrincipalProductAlgebra

L62 ↗
SchemeTheory.nativePrincipalProductAlgebra
Documentation

The literal second localization with its existing native R-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 nativePrincipalProductAlgebra (R : Type u) [CommRing R] (f d : R) :
    CommAlgCat.{u} R
theorem

nativePrincipalProductAlgebra_isLocalization

L70 ↗
SchemeTheory.nativePrincipalProductAlgebra_isLocalization
Documentation

The two native presentations have the same ring and the same original R-action. Only that already constructed action is supplied to the native two-stage localization theorem.

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 nativePrincipalProductAlgebra_isLocalization
    (R : Type u) [CommRing R] (f d : R) :
    IsLocalization.Away (f * d) (nativePrincipalProductAlgebra R f d)
def

nativePrincipalProductAlgEquiv

L83 ↗
SchemeTheory.nativePrincipalProductAlgEquiv
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 nativePrincipalProductAlgEquiv (R : Type u) [CommRing R] (f d : R) :
    nativePrincipalProductAlgebra R f d ≃ₐ[R] nativePrincipalAlgebra R (f * d)
def

nativePrincipalProductEquiv

L92 ↗
SchemeTheory.nativePrincipalProductEquiv
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 nativePrincipalProductEquiv (R : Type u) [CommRing R] (f d : R) :
    nativePrincipalProductAlgebra R f d ≃+* nativePrincipalAlgebra R (f * d)
def

nativePrincipalProductCoefficient

L96 ↗
SchemeTheory.nativePrincipalProductCoefficient
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 nativePrincipalProductCoefficient (R : Type u) [CommRing R] (f d : R) :
    nativePrincipalAlgebra R f →+* nativePrincipalProductAlgebra R f d
theorem

nativePrincipalProductCoefficient_comp_base

L101 ↗
SchemeTheory.nativePrincipalProductCoefficient_comp_base
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 nativePrincipalProductCoefficient_comp_base
    (R : Type u) [CommRing R] (f d : R) :
    (nativePrincipalProductCoefficient R f d).comp (nativePrincipalCoefficient R f) =
      commAlgCoefficientMap (nativePrincipalProductAlgebra R f d)
theorem

nativePrincipalProductEquiv_comp_base

L108 ↗
SchemeTheory.nativePrincipalProductEquiv_comp_base
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 nativePrincipalProductEquiv_comp_base
    (R : Type u) [CommRing R] (f d : R) :
    (nativePrincipalProductEquiv R f d).toRingHom.comp
        (commAlgCoefficientMap (nativePrincipalProductAlgebra R f d)) =
      nativePrincipalCoefficient R (f * d)
theorem

nativePrincipalProductCoefficient_etale

L115 ↗
SchemeTheory.nativePrincipalProductCoefficient_etale
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 nativePrincipalProductCoefficient_etale
    (R : Type u) [CommRing R] (f d : R) :
    (nativePrincipalProductCoefficient R f d).Etale
def

commAlgPrincipalProductMap

L126 ↗
SchemeTheory.commAlgPrincipalProductMap
Documentation

The actual constructed native transition to the product denominator.

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 commAlgPrincipalProductMap {A : Type u} [CommRing A]
    (R : CommAlgCat.{v} A) (f d : R) :
    commAlgPrincipalLocalization R f →+* commAlgPrincipalLocalization R (f * d)
theorem

commAlgPrincipalProductMap_comp_coefficient

L132 ↗
SchemeTheory.commAlgPrincipalProductMap_comp_coefficient
Documentation

The product transition retains the original native coefficient map.

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 commAlgPrincipalProductMap_comp_coefficient {A : Type u} [CommRing A]
    (R : CommAlgCat.{v} A) (f d : R) :
    (commAlgPrincipalProductMap R f d).comp (commAlgPrincipalCoefficientMap R f) =
      commAlgPrincipalCoefficientMap R (f * d)
theorem

nativePrincipalProductMap_eq

L140 ↗
SchemeTheory.nativePrincipalProductMap_eq
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 nativePrincipalProductMap_eq
    (R : Type u) [CommRing R] (f d : R) :
    commAlgPrincipalProductMap (CommAlgCat.of R R) f d =
      (nativePrincipalProductEquiv R f d).toRingHom.comp
        (nativePrincipalProductCoefficient R f d)
theorem

nativePrincipalProductMap_etale

L166 ↗
SchemeTheory.nativePrincipalProductMap_etale
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 nativePrincipalProductMap_etale
    (R : Type u) [CommRing R] (f d : R) :
    (commAlgPrincipalProductMap (CommAlgCat.of R R) f d).Etale
theorem

commAlgPrincipalProductMap_etale

L176 ↗
SchemeTheory.commAlgPrincipalProductMap_etale
Documentation

The native principal-product transition is etale. The proof uses the original R-only nested-localization equivalence, with no new A-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
theorem commAlgPrincipalProductMap_etale {A : Type u} [CommRing A]
    (R : CommAlgCat.{v} A) (f d : R) :
    (commAlgPrincipalProductMap R f d).Etale
theorem

commAlgPrincipalProductMap_comp_base

L183 ↗
SchemeTheory.commAlgPrincipalProductMap_comp_base
Documentation

The product transition preserves the original base coefficient map. This square follows from the native localization coefficient equations.

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 commAlgPrincipalProductMap_comp_base {A : Type u} [CommRing A]
    (R : CommAlgCat.{v} A) (f d : R) :
    (commAlgPrincipalProductMap R f d).comp
        (commAlgCoefficientMap (commAlgPrincipalLocalization R f)) =
      commAlgCoefficientMap (commAlgPrincipalLocalization R (f * d))
theorem

commAlgPrincipalProductCoefficient_etale

L196 ↗
SchemeTheory.commAlgPrincipalProductCoefficient_etale
Documentation

Refining a proved principal etale neighborhood by a product preserves etaleness of its actual original-base coefficient map. The heterogeneous ring-map composition theorems retain independent base and carrier universes.

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 commAlgPrincipalProductCoefficient_etale {A : Type u} [CommRing A]
    (R : CommAlgCat.{v} A) (f d : R)
    (hf : (commAlgCoefficientMap (commAlgPrincipalLocalization R f)).Etale) :
    (commAlgCoefficientMap (commAlgPrincipalLocalization R (f * d))).Etale
theorem

commAlgPrincipalProduct_etale

L207 ↗
SchemeTheory.commAlgPrincipalProduct_etale
Documentation

The product refinement is etale for the original stored A-action. The input is the already proved etaleness of the chosen principal stage.

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 commAlgPrincipalProduct_etale {A : Type u} [CommRing A]
    (R : CommAlgCat.{v} A) (f d : R)
    (hf : Algebra.Etale A (commAlgPrincipalLocalization R f)) :
    Algebra.Etale A (commAlgPrincipalLocalization R (f * d))

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