Module

GeometricallyIntegralDescent.lean

Nyll.SchemeTheory.Morphisms.GeometricallyIntegralDescent

5 declarations indexed from sourceView source ↗

Module documentation

Descent of geometric integrality

This file records a descent criterion for geometric integrality over a field. The morphism used for descent need not be flat: quasicompact scheme-theoretic dominance is enough, since it remains scheme-theoretically dominant after every field extension of the base.

Imports2

Mathlib.AlgebraicGeometry.Geometrically.Integral
Mathlib.AlgebraicGeometry.FunctionField

Imported by2

lemma

flat_fromSpecResidueField_genericPoint

L29 ↗

AlgebraicGeometry.Scheme.flat_fromSpecResidueField_genericPoint

Documentation

The morphism from the residue field of the generic point of an integral scheme is flat.

Source context 4 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
namespace AlgebraicGeometry
universe u

Lean source · statement

lemma Scheme.flat_fromSpecResidueField_genericPoint
    (S : Scheme.{u}) [IsIntegral S] :
    Flat (S.fromSpecResidueField (genericPoint S))

lemma

of_comp_of_isSchemeTheoreticallyDominant

L44 ↗

AlgebraicGeometry.GeometricallyIntegral.of_comp_of_isSchemeTheoreticallyDominant

Documentation

Geometric integrality over a field descends through a quasicompact, scheme-theoretically dominant morphism.

Source context 4 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
namespace AlgebraicGeometry
universe u

Lean source · statement

lemma GeometricallyIntegral.of_comp_of_isSchemeTheoreticallyDominant
    {k : CommRingCat.{u}} {X Y : Scheme.{u}}
    (f : X ⟶ Y) (g : Y ⟶ Spec k) (hk : IsField k)
    [QuasiCompact f] [IsSchemeTheoreticallyDominant f]
    (h : GeometricallyIntegral (f ≫ g)) : GeometricallyIntegral g

lemma

of_comp_of_isDominant

L78 ↗

AlgebraicGeometry.GeometricallyIntegral.of_comp_of_isDominant

Documentation

Geometric integrality over a field descends through a quasicompact dominant morphism with reduced target.

Source context 4 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
namespace AlgebraicGeometry
universe u

Lean source · statement

lemma GeometricallyIntegral.of_comp_of_isDominant
    {k : CommRingCat.{u}} {X Y : Scheme.{u}}
    (f : X ⟶ Y) (g : Y ⟶ Spec k) (hk : IsField k)
    [QuasiCompact f] [IsDominant f] [IsReduced Y]
    (h : GeometricallyIntegral (f ≫ g)) : GeometricallyIntegral g

lemma

genericFiber_of_comp_of_isSchemeTheoreticallyDominant

L89 ↗

AlgebraicGeometry.GeometricallyIntegral.genericFiber_of_comp_of_isSchemeTheoreticallyDominant

Documentation

Geometric integrality of the generic fiber descends through a quasicompact scheme-theoretically dominant morphism.

Source context 4 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
namespace AlgebraicGeometry
universe u

Lean source · statement

lemma GeometricallyIntegral.genericFiber_of_comp_of_isSchemeTheoreticallyDominant
    {X Y S : Scheme.{u}} [IsIntegral S]
    (f : X ⟶ Y) (g : Y ⟶ S)
    [QuasiCompact f] [IsSchemeTheoreticallyDominant f]
    (h : GeometricallyIntegral
      ((f ≫ g).fiberToSpecResidueField (genericPoint S))) :
    GeometricallyIntegral
      (g.fiberToSpecResidueField (genericPoint S))

lemma

genericFiber_of_comp_of_isDominant

L121 ↗

AlgebraicGeometry.GeometricallyIntegral.genericFiber_of_comp_of_isDominant

Documentation

Geometric integrality of the generic fiber descends through a quasicompact dominant morphism with reduced target.

Source context 4 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
namespace AlgebraicGeometry
universe u

Lean source · statement

lemma GeometricallyIntegral.genericFiber_of_comp_of_isDominant
    {X Y S : Scheme.{u}} [IsIntegral S]
    (f : X ⟶ Y) (g : Y ⟶ S)
    [QuasiCompact f] [IsDominant f] [IsReduced Y]
    (h : GeometricallyIntegral
      ((f ≫ g).fiberToSpecResidueField (genericPoint S))) :
    GeometricallyIntegral
      (g.fiberToSpecResidueField (genericPoint S))

Module documentation

Descent of geometric integrality

Declarations

flat_fromSpecResidueField_genericPoint

of_comp_of_isSchemeTheoreticallyDominant

of_comp_of_isDominant

genericFiber_of_comp_of_isSchemeTheoreticallyDominant

genericFiber_of_comp_of_isDominant