NYLL
Module

AffineFiniteEtale.lean

Nyll.SchemeTheory.Normalization.AffineFiniteEtale
3 declarations indexed from sourceView source ↗

Module documentation

The structure map of an affine relative normalization

The canonical affine normalization isomorphism intertwines the actual structure map with the algebra map into the integral closure. This gives the ring criterion for finite etaleness of that actual normalization map.

Imports5
Imported by3

Declarations

theorem

specNormalizationIso_hom_fromNormalization

L35 ↗
AlgebraicGeometry.specNormalizationIso_hom_fromNormalization
Documentation

The affine normalization comparison is an isomorphism over the original base, for the literal structural algebra map.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace AlgebraicGeometry
universe u
variable (R T : Type u) [CommRing R] [CommRing T] [Algebra R T]
Lean source · statement
theorem specNormalizationIso_hom_fromNormalization :
    (specNormalizationIso R T).hom ≫
        Spec.map (CommRingCat.ofHom (algebraMap R (integralClosure R T))) =
      (affineStructureMap R T).fromNormalization
theorem

isFiniteEtale_specNormalization_iff

L46 ↗
AlgebraicGeometry.isFiniteEtale_specNormalization_iff
Documentation

Finite etaleness of an affine relative normalization is precisely finite etaleness of the literal integral-closure algebra.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace AlgebraicGeometry
universe u
variable (R T : Type u) [CommRing R] [CommRing T] [Algebra R T]
Lean source · statement
theorem isFiniteEtale_specNormalization_iff :
    IsFiniteEtale (affineStructureMap R T).fromNormalization ↔
      Module.Finite R (integralClosure R T) ∧ Algebra.Etale R (integralClosure R T)
theorem

finite_etale_tensor_integralClosure_of_normalization_baseChange

L74 ↗
AlgebraicGeometry.finite_etale_tensor_integralClosure_of_normalization_baseChange
Documentation

Finite etaleness of an actual base change of an affine normalization supplies the canonical tensor-algebra properties used in affine spreading.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace AlgebraicGeometry
universe u
variable (R T : Type u) [CommRing R] [CommRing T] [Algebra R T]
Lean source · statement
theorem finite_etale_tensor_integralClosure_of_normalization_baseChange
    (A : Type u) [CommRing A] [Algebra R A]
    (h : IsFiniteEtale (pullback.snd (affineStructureMap R T).fromNormalization
      (Spec.map (CommRingCat.ofHom (algebraMap R A))))) :
    Module.Finite A (A ⊗[R] integralClosure R T) ∧
      Algebra.Etale A (A ⊗[R] integralClosure R T)

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