Module

NormalizationLocalization.lean

Nyll.EtaleFundamentalGroups.Inertia.NormalizationLocalization

9 declarations indexed from sourceView source ↗

Module documentation

Affine relative normalization and arbitrary localization

Let Rm be the localization of R at M, and let Bm be the localization of an R-algebra B at the image of M. The actual map between integral closures is constructed by mapping integral elements and extending scalars. Mathlib's localization theorem for integral closures makes the resulting square a pushout of rings. Its spectrum is therefore a pullback of schemes.

Using the canonical affine normalization isomorphisms, this gives an actual isomorphism between the relative normalization of Spec Bm → Spec Rm and the pullback of the relative normalization of Spec B → Spec R. The argument allows arbitrary multiplicative sets, including the complement of a prime. It requires no domain, normality, finite-type, or smoothness assumptions. This file treats the affine comparison; it does not claim that the canonical map from a scheme's stalk spectrum is smooth.

Imports5

Nyll.SchemeTheory.Normalization.Affine
Mathlib.Algebra.Category.Ring.Constructions
Mathlib.AlgebraicGeometry.Pullbacks
Mathlib.RingTheory.Localization.Integral
Mathlib.RingTheory.Localization.BaseChange

Imported by4

theorem

specNormalizationIso_hom_structureMap

L42 ↗

EtaleFundamentalGroups.Inertia.specNormalizationIso_hom_structureMap

Documentation

The canonical affine normalization isomorphism also intertwines the maps to the base. This follows from the actual integral-closure inclusion.

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace EtaleFundamentalGroups.Inertia
universe u

Lean source · statement

theorem specNormalizationIso_hom_structureMap
    (R B : Type u) [CommRing R] [CommRing B] [Algebra R B] :
    (specNormalizationIso R B).hom ≫
        Spec.map (CommRingCat.ofHom (algebraMap R (integralClosure R B))) =
      (Spec.map (CommRingCat.ofHom (algebraMap R B))).fromNormalization

def

integralClosureLocalizationMap

L60 ↗

EtaleFundamentalGroups.Inertia.integralClosureLocalizationMap

Documentation

The literal integral-closure map in a localization square. Its definition already makes sense for every compatible square of algebra maps.

Source context 9 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]

Lean source · full declaration

def integralClosureLocalizationMap :
    integralClosure R B →ₐ[R] integralClosure Rm Bm where
  toFun b := ⟨algebraMap B Bm (b : B),
    (b.property.map (IsScalarTower.toAlgHom R B Bm)).tower_top⟩
  map_one' := Subtype.ext (map_one (algebraMap B Bm))
  map_mul' b c := Subtype.ext (map_mul (algebraMap B Bm) (b : B) (c : B))
  map_zero' := Subtype.ext (map_zero (algebraMap B Bm))
  map_add' b c := Subtype.ext (map_add (algebraMap B Bm) (b : B) (c : B))
  commutes' r := by
    apply Subtype.ext
    change algebraMap B Bm (algebraMap R B r) = algebraMap R Bm r
    exact (IsScalarTower.algebraMap_apply R B Bm r).symm

theorem

integralClosureLocalization_isPushout

L81 ↗

EtaleFundamentalGroups.Inertia.integralClosureLocalization_isPushout

Documentation

Integral closure gives a literal pushout square after localizing the base. The algebra structure on the target closure is constructed from the displayed map, and its scalar-tower laws are proved from that map.

Source context 13 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)
variable [IsLocalization M Rm]
variable [IsLocalization (Algebra.algebraMapSubmonoid B M) Bm]
include M

Lean source · statement

theorem integralClosureLocalization_isPushout :
    IsPushout
      (CommRingCat.ofHom (algebraMap R (integralClosure R B)))
      (CommRingCat.ofHom (algebraMap R Rm))
      (CommRingCat.ofHom (integralClosureLocalizationMap R B Rm Bm).toRingHom)
      (CommRingCat.ofHom (algebraMap Rm (integralClosure Rm Bm)))

def

affineNormalizationLocalizationMap

L104 ↗

EtaleFundamentalGroups.Inertia.affineNormalizationLocalizationMap

Documentation

The canonical map from the normalization after localization to the original normalization, expressed through the actual integral-closure map.

Source context 14 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)
variable [IsLocalization M Rm]
variable [IsLocalization (Algebra.algebraMapSubmonoid B M) Bm]
include M
omit M

Lean source · statement

def affineNormalizationLocalizationMap :
    (Spec.map (CommRingCat.ofHom (algebraMap Rm Bm))).normalization ⟶
      (Spec.map (CommRingCat.ofHom (algebraMap R B))).normalization

theorem

toNormalization_affineNormalizationLocalizationMap

L114 ↗

EtaleFundamentalGroups.Inertia.toNormalization_affineNormalizationLocalizationMap

Documentation

The comparison is the canonical extension of the original localization map, as witnessed by its composite with the normalization maps.

Source context 14 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)
variable [IsLocalization M Rm]
variable [IsLocalization (Algebra.algebraMapSubmonoid B M) Bm]
include M
omit M

Lean source · statement

theorem toNormalization_affineNormalizationLocalizationMap :
    (Spec.map (CommRingCat.ofHom (algebraMap Rm Bm))).toNormalization ≫
        affineNormalizationLocalizationMap R B Rm Bm =
      Spec.map (CommRingCat.ofHom (algebraMap B Bm)) ≫
        (Spec.map (CommRingCat.ofHom (algebraMap R B))).toNormalization

theorem

affineNormalizationLocalization_isPullback

L131 ↗

EtaleFundamentalGroups.Inertia.affineNormalizationLocalization_isPullback

Documentation

The relative-normalization square associated with an arbitrary localization of affine schemes is cartesian. All arrows are the actual structure maps or the map constructed from the integral closures.

Source context 15 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)
variable [IsLocalization M Rm]
variable [IsLocalization (Algebra.algebraMapSubmonoid B M) Bm]
include M
omit M
include M

Lean source · statement

theorem affineNormalizationLocalization_isPullback :
    IsPullback
      (affineNormalizationLocalizationMap R B Rm Bm)
      (Spec.map (CommRingCat.ofHom (algebraMap Rm Bm))).fromNormalization
      (Spec.map (CommRingCat.ofHom (algebraMap R B))).fromNormalization
      (Spec.map (CommRingCat.ofHom (algebraMap R Rm)))

def

affineNormalizationLocalizationIso

L156 ↗

EtaleFundamentalGroups.Inertia.affineNormalizationLocalizationIso

Documentation

Normalization after localization is canonically isomorphic to the actual pullback of the original normalization. This applies in particular to localization at a prime ideal.

Source context 17 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)
variable [IsLocalization M Rm]
variable [IsLocalization (Algebra.algebraMapSubmonoid B M) Bm]
include M
omit M
include M
omit M
include M

Lean source · statement

def affineNormalizationLocalizationIso :
    (Spec.map (CommRingCat.ofHom (algebraMap Rm Bm))).normalization ≅
      pullback (Spec.map (CommRingCat.ofHom (algebraMap R B))).fromNormalization
        (Spec.map (CommRingCat.ofHom (algebraMap R Rm)))

theorem

affineNormalizationLocalizationIso_hom_fst

L163 ↗

EtaleFundamentalGroups.Inertia.affineNormalizationLocalizationIso_hom_fst

Source context 17 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)
variable [IsLocalization M Rm]
variable [IsLocalization (Algebra.algebraMapSubmonoid B M) Bm]
include M
omit M
include M
omit M
include M

Lean source · statement

theorem affineNormalizationLocalizationIso_hom_fst :
    (affineNormalizationLocalizationIso R B Rm Bm M).hom ≫
        pullback.fst
          (Spec.map (CommRingCat.ofHom (algebraMap R B))).fromNormalization
          (Spec.map (CommRingCat.ofHom (algebraMap R Rm))) =
      affineNormalizationLocalizationMap R B Rm Bm

theorem

affineNormalizationLocalizationIso_hom_snd

L172 ↗

EtaleFundamentalGroups.Inertia.affineNormalizationLocalizationIso_hom_snd

Source context 17 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)
variable [IsLocalization M Rm]
variable [IsLocalization (Algebra.algebraMapSubmonoid B M) Bm]
include M
omit M
include M
omit M
include M

Lean source · statement

theorem affineNormalizationLocalizationIso_hom_snd :
    (affineNormalizationLocalizationIso R B Rm Bm M).hom ≫
        pullback.snd
          (Spec.map (CommRingCat.ofHom (algebraMap R B))).fromNormalization
          (Spec.map (CommRingCat.ofHom (algebraMap R Rm))) =
      (Spec.map (CommRingCat.ofHom (algebraMap Rm Bm))).fromNormalization

Module documentation

Affine relative normalization and arbitrary localization

Declarations