NYLL
Module

NormalizationStalkLocalization.lean

Nyll.EtaleFundamentalGroups.Inertia.NormalizationStalkLocalization
4 declarations indexed from sourceView source ↗

Module documentation

Relative normalization over localized stalks

The actual map from a localized stalk factors through an affine neighbourhood. Its section map is a localization, using the germ map and the standard localization-at-prime construction. The normalization comparison therefore is an isomorphism for any qcqs source, without assuming the source is affine.

Imports5
Imported by7

Declarations

theorem

fromSpec_appLE_self

L30 ↗
EtaleFundamentalGroups.Inertia.fromSpec_appLE_self
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 fromSpec_appLE_self
    {X : Scheme.{u}} {U : X.Opens} (hU : IsAffineOpen U)
    (h : (⊤ : (Spec Γ(X, U)).Opens) ≤ hU.fromSpec ⁻¹ᵁ U) :
    hU.fromSpec.appLE U ⊤ h = (Scheme.ΓSpecIso Γ(X, U)).inv
theorem

isIso_normalizationPullback_fromAffineLocalization

L41 ↗
EtaleFundamentalGroups.Inertia.isIso_normalizationPullback_fromAffineLocalization
Documentation

A localization of the coordinate ring of an affine neighbourhood commutes with normalization through the actual comparison map.

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 isIso_normalizationPullback_fromAffineLocalization
    {X Y : Scheme.{u}} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f]
    {U : Y.Opens} (hU : IsAffineOpen U)
    (S : CommRingCat.{u}) [Algebra Γ(Y, U) S]
    (M : Submonoid Γ(Y, U)) [IsLocalization M S] :
    IsIso (f.normalizationPullback
      (Spec.map (CommRingCat.ofHom (algebraMap Γ(Y, U) S)) ≫ hU.fromSpec))
theorem

isIso_normalizationPullback_fromSpecStalk

L86 ↗
EtaleFundamentalGroups.Inertia.isIso_normalizationPullback_fromSpecStalk
Documentation

Relative normalization commutes with the actual map from the spectrum of any stalk, independently of an affine-neighbourhood choice.

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 isIso_normalizationPullback_fromSpecStalk
    {X Y : Scheme.{u}} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f]
    (y : Y) : IsIso (f.normalizationPullback (Y.fromSpecStalk y))
theorem

isIso_normalizationPullback_fromSpecStalkLocalization

L102 ↗
EtaleFundamentalGroups.Inertia.isIso_normalizationPullback_fromSpecStalkLocalization
Documentation

Relative normalization commutes with the canonical map from any prime localization of a stalk. All localization and flatness data are constructed.

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 isIso_normalizationPullback_fromSpecStalkLocalization
    {X Y : Scheme.{u}} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f]
    (y : Y) (P : Ideal (Y.presheaf.stalk y)) [P.IsPrime] :
    IsIso (f.normalizationPullback
      (Spec.map (CommRingCat.ofHom (algebraMap (Y.presheaf.stalk y)
        (Localization.AtPrime P))) ≫ Y.fromSpecStalk y))

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