Module

Scheme_IdealSheafData_isReduced_subscheme_vanishingIdeal_and_le_ker.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_isReduced_subscheme_vanishingIdeal_and_le_ker

7 declarations indexed from sourceView source ↗

Module documentation

Scheme Ideal Sheaf Data is Reduced subscheme vanishing Ideal and le ker

Imports1

Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Imported by5

theorem

isRadical_vanishingIdeal_ideal

L34 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_isReduced_subscheme_vanishingIdeal_and_le_ker.P2mReducedInduced.isRadical_vanishingIdeal_ideal

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_isReduced_subscheme_vanishingIdeal_and_le_ker
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace
universe u
namespace P2mReducedInduced
open AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.IdealSheafData
variable {X : Scheme.{u}}

Lean source · statement

theorem isRadical_vanishingIdeal_ideal (Z : Closeds X) (U : X.affineOpens) :
    ((vanishingIdeal Z).ideal U).IsRadical

theorem

isReduced_subscheme_vanishingIdeal

L39 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_isReduced_subscheme_vanishingIdeal_and_le_ker.P2mReducedInduced.isReduced_subscheme_vanishingIdeal

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_isReduced_subscheme_vanishingIdeal_and_le_ker
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace
universe u
namespace P2mReducedInduced
open AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.IdealSheafData
variable {X : Scheme.{u}}

Lean source · statement

theorem isReduced_subscheme_vanishingIdeal (Z : Closeds X) :
    IsReduced (vanishingIdeal Z).subscheme

theorem

range_subschemeι_vanishingIdeal

L50 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_isReduced_subscheme_vanishingIdeal_and_le_ker.P2mReducedInduced.range_subschemeι_vanishingIdeal

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_isReduced_subscheme_vanishingIdeal_and_le_ker
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace
universe u
namespace P2mReducedInduced
open AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.IdealSheafData
variable {X : Scheme.{u}}

Lean source · statement

theorem range_subschemeι_vanishingIdeal (Z : Closeds X) :
    Set.range (vanishingIdeal Z).subschemeι = (Z : Set X)

theorem

basicOpen_inter_eq_empty_of_mem_vanishingIdeal

L55 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_isReduced_subscheme_vanishingIdeal_and_le_ker.P2mReducedInduced.basicOpen_inter_eq_empty_of_mem_vanishingIdeal

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_isReduced_subscheme_vanishingIdeal_and_le_ker
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace
universe u
namespace P2mReducedInduced
open AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.IdealSheafData
variable {X : Scheme.{u}}

Lean source · statement

theorem basicOpen_inter_eq_empty_of_mem_vanishingIdeal (Z : Closeds X) (U : X.affineOpens)
    {s : Γ(X, U)} (hs : s ∈ (vanishingIdeal Z).ideal U) :
    (X.basicOpen s : Set X) ∩ Z = ∅

theorem

vanishingIdeal_le_ker

L70 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_isReduced_subscheme_vanishingIdeal_and_le_ker.P2mReducedInduced.vanishingIdeal_le_ker

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_isReduced_subscheme_vanishingIdeal_and_le_ker
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace
universe u
namespace P2mReducedInduced
open AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.IdealSheafData
variable {X : Scheme.{u}}

Lean source · statement

theorem vanishingIdeal_le_ker {T : Scheme.{u}} [IsReduced T] (Z : Closeds X) (f : T ⟶ X)
    (hf : Set.range f ⊆ Z) : vanishingIdeal Z ≤ f.ker

theorem

exists_lift_subschemeι_vanishingIdeal

L86 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_isReduced_subscheme_vanishingIdeal_and_le_ker.P2mReducedInduced.exists_lift_subschemeι_vanishingIdeal

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_isReduced_subscheme_vanishingIdeal_and_le_ker
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace
universe u
namespace P2mReducedInduced
open AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.IdealSheafData
variable {X : Scheme.{u}}

Lean source · statement

theorem exists_lift_subschemeι_vanishingIdeal {T : Scheme.{u}} [IsReduced T] (Z : Closeds X)
    (f : T ⟶ X) (hf : Set.range f ⊆ Z) :
    ∃! g : T ⟶ (vanishingIdeal Z).subscheme, g ≫ (vanishingIdeal Z).subschemeι = f

theorem

isReduced_subscheme_vanishingIdeal_and_le_ker

L99 ↗

AlgebraicGeometry.Scheme.IdealSheafData.isReduced_subscheme_vanishingIdeal_and_le_ker

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_isReduced_subscheme_vanishingIdeal_and_le_ker
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace
universe u
open P2mReducedInduced AlgebraicGeometry.Scheme.IdealSheafData in

Lean source · statement

theorem
  _root_.AlgebraicGeometry.Scheme.IdealSheafData.isReduced_subscheme_vanishingIdeal_and_le_ker {X :
  Scheme.{u}} (Z : TopologicalSpace.Closeds X) :
    IsReduced (vanishingIdeal Z).subscheme ∧
      ∀ {T : Scheme.{u}} [IsReduced T] (f : T ⟶ X), Set.range f ⊆ Z →
        vanishingIdeal Z ≤ f.ker

Module documentation

Scheme Ideal Sheaf Data is Reduced subscheme vanishing Ideal and le ker

Declarations

isRadical_vanishingIdeal_ideal

isReduced_subscheme_vanishingIdeal

range_subschemeι_vanishingIdeal

basicOpen_inter_eq_empty_of_mem_vanishingIdeal

vanishingIdeal_le_ker

exists_lift_subschemeι_vanishingIdeal

isReduced_subscheme_vanishingIdeal_and_le_ker