Module

GeometricallyIntegral_isIntegral_of_flat_of_universallyOpen.lean

Nyll.AlgebraicCurves.Geometry.Curves.GeometricallyIntegral_isIntegral_of_flat_of_universallyOpen

2 declarations indexed from sourceView source ↗

Module documentation

Integrality over an integral base

A flat, universally open, geometrically integral morphism has an integral total scheme when its base is integral.

Imports1

Mathlib.AlgebraicGeometry.Geometrically.Integral

Imported by2

theorem

finite_irreducibleComponents_of_irreducibleSpace

L38 ↗

AlgebraicCurves.Geometry.Curves.Proofs.GeometricallyIntegral_isIntegral_of_flat_of_universallyOpen.AlgebraicGeometry.finite_irreducibleComponents_of_irreducibleSpace

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace GeometricallyIntegral_isIntegral_of_flat_of_universallyOpen
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry

Lean source · statement

theorem finite_irreducibleComponents_of_irreducibleSpace (S : Type*) [TopologicalSpace S]
    [IrreducibleSpace S] : (irreducibleComponents S).Finite

theorem

isIntegral_of_flat_of_universallyOpen

L47 ↗

AlgebraicGeometry.GeometricallyIntegral.isIntegral_of_flat_of_universallyOpen

Source context 7 commands