NYLL
Module

NormalizationLocalizationPullback.lean

Nyll.EtaleFundamentalGroups.Inertia.NormalizationLocalizationPullback
1 declaration indexed from sourceView source ↗

Module documentation

The canonical normalization pullback for an affine localization

The localization square of actual coordinate rings is a pushout. Its spectrum identifies the affine localized source with the categorical pullback. The corresponding source isomorphism extends to normalization, and uniqueness of normalization shows that the already constructed localization comparison is exactly the canonical normalizationPullback morphism. Hence that canonical morphism is an isomorphism without any smoothness assumption.

There are nine data instances: four commutative rings and the five displayed algebra edges. Every target has one owner; both compatible paths to Bm use the same Algebra R Bm. The localization and tower instances are propositions.

Imports5
Imported by1

Declarations

theorem

isIso_normalizationPullback_of_affineLocalization

L48 ↗
EtaleFundamentalGroups.Inertia.isIso_normalizationPullback_of_affineLocalization
Documentation

Normalization commutes with an arbitrary affine localization through its actual canonical pullback comparison.

Source context 12 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]
include M Bm
Lean source · statement
theorem isIso_normalizationPullback_of_affineLocalization :
    IsIso ((Spec.map (CommRingCat.ofHom (algebraMap R B))).normalizationPullback
      (Spec.map (CommRingCat.ofHom (algebraMap R Rm))))

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