Module

FlatBaseChangeNormalization.lean

Nyll.SchemeTheory.Morphisms.FlatBaseChangeNormalization

2 declarations indexed from sourceView source ↗

Module documentation

Flat affine base change for a universally closed normalization

The relative normalization of a universally closed qcqs morphism agrees with affinization over an affine base. The flat base-change theorem for sections therefore gives the cartesian square for the native normalization maps. No connected-fibre or finite-etale hypothesis is used.

Imports2

Imported by1

Nyll.SchemeTheory.Morphisms.All

lemma

normalizationPullback_fst_normalizationIsoSpec

L33 ↗

AlgebraicGeometry.Scheme.Hom.normalizationPullback_fst_normalizationIsoSpec

Documentation

Compatibility of the actual normalization comparison with the affine identifications coming from global sections.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.Scheme.Hom
universe u
variable {X S T : Scheme.{u}} (f : X ⟶ S) (g : T ⟶ S)
variable [QuasiCompact f] [QuasiSeparated f] [UniversallyClosed f]
variable [IsAffine S] [IsAffine T]

Lean source · statement

lemma normalizationPullback_fst_normalizationIsoSpec :
    (f.normalizationPullback g ≫ pullback.fst f.fromNormalization g) ≫
        f.normalizationIsoSpec.hom =
      (pullback.snd f g).normalizationIsoSpec.hom ≫
        Spec.map (pullback.fst f g).appTop

lemma

isPullback_toNormalization_of_flat

L51 ↗

AlgebraicGeometry.Scheme.Hom.isPullback_toNormalization_of_flat