Module

NormalizationLocalizationAction.lean

Nyll.EtaleFundamentalGroups.Inertia.NormalizationLocalizationAction

6 declarations indexed from sourceView source ↗

Module documentation

Geometric-point stabilizers under arbitrary affine localization

The algebra automorphism on the localized cover is constructed from the original automorphism by the localization universal property. The cartesian normalization square then lifts each compatible geometric point, preserving its exact stabilizer. No smoothness or finite-presentation condition is used.

Imports4

Nyll.EtaleFundamentalGroups.Inertia.NormalizationLocalization
Nyll.EtaleFundamentalGroups.Inertia.AffineNormalizationGeometricPoint
Mathlib.RingTheory.Localization.Basic
Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs

Imported by1

Nyll.EtaleFundamentalGroups.Inertia.All

theorem

algebraMapSubmonoid_map_algEquiv

L36 ↗

EtaleFundamentalGroups.Inertia.algebraMapSubmonoid_map_algEquiv

Documentation

An algebra automorphism fixes the multiplicative set coming from the base.

Source context 8 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace EtaleFundamentalGroups.Inertia
universe u
section LocalizationAutomorphism
variable (R B Bm : Type u) [CommRing R] [CommRing B] [CommRing Bm]
variable [Algebra R B] [Algebra B Bm] [Algebra R Bm] [IsScalarTower R B Bm]
variable (M : Submonoid R) [IsLocalization (Algebra.algebraMapSubmonoid B M) Bm]

Lean source · statement

theorem algebraMapSubmonoid_map_algEquiv (sigma : B ≃ₐ[R] B) :
    (Algebra.algebraMapSubmonoid B M).map sigma.toMonoidHom =
      Algebra.algebraMapSubmonoid B M

def

localizationBaseAlgEquiv

L47 ↗

EtaleFundamentalGroups.Inertia.localizationBaseAlgEquiv

Documentation

Extend the actual cover automorphism to the localization.

Source context 8 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace EtaleFundamentalGroups.Inertia
universe u
section LocalizationAutomorphism
variable (R B Bm : Type u) [CommRing R] [CommRing B] [CommRing Bm]
variable [Algebra R B] [Algebra B Bm] [Algebra R Bm] [IsScalarTower R B Bm]
variable (M : Submonoid R) [IsLocalization (Algebra.algebraMapSubmonoid B M) Bm]

Lean source · statement

def localizationBaseAlgEquiv (sigma : B ≃ₐ[R] B) : Bm ≃ₐ[R] Bm

theorem

localizationBaseAlgEquiv_algebraMap

L51 ↗

EtaleFundamentalGroups.Inertia.localizationBaseAlgEquiv_algebraMap

Source context 8 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace EtaleFundamentalGroups.Inertia
universe u
section LocalizationAutomorphism
variable (R B Bm : Type u) [CommRing R] [CommRing B] [CommRing Bm]
variable [Algebra R B] [Algebra B Bm] [Algebra R Bm] [IsScalarTower R B Bm]
variable (M : Submonoid R) [IsLocalization (Algebra.algebraMapSubmonoid B M) Bm]

Lean source · statement

theorem localizationBaseAlgEquiv_algebraMap
    (sigma : B ≃ₐ[R] B) (b : B) :
    localizationBaseAlgEquiv R B Bm M sigma (algebraMap B Bm b) =
      algebraMap B Bm (sigma b)

def

localizationAlgEquiv

L71 ↗

EtaleFundamentalGroups.Inertia.localizationAlgEquiv

Documentation

The extended automorphism is linear over the localized base as well.

Source context 11 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace EtaleFundamentalGroups.Inertia
universe u
variable (R B Rm Bm : Type u)
variable [CommRing R] [CommRing B] [CommRing Rm] [CommRing Bm]
variable [Algebra R B] [Algebra R Rm] [Algebra B Bm]
variable [Algebra Rm Bm] [Algebra R Bm]
variable [IsScalarTower R B Bm] [IsScalarTower R Rm Bm]
variable (M : Submonoid R) [IsLocalization M Rm]
variable [IsLocalization (Algebra.algebraMapSubmonoid B M) Bm]

Lean source · statement

def localizationAlgEquiv (sigma : B ≃ₐ[R] B) : Bm ≃ₐ[Rm] Bm

theorem

affineNormalizationLocalizationMap_deck

L76 ↗

EtaleFundamentalGroups.Inertia.affineNormalizationLocalizationMap_deck

Documentation

The actual affine normalization map intertwines the extended deck maps.

Source context 11 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace EtaleFundamentalGroups.Inertia
universe u
variable (R B Rm Bm : Type u)
variable [CommRing R] [CommRing B] [CommRing Rm] [CommRing Bm]
variable [Algebra R B] [Algebra R Rm] [Algebra B Bm]
variable [Algebra Rm Bm] [Algebra R Bm]
variable [IsScalarTower R B Bm] [IsScalarTower R Rm Bm]
variable (M : Submonoid R) [IsLocalization M Rm]
variable [IsLocalization (Algebra.algebraMapSubmonoid B M) Bm]

Lean source · statement

theorem affineNormalizationLocalizationMap_deck (sigma : B ≃ₐ[R] B) :
    affineNormalizationDeck Rm Bm (localizationAlgEquiv R B Rm Bm M sigma) ≫
        affineNormalizationLocalizationMap R B Rm Bm =
      affineNormalizationLocalizationMap R B Rm Bm ≫
        affineNormalizationDeck R B sigma

theorem

exists_affineNormalizationLocalizationPoint_fixes_iff

L98 ↗

EtaleFundamentalGroups.Inertia.exists_affineNormalizationLocalizationPoint_fixes_iff

Documentation

A compatible point lifts through the actual normalization localization square, and the lift is fixed precisely by the original fixing automorphisms.

Source context 11 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace EtaleFundamentalGroups.Inertia
universe u
variable (R B Rm Bm : Type u)
variable [CommRing R] [CommRing B] [CommRing Rm] [CommRing Bm]
variable [Algebra R B] [Algebra R Rm] [Algebra B Bm]
variable [Algebra Rm Bm] [Algebra R Bm]
variable [IsScalarTower R B Bm] [IsScalarTower R Rm Bm]
variable (M : Submonoid R) [IsLocalization M Rm]
variable [IsLocalization (Algebra.algebraMapSubmonoid B M) Bm]

Lean source · statement

theorem exists_affineNormalizationLocalizationPoint_fixes_iff
    {T : Scheme.{u}}
    (z : T ⟶ (Spec.map (CommRingCat.ofHom (algebraMap R B))).normalization)
    (y : T ⟶ Spec (.of Rm))
    (hzy : z ≫ (Spec.map (CommRingCat.ofHom (algebraMap R B))).fromNormalization =
      y ≫ Spec.map (CommRingCat.ofHom (algebraMap R Rm))) :
    ∃ q : T ⟶ (Spec.map (CommRingCat.ofHom (algebraMap Rm Bm))).normalization,
      q ≫ affineNormalizationLocalizationMap R B Rm Bm = z ∧
      q ≫ (Spec.map (CommRingCat.ofHom (algebraMap Rm Bm))).fromNormalization = y ∧
      ∀ sigma : B ≃ₐ[R] B,
        q ≫ affineNormalizationDeck Rm Bm
            (localizationAlgEquiv R B Rm Bm M sigma) = q ↔
          z ≫ affineNormalizationDeck R B sigma = z

Module documentation

Geometric-point stabilizers under arbitrary affine localization

Declarations

algebraMapSubmonoid_map_algEquiv

localizationBaseAlgEquiv

localizationBaseAlgEquiv_algebraMap

localizationAlgEquiv

affineNormalizationLocalizationMap_deck

exists_affineNormalizationLocalizationPoint_fixes_iff