Module

Scheme_isIntegral_subscheme_vanishingIdeal.lean

Nyll.SchemeTheory.Divisors.Scheme_isIntegral_subscheme_vanishingIdeal

5 declarations indexed from sourceView source ↗

Module documentation

The integral subscheme of an irreducible closed set

The vanishing ideal of an irreducible closed set defines an integral subscheme with that closed set as its support.

Imports3

Mathlib.Util.WithWeakNamespace
Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Mathlib.AlgebraicGeometry.Properties

Imported by2

theorem

isReduced_vanishingIdeal

L45 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_isIntegral_subscheme_vanishingIdeal.AlgebraicGeometry.Scheme.IntegralSubscheme.isReduced_vanishingIdeal

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_isIntegral_subscheme_vanishingIdeal
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IntegralSubscheme
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
universe u
section IntegralSubscheme
variable {V : Scheme.{u}}

Lean source · statement

theorem isReduced_vanishingIdeal (Z : Closeds V) :
    IsReduced (IdealSheafData.vanishingIdeal Z).subscheme

theorem

support_vanishingIdeal

L69 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_isIntegral_subscheme_vanishingIdeal.AlgebraicGeometry.Scheme.IntegralSubscheme.support_vanishingIdeal

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_isIntegral_subscheme_vanishingIdeal
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IntegralSubscheme
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
universe u
section IntegralSubscheme
variable {V : Scheme.{u}}

Lean source · statement

theorem support_vanishingIdeal (Z : Closeds V) :
    (IdealSheafData.vanishingIdeal Z).support = Z

theorem

irreducible_vanishingIdeal

L73 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_isIntegral_subscheme_vanishingIdeal.AlgebraicGeometry.Scheme.IntegralSubscheme.irreducible_vanishingIdeal

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_isIntegral_subscheme_vanishingIdeal
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IntegralSubscheme
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
universe u
section IntegralSubscheme
variable {V : Scheme.{u}}

Lean source · statement

theorem irreducible_vanishingIdeal (Z : Closeds V)
    (hZ : IsIrreducible (Z : Set V)) :
    IrreducibleSpace (IdealSheafData.vanishingIdeal Z).subscheme

theorem

isIntegral_vanishingIdeal

L78 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_isIntegral_subscheme_vanishingIdeal.AlgebraicGeometry.Scheme.IntegralSubscheme.isIntegral_vanishingIdeal

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_isIntegral_subscheme_vanishingIdeal
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IntegralSubscheme
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
universe u
section IntegralSubscheme
variable {V : Scheme.{u}}

Lean source · statement

theorem isIntegral_vanishingIdeal (Z : Closeds V)
    (hZ : IsIrreducible (Z : Set V)) :
    IsIntegral (IdealSheafData.vanishingIdeal Z).subscheme

theorem

isIntegral_subscheme_vanishingIdeal

L93 ↗

AlgebraicGeometry.Scheme.isIntegral_subscheme_vanishingIdeal

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_isIntegral_subscheme_vanishingIdeal
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme
universe u
with_weak_namespace _root_.AlgebraicCurves.Geometry.Schemes.Proofs
open _root_.AlgebraicGeometry Scheme_isIntegral_subscheme_vanishingIdeal.AlgebraicGeometry
    TopologicalSpace in
with_weak_namespace Scheme_isIntegral_subscheme_vanishingIdeal

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.isIntegral_subscheme_vanishingIdeal {V : Scheme.{u}} (Z
    : Closeds V) (hZ : IsIrreducible (Z : Set V)) :
    IsIntegral (Scheme.IdealSheafData.vanishingIdeal Z).subscheme

Module documentation

The integral subscheme of an irreducible closed set

Declarations

isReduced_vanishingIdeal

support_vanishingIdeal

irreducible_vanishingIdeal

isIntegral_vanishingIdeal

isIntegral_subscheme_vanishingIdeal