Module

geometricallyIntegral_of_isAlgClosed.lean

Nyll.AlgebraicCurves.Geometry.Curves.geometricallyIntegral_of_isAlgClosed

6 declarations indexed from sourceView source ↗

Module documentation

Geometric integrality over an algebraically closed field

An integral scheme locally of finite type over an algebraically closed field is geometrically integral, using the domain property of tensor products of affine sections.

Imports5

Mathlib.AlgebraicGeometry.Geometrically.Integral
Mathlib.FieldTheory.IsAlgClosed.Basic
Mathlib.RingTheory.TensorProduct.Free
Mathlib.RingTheory.TensorProduct.Nontrivial
Mathlib.Tactic.Algebraize

Imported by18

theorem

algebraMap_quotient_bijective_of_isAlgClosed

L39 ↗

AlgebraicCurves.Geometry.Curves.Proofs.geometricallyIntegral_of_isAlgClosed.GeomIntegralOfIsAlgClosed.algebraMap_quotient_bijective_of_isAlgClosed

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs.geometricallyIntegral_of_isAlgClosed
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace AlgebraicGeometry
open scoped TensorProduct
namespace GeomIntegralOfIsAlgClosed
variable {K : Type u} [Field K]

Lean source · statement

theorem algebraMap_quotient_bijective_of_isAlgClosed [IsAlgClosed K] {A : Type*} [CommRing A]
    [Algebra K A] [Algebra.FiniteType K A] (m : Ideal A) [m.IsMaximal] :
    Function.Bijective (algebraMap K (A ⧸ m))

def

pointOfMaximal

L49 ↗

AlgebraicCurves.Geometry.Curves.Proofs.geometricallyIntegral_of_isAlgClosed.GeomIntegralOfIsAlgClosed.pointOfMaximal

Documentation

The rational point corresponding to a maximal ideal over an algebraically closed field.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs.geometricallyIntegral_of_isAlgClosed
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace AlgebraicGeometry
open scoped TensorProduct
namespace GeomIntegralOfIsAlgClosed
variable {K : Type u} [Field K]
variable (K) in

Lean source · statement

def pointOfMaximal [IsAlgClosed K] {A : Type*} [CommRing A]
    [Algebra K A] [Algebra.FiniteType K A] (m : Ideal A) [m.IsMaximal] : A →ₐ[K] K

theorem

pointOfMaximal_eq_zero_iff

L59 ↗

AlgebraicCurves.Geometry.Curves.Proofs.geometricallyIntegral_of_isAlgClosed.GeomIntegralOfIsAlgClosed.pointOfMaximal_eq_zero_iff

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs.geometricallyIntegral_of_isAlgClosed
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace AlgebraicGeometry
open scoped TensorProduct
namespace GeomIntegralOfIsAlgClosed
variable {K : Type u} [Field K]
variable (K) in

Lean source · statement

theorem pointOfMaximal_eq_zero_iff [IsAlgClosed K] {A : Type*} [CommRing A] [Algebra K A]
    [Algebra.FiniteType K A] (m : Ideal A) [m.IsMaximal] (a : A) :
    pointOfMaximal K m a = 0 ↔ a ∈ m

theorem

isDomain_tensorProduct_of_isAlgClosed

L66 ↗

AlgebraicCurves.Geometry.Curves.Proofs.geometricallyIntegral_of_isAlgClosed.GeomIntegralOfIsAlgClosed.isDomain_tensorProduct_of_isAlgClosed

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs.geometricallyIntegral_of_isAlgClosed
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace AlgebraicGeometry
open scoped TensorProduct
namespace GeomIntegralOfIsAlgClosed
variable {K : Type u} [Field K]
variable (K) in

Lean source · statement

theorem isDomain_tensorProduct_of_isAlgClosed [IsAlgClosed K] (A B : Type u) [CommRing A]
    [Algebra K A] [Algebra.FiniteType K A] [IsDomain A] [CommRing B] [Algebra K B] [IsDomain B] :
    IsDomain (A ⊗[K] B)

theorem

isIntegral_pullback_SpecMap_of_isAlgClosed

L121 ↗

AlgebraicCurves.Geometry.Curves.Proofs.geometricallyIntegral_of_isAlgClosed.GeomIntegralOfIsAlgClosed.isIntegral_pullback_SpecMap_of_isAlgClosed

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs.geometricallyIntegral_of_isAlgClosed
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace AlgebraicGeometry
open scoped TensorProduct
namespace GeomIntegralOfIsAlgClosed
variable {K : Type u} [Field K]
variable (K) in

Lean source · statement

theorem isIntegral_pullback_SpecMap_of_isAlgClosed [IsAlgClosed K] {A : CommRingCat.{u}}
    (φ : CommRingCat.of K ⟶ A) [IsIntegral (Spec A)] [LocallyOfFiniteType (Spec.map φ)]
    (K' : Type u) [Field K'] [Algebra K K'] :
    IsIntegral ↑(pullback (Spec.map φ) (Spec.map (CommRingCat.ofHom (algebraMap K K'))))

theorem