Module

Scheme_exists_isClosedImmersion_forall_exists_comp_eq_iff_ideal_eq_bot.lean

Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_exists_isClosedImmersion_forall_exists_comp_eq_iff_ideal_eq_bot

11 declarations indexed from sourceView source ↗

Module documentation

Scheme exists is Closed Immersion forall exists comp eq iff ideal eq bot

Imports15

Mathlib.Algebra.Category.Ring.Limits
Mathlib.AlgebraicGeometry.AffineScheme
Mathlib.AlgebraicGeometry.Cover.MorphismProperty
Mathlib.AlgebraicGeometry.Cover.Open
Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Mathlib.AlgebraicGeometry.Gluing
Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Mathlib.AlgebraicGeometry.OpenImmersion
Mathlib.AlgebraicGeometry.Pullbacks
Mathlib.AlgebraicGeometry.Restrict
Mathlib.RingTheory.Ideal.Quotient.Operations
Mathlib.Tactic.Choose
Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing

Imported by2

theorem

affineOpenWitness

L53 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isClosedImmersion_forall_exists_comp_eq_iff_ideal_eq_bot.G0.affineOpenWitness

Documentation

The affine-open subtype supplies the hypothesis expected by affine chart maps.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isClosedImmersion_forall_exists_comp_eq_iff_ideal_eq_bot
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
noncomputable section
namespace G0
variable (E : Scheme.{u})
  (I : ∀ (R : Type u) [CommRing R], (Spec (CommRingCat.of R) ⟶ E) → Ideal R)
  (hI : ∀ (R R' : Type u) [CommRing R] [CommRing R'] (ψ : R →+* R') (s : Spec (CommRingCat.of R) ⟶
    E),
      I R' (Spec.map (CommRingCat.ofHom ψ) ≫ s) = (I R s).map ψ)

Lean source · statement

theorem affineOpenWitness {X : Scheme.{u}} (U : X.affineOpens) :
    IsAffineOpen U.1

def

idealOf

L59 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isClosedImmersion_forall_exists_comp_eq_iff_ideal_eq_bot.G0.idealOf

Documentation

The ideal assigned to the affine chart of E by the given functorial ideal rule.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isClosedImmersion_forall_exists_comp_eq_iff_ideal_eq_bot
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
noncomputable section
namespace G0
variable (E : Scheme.{u})
  (I : ∀ (R : Type u) [CommRing R], (Spec (CommRingCat.of R) ⟶ E) → Ideal R)
  (hI : ∀ (R R' : Type u) [CommRing R] [CommRing R'] (ψ : R →+* R') (s : Spec (CommRingCat.of R) ⟶
    E),
      I R' (Spec.map (CommRingCat.ofHom ψ) ≫ s) = (I R s).map ψ)

Lean source · statement

def idealOf (U : E.affineOpens) : Ideal Γ(E, U)

theorem

idealOf_map

L61 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isClosedImmersion_forall_exists_comp_eq_iff_ideal_eq_bot.G0.idealOf_map

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isClosedImmersion_forall_exists_comp_eq_iff_ideal_eq_bot
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
noncomputable section
namespace G0
variable (E : Scheme.{u})
  (I : ∀ (R : Type u) [CommRing R], (Spec (CommRingCat.of R) ⟶ E) → Ideal R)
  (hI : ∀ (R R' : Type u) [CommRing R] [CommRing R'] (ψ : R →+* R') (s : Spec (CommRingCat.of R) ⟶
    E),
      I R' (Spec.map (CommRingCat.ofHom ψ) ≫ s) = (I R s).map ψ)
include hI in

Lean source · statement

theorem idealOf_map {U V : E.affineOpens} (h : V.1 ≤ U.1) :
    (idealOf E I U).map (E.presheaf.map (homOfLE h).op).hom = idealOf E I V

def

J

L68 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isClosedImmersion_forall_exists_comp_eq_iff_ideal_eq_bot.G0.J

Documentation

The ideal sheaf data obtained by restricting the functorial ideal rule to affine opens.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isClosedImmersion_forall_exists_comp_eq_iff_ideal_eq_bot
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
noncomputable section
namespace G0
variable (E : Scheme.{u})
  (I : ∀ (R : Type u) [CommRing R], (Spec (CommRingCat.of R) ⟶ E) → Ideal R)
  (hI : ∀ (R R' : Type u) [CommRing R] [CommRing R'] (ψ : R →+* R') (s : Spec (CommRingCat.of R) ⟶
    E),
      I R' (Spec.map (CommRingCat.ofHom ψ) ≫ s) = (I R s).map ψ)

Lean source · full declaration

def J : E.IdealSheafData where
  ideal U := idealOf E I U
  map_ideal_basicOpen U f := by
    have h := idealOf_map E I hI (U := U) (V := E.affineBasicOpen f) (E.basicOpen_le f)
    exact h

theorem

J_ideal

L74 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isClosedImmersion_forall_exists_comp_eq_iff_ideal_eq_bot.G0.J_ideal

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isClosedImmersion_forall_exists_comp_eq_iff_ideal_eq_bot
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
noncomputable section
namespace G0
variable (E : Scheme.{u})
  (I : ∀ (R : Type u) [CommRing R], (Spec (CommRingCat.of R) ⟶ E) → Ideal R)
  (hI : ∀ (R R' : Type u) [CommRing R] [CommRing R'] (ψ : R →+* R') (s : Spec (CommRingCat.of R) ⟶
    E),
      I R' (Spec.map (CommRingCat.ofHom ψ) ≫ s) = (I R s).map ψ)

Lean source · statement

theorem J_ideal (U : E.affineOpens) : (J E I hI).ideal U = I (Γ(E, U))
  (affineOpenWitness U).fromSpec

def

ψV

L83 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isClosedImmersion_forall_exists_comp_eq_iff_ideal_eq_bot.G0.ψV

Documentation

The restriction from R to an affine open of its spectrum, via the canonical global-sections isomorphism.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isClosedImmersion_forall_exists_comp_eq_iff_ideal_eq_bot
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
noncomputable section
namespace G0
variable (E : Scheme.{u})
  (I : ∀ (R : Type u) [CommRing R], (Spec (CommRingCat.of R) ⟶ E) → Ideal R)
  (hI : ∀ (R R' : Type u) [CommRing R] [CommRing R'] (ψ : R →+* R') (s : Spec (CommRingCat.of R) ⟶
    E),
      I R' (Spec.map (CommRingCat.ofHom ψ) ≫ s) = (I R s).map ψ)
section AffinePoints
variable (R : Type u) [CommRing R]

Lean source · statement

def ψV (V : (Spec (CommRingCat.of R)).affineOpens) : R →+* Γ(Spec (CommRingCat.of R), V)

theorem

fromSpec_eq_specMap_ψV

L86 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isClosedImmersion_forall_exists_comp_eq_iff_ideal_eq_bot.G0.fromSpec_eq_specMap_ψV

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isClosedImmersion_forall_exists_comp_eq_iff_ideal_eq_bot
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
noncomputable section
namespace G0
variable (E : Scheme.{u})
  (I : ∀ (R : Type u) [CommRing R], (Spec (CommRingCat.of R) ⟶ E) → Ideal R)
  (hI : ∀ (R R' : Type u) [CommRing R] [CommRing R'] (ψ : R →+* R') (s : Spec (CommRingCat.of R) ⟶
    E),
      I R' (Spec.map (CommRingCat.ofHom ψ) ≫ s) = (I R s).map ψ)
section AffinePoints
variable (R : Type u) [CommRing R]

Lean source · statement

theorem fromSpec_eq_specMap_ψV (V : (Spec (CommRingCat.of R)).affineOpens) :
    (affineOpenWitness V).fromSpec = Spec.map (CommRingCat.ofHom (ψV R V))

theorem

exists_theta

L96 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isClosedImmersion_forall_exists_comp_eq_iff_ideal_eq_bot.G0.exists_theta

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isClosedImmersion_forall_exists_comp_eq_iff_ideal_eq_bot
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
noncomputable section
namespace G0
variable (E : Scheme.{u})
  (I : ∀ (R : Type u) [CommRing R], (Spec (CommRingCat.of R) ⟶ E) → Ideal R)
  (hI : ∀ (R R' : Type u) [CommRing R] [CommRing R'] (ψ : R →+* R') (s : Spec (CommRingCat.of R) ⟶
    E),
      I R' (Spec.map (CommRingCat.ofHom ψ) ≫ s) = (I R s).map ψ)
variable {E}
include hI in

Lean source · statement

theorem exists_theta {R : Type u} [CommRing R] (s : Spec (CommRingCat.of R) ⟶ E)
    (U : E.affineOpens) (V : (Spec (CommRingCat.of R)).affineOpens) (hV : V.1 ≤ s ⁻¹ᵁ U.1) :
    ∃ θ : Γ(E, U) ⟶ Γ(Spec (CommRingCat.of R), V),
      Spec.map θ ≫ (affineOpenWitness U).fromSpec = (affineOpenWitness V).fromSpec ≫ s ∧
      (idealOf E I U).map θ.hom = (I R s).map (ψV R V)

theorem

iSup_small_eq_top

L123 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isClosedImmersion_forall_exists_comp_eq_iff_ideal_eq_bot.G0.iSup_small_eq_top

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isClosedImmersion_forall_exists_comp_eq_iff_ideal_eq_bot
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
noncomputable section
namespace G0
variable (E : Scheme.{u})
  (I : ∀ (R : Type u) [CommRing R], (Spec (CommRingCat.of R) ⟶ E) → Ideal R)
  (hI : ∀ (R R' : Type u) [CommRing R] [CommRing R'] (ψ : R →+* R') (s : Spec (CommRingCat.of R) ⟶
    E),
      I R' (Spec.map (CommRingCat.ofHom ψ) ≫ s) = (I R s).map ψ)
variable {E}

Lean source · statement

theorem iSup_small_eq_top {R : Type u} [CommRing R] (s : Spec (CommRingCat.of R) ⟶ E) :
    (⨆ V : {V : (Spec (CommRingCat.of R)).affineOpens // ∃ U : E.affineOpens, V.1 ≤ s ⁻¹ᵁ U.1},
      V.1.1) = ⊤

theorem

main

L135 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isClosedImmersion_forall_exists_comp_eq_iff_ideal_eq_bot.G0.main

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isClosedImmersion_forall_exists_comp_eq_iff_ideal_eq_bot
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
noncomputable section
namespace G0
variable (E : Scheme.{u})
  (I : ∀ (R : Type u) [CommRing R], (Spec (CommRingCat.of R) ⟶ E) → Ideal R)
  (hI : ∀ (R R' : Type u) [CommRing R] [CommRing R'] (ψ : R →+* R') (s : Spec (CommRingCat.of R) ⟶
    E),
      I R' (Spec.map (CommRingCat.ofHom ψ) ≫ s) = (I R s).map ψ)
variable {E}
include hI in

Lean source · statement

theorem main : ∃ (Z : Scheme.{u}) (ι : Z ⟶ E), IsClosedImmersion ι ∧
      ∀ (R : Type u) [CommRing R] (s : Spec (CommRingCat.of R) ⟶ E),
        (∃ z : Spec (CommRingCat.of R) ⟶ Z, z ≫ ι = s) ↔ I R s = ⊥

theorem

exists_isClosedImmersion_forall_exists_comp_eq_iff_ideal_eq_bot

L321 ↗

AlgebraicGeometry.Scheme.exists_isClosedImmersion_forall_exists_comp_eq_iff_ideal_eq_bot

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isClosedImmersion_forall_exists_comp_eq_iff_ideal_eq_bot
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
attribute [local simp] G0.J_ideal

Lean source · statement

theorem
  _root_.AlgebraicGeometry.Scheme.exists_isClosedImmersion_forall_exists_comp_eq_iff_ideal_eq_bot
    (E : Scheme.{u})
    (I : ∀ (R : Type u) [CommRing R], (Spec (CommRingCat.of R) ⟶ E) → Ideal R)
    (hI : ∀ (R R' : Type u) [CommRing R] [CommRing R'] (ψ : R →+* R') (s : Spec (CommRingCat.of R)
      ⟶ E),
      I R' (Spec.map (CommRingCat.ofHom ψ) ≫ s) = (I R s).map ψ) :
    ∃ (Z : Scheme.{u}) (ι : Z ⟶ E), IsClosedImmersion ι ∧
      ∀ (R : Type u) [CommRing R] (s : Spec (CommRingCat.of R) ⟶ E),
        (∃ z : Spec (CommRingCat.of R) ⟶ Z, z ≫ ι = s) ↔ I R s = ⊥

Module documentation

Scheme exists is Closed Immersion forall exists comp eq iff ideal eq bot

Declarations