Module

GeometricallyIntegralFieldDescent.lean

Nyll.SchemeTheory.Morphisms.GeometricallyIntegralFieldDescent

5 declarations indexed from sourceView source ↗

Module documentation

Descent of geometric integrality across field base change

Geometric integrality is recovered from a pullback over a field extension. The argument combines faithful flat descent of reducedness with the geometric irreducibility comparison.

Imports2

Mathlib.AlgebraicGeometry.Geometrically.Integral
Mathlib.AlgebraicGeometry.Morphisms.Flat

Imported by3

instance

(anonymous instance)

L40 ↗

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace GeometricallyIntegral_of_isPullback_of_geometricallyIntegral
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open scoped TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry

Lean source · statement

instance : ObjectProperty.IsClosedUnderIsomorphisms (C := Scheme) IsIntegral

theorem

surjective_specMap_of_fields

L46 ↗

AlgebraicCurves.Geometry.Curves.Proofs.GeometricallyIntegral_of_isPullback_of_geometricallyIntegral.AlgebraicGeometry.surjective_specMap_of_fields

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace GeometricallyIntegral_of_isPullback_of_geometricallyIntegral
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open scoped TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry

Lean source · statement

theorem surjective_specMap_of_fields {K Ω : Type u} [Field K] [Field Ω] (φ : K →+* Ω) :
    Surjective (Spec.map (CommRingCat.ofHom φ))

theorem

flat_specMap_of_fields

L50 ↗

AlgebraicCurves.Geometry.Curves.Proofs.GeometricallyIntegral_of_isPullback_of_geometricallyIntegral.AlgebraicGeometry.flat_specMap_of_fields

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace GeometricallyIntegral_of_isPullback_of_geometricallyIntegral
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open scoped TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry

Lean source · statement

theorem flat_specMap_of_fields {K Ω : Type u} [Field K] [Field Ω] (φ : K →+* Ω) :
    Flat (Spec.map (CommRingCat.ofHom φ))

theorem

isReduced_of_flat_of_surjective

L56 ↗

AlgebraicCurves.Geometry.Curves.Proofs.GeometricallyIntegral_of_isPullback_of_geometricallyIntegral.AlgebraicGeometry.isReduced_of_flat_of_surjective

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace GeometricallyIntegral_of_isPullback_of_geometricallyIntegral
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open scoped TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry

Lean source · statement

theorem isReduced_of_flat_of_surjective {X Y : Scheme.{u}}
    (π : X ⟶ Y) [Flat π] [Surjective π]
    [IsReduced X] : IsReduced Y

theorem

of_isPullback_of_geometricallyIntegral

L77 ↗

AlgebraicGeometry.GeometricallyIntegral.of_isPullback_of_geometricallyIntegral

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace GeometricallyIntegral_of_isPullback_of_geometricallyIntegral
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open scoped TensorProduct
open _root_.AlgebraicGeometry in
open GeometricallyIntegral_of_isPullback_of_geometricallyIntegral.AlgebraicGeometry in

Lean source · statement

theorem _root_.AlgebraicGeometry.GeometricallyIntegral.of_isPullback_of_geometricallyIntegral
    {κ k : Type u} [Field κ] [Field k] [Algebra κ k]
    {C C' : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of κ))
    (c' : C' ⟶ Spec (CommRingCat.of k)) (g : C' ⟶ C)
    (h : IsPullback g c' c (Spec.map (CommRingCat.ofHom (algebraMap κ k))))
    [GeometricallyIntegral c'] :
    GeometricallyIntegral c

Module documentation

Descent of geometric integrality across field base change

Declarations

(anonymous instance)

surjective_specMap_of_fields

flat_specMap_of_fields

isReduced_of_flat_of_surjective

of_isPullback_of_geometricallyIntegral