NYLL
Module

NormalizationFlatBaseChangeIso.lean

Nyll.SchemeTheory.Morphisms.NormalizationFlatBaseChangeIso
1 declaration indexed from sourceView source ↗

Module documentation

The native normalization comparison under flat affine base change

For a universally closed qcqs morphism, the native normalization comparison is an isomorphism after flat base change between affine bases. The proof compares the two actual pushout squares on global sections, using the section isomorphisms of the normalization maps.

Imports2
Imported by1

Declarations

lemma

isIso_normalizationPullback_of_flat_affine

L33 ↗
AlgebraicGeometry.Scheme.Hom.isIso_normalizationPullback_of_flat_affine
Documentation

The actual map from the normalization of the base change to the base change of the normalization is an isomorphism for flat affine base change.

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] [Flat g]
Lean source · statement
lemma isIso_normalizationPullback_of_flat_affine :
    IsIso (f.normalizationPullback g)

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