Module

GeometricallyIrreducibleOverAlgebraicallyClosed.lean

Nyll.SchemeTheory.Morphisms.GeometricallyIrreducibleOverAlgebraicallyClosed

8 declarations indexed from sourceView source ↗

Module documentation

Geometric irreducibility over an algebraically closed field

An irreducible scheme over an algebraically closed field remains irreducible after extension of the base field. Affine algebra arguments and local affine charts supply the comparison.

Imports8

Mathlib.AlgebraicGeometry.Geometrically.Irreducible
Mathlib.AlgebraicGeometry.Fiber
Mathlib.FieldTheory.IsAlgClosed.Basic
Mathlib.RingTheory.Jacobson.Ring
Mathlib.RingTheory.TensorProduct.Nontrivial
Mathlib.RingTheory.TensorProduct.Free
Mathlib.RingTheory.Flat.Basic
Mathlib.LinearAlgebra.TensorProduct.Finiteness

Imported by10

theorem

algebraMap_quotient_bijective

L49 ↗

AlgebraicCurves.Geometry.Curves.Proofs.GeometricallyIrreducible_of_irreducibleSpace_of_isAlgClosed.IsAlgClosed.BaseChangeIrreducible.algebraMap_quotient_bijective

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace GeometricallyIrreducible_of_irreducibleSpace_of_isAlgClosed
universe u v w
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
namespace IsAlgClosed
open _root_.IsAlgClosed
namespace BaseChangeIrreducible
open _root_.IsAlgClosed
section FiniteType
variable {K : Type u} [Field K]

Lean source · statement

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

def

pointOfMaximal

L59 ↗

AlgebraicCurves.Geometry.Curves.Proofs.GeometricallyIrreducible_of_irreducibleSpace_of_isAlgClosed.IsAlgClosed.BaseChangeIrreducible.pointOfMaximal

Documentation

The K-valued point obtained by identifying the residue field of a maximal ideal with K.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace GeometricallyIrreducible_of_irreducibleSpace_of_isAlgClosed
universe u v w
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
namespace IsAlgClosed
open _root_.IsAlgClosed
namespace BaseChangeIrreducible
open _root_.IsAlgClosed
section FiniteType
variable {K : Type u} [Field K]
variable (K) in

Lean source · statement

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

theorem

pointOfMaximal_eq_zero_iff

L68 ↗

AlgebraicCurves.Geometry.Curves.Proofs.GeometricallyIrreducible_of_irreducibleSpace_of_isAlgClosed.IsAlgClosed.BaseChangeIrreducible.pointOfMaximal_eq_zero_iff

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace GeometricallyIrreducible_of_irreducibleSpace_of_isAlgClosed
universe u v w
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
namespace IsAlgClosed
open _root_.IsAlgClosed
namespace BaseChangeIrreducible
open _root_.IsAlgClosed
section FiniteType
variable {K : Type u} [Field K]
variable (K) in

Lean source · statement

theorem pointOfMaximal_eq_zero_iff [IsAlgClosed K] {A : Type v} [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_finiteType

L75 ↗

AlgebraicCurves.Geometry.Curves.Proofs.GeometricallyIrreducible_of_irreducibleSpace_of_isAlgClosed.IsAlgClosed.BaseChangeIrreducible.isDomain_tensorProduct_of_finiteType

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace GeometricallyIrreducible_of_irreducibleSpace_of_isAlgClosed
universe u v w
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
namespace IsAlgClosed
open _root_.IsAlgClosed
namespace BaseChangeIrreducible
open _root_.IsAlgClosed
section FiniteType
variable {K : Type u} [Field K]
variable (K) in

Lean source · statement

theorem isDomain_tensorProduct_of_finiteType [IsAlgClosed K] (A : Type v) (B : Type w)
    [CommRing A] [Algebra K A] [Algebra.FiniteType K A] [IsDomain A]
    [CommRing B] [Algebra K B] [IsDomain B] :
    IsDomain (A ⊗[K] B)

theorem

isDomain_tensorProduct_of_field

L138 ↗

AlgebraicCurves.Geometry.Curves.Proofs.GeometricallyIrreducible_of_irreducibleSpace_of_isAlgClosed.IsAlgClosed.BaseChangeIrreducible.isDomain_tensorProduct_of_field

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace GeometricallyIrreducible_of_irreducibleSpace_of_isAlgClosed
universe u v w
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
namespace IsAlgClosed
open _root_.IsAlgClosed
namespace BaseChangeIrreducible
open _root_.IsAlgClosed
section Fields
variable (k : Type u) [Field k] [IsAlgClosed k]

Lean source · statement

theorem isDomain_tensorProduct_of_field (F : Type v) (B : Type w) [Field F] [Algebra k F]
    [CommRing B] [Algebra k B] [IsDomain B] : IsDomain (F ⊗[k] B)

theorem

irreducibleSpace_fiber_fst

L188 ↗

AlgebraicCurves.Geometry.Curves.Proofs.GeometricallyIrreducible_of_irreducibleSpace_of_isAlgClosed.IsAlgClosed.BaseChangeIrreducible.irreducibleSpace_fiber_fst

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace GeometricallyIrreducible_of_irreducibleSpace_of_isAlgClosed
universe u v w
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
namespace IsAlgClosed
open _root_.IsAlgClosed
namespace BaseChangeIrreducible
open _root_.IsAlgClosed
section Schemes
variable {k : Type u} [Field k] [IsAlgClosed k] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of k)) (K : Type u) [Field K] [Algebra k K]

Lean source · statement

theorem irreducibleSpace_fiber_fst (x : X) :
    IrreducibleSpace
      ↥((pullback.fst f (Spec.map (CommRingCat.ofHom (algebraMap k K)))).fiber x)

theorem

irreducibleSpace_pullback

L205 ↗

AlgebraicCurves.Geometry.Curves.Proofs.GeometricallyIrreducible_of_irreducibleSpace_of_isAlgClosed.IsAlgClosed.BaseChangeIrreducible.irreducibleSpace_pullback

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace GeometricallyIrreducible_of_irreducibleSpace_of_isAlgClosed
universe u v w
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
namespace IsAlgClosed
open _root_.IsAlgClosed
namespace BaseChangeIrreducible
open _root_.IsAlgClosed
section Schemes
variable {k : Type u} [Field k] [IsAlgClosed k] {X : Scheme.{u}}
  (f : X ⟶ Spec (CommRingCat.of k)) (K : Type u) [Field K] [Algebra k K]

Lean source · statement

theorem irreducibleSpace_pullback [IrreducibleSpace X] :
    IrreducibleSpace ↥(pullback f (Spec.map (CommRingCat.ofHom (algebraMap k K))))

theorem

of_irreducibleSpace_of_isAlgClosed

L234 ↗

AlgebraicGeometry.GeometricallyIrreducible.of_irreducibleSpace_of_isAlgClosed

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace GeometricallyIrreducible_of_irreducibleSpace_of_isAlgClosed
universe u v w
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct

Lean source · statement

theorem _root_.AlgebraicGeometry.GeometricallyIrreducible.of_irreducibleSpace_of_isAlgClosed {k :
    Type u} [Field k] [IsAlgClosed k] {X : Scheme.{u}}
    (f : X ⟶ Spec (CommRingCat.of k)) [IrreducibleSpace X] :
    GeometricallyIrreducible f

Module documentation

Geometric irreducibility over an algebraically closed field

Declarations