Module

Scheme_exists_isClosedImmersion_represents_of_forall_exists_ideal.lean

Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_exists_isClosedImmersion_represents_of_forall_exists_ideal

35 declarations indexed from sourceView source ↗

Module documentation

Scheme exists is Closed Immersion represents of forall exists ideal

Imports4

Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing

Imported by1

Nyll.AlgebraicCurves.Geometry.Schemes.All

theorem

section_eq_zero_of_cover

L35 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isClosedImmersion_represents_of_forall_exists_ideal.ClosedRep.section_eq_zero_of_cover

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isClosedImmersion_represents_of_forall_exists_ideal
open CategoryTheory AlgebraicGeometry Opposite
namespace ClosedRep
universe u
section Generalities

Lean source · statement

theorem section_eq_zero_of_cover {Y : Scheme.{0}} {V : Y.Opens} (s : Γ(Y, V)) {ι : Type} (U : ι →
  Y.Opens)
    (hU : ∀ i, U i ≤ V) (hcov : V ≤ ⨆ i, U i)
    (h : ∀ i, (Y.presheaf.map (homOfLE (hU i)).op).hom s = 0) : s = 0

theorem

algebraMap_comm_of_Spec

L45 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isClosedImmersion_represents_of_forall_exists_ideal.ClosedRep.algebraMap_comm_of_Spec

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_represents_of_forall_exists_ideal
open CategoryTheory AlgebraicGeometry Opposite
namespace ClosedRep
universe u
section Generalities
variable {R : Type} [CommRing R]

Lean source · statement

theorem algebraMap_comm_of_Spec {A B : Type} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B]
    (ψ : A →+* B)
    (h : Spec.map (CommRingCat.ofHom ψ) ≫ Spec.map (CommRingCat.ofHom (algebraMap R A)) =
      Spec.map (CommRingCat.ofHom (algebraMap R B))) (r : R) :
    ψ (algebraMap R A r) = algebraMap R B r

def

algHomOfSpec

L59 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isClosedImmersion_represents_of_forall_exists_ideal.ClosedRep.algHomOfSpec

Documentation

The algebra homomorphism associated with a ring homomorphism whose spectrum map is over the base.

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_represents_of_forall_exists_ideal
open CategoryTheory AlgebraicGeometry Opposite
namespace ClosedRep
universe u
section Generalities
variable {R : Type} [CommRing R]

Lean source · statement

def algHomOfSpec {A B : Type} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (ψ : A →+* B)
    (h : Spec.map (CommRingCat.ofHom ψ) ≫ Spec.map (CommRingCat.ofHom (algebraMap R A)) =
      Spec.map (CommRingCat.ofHom (algebraMap R B))) : A →ₐ[R] B

theorem

algHomOfSpec_toRingHom

L64 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isClosedImmersion_represents_of_forall_exists_ideal.ClosedRep.algHomOfSpec_toRingHom

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_represents_of_forall_exists_ideal
open CategoryTheory AlgebraicGeometry Opposite
namespace ClosedRep
universe u
section Generalities
variable {R : Type} [CommRing R]

Lean source · statement

theorem algHomOfSpec_toRingHom {A B : Type} [CommRing A] [CommRing B] [Algebra R A]
  [Algebra R B]
    (ψ : A →+* B) (h) : (algHomOfSpec (R := R) ψ h).toRingHom = ψ

theorem

algHomOfSpec_apply

L68 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isClosedImmersion_represents_of_forall_exists_ideal.ClosedRep.algHomOfSpec_apply

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_represents_of_forall_exists_ideal
open CategoryTheory AlgebraicGeometry Opposite
namespace ClosedRep
universe u
section Generalities
variable {R : Type} [CommRing R]

Lean source · statement

theorem algHomOfSpec_apply {A B : Type} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B]
    (ψ : A →+* B) (h) (x : A) : algHomOfSpec (R := R) ψ h x = ψ x

def

PtNatural

L86 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isClosedImmersion_represents_of_forall_exists_ideal.ClosedRep.PtNatural

Documentation

The chosen points commute with extension of the coefficient algebra.

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_represents_of_forall_exists_ideal
open CategoryTheory AlgebraicGeometry Opposite
namespace ClosedRep
universe u
section Setting
variable {R : Type} [CommRing R]
  (F : ∀ (A : Type) [CommRing A] [Algebra R A], Type)
  (Fmap : ∀ (A B : Type) [CommRing A] [CommRing B] [Algebra R A] [Algebra R B], (A →ₐ[R] B) → F A →
    F B)
  {X : Scheme.{0}} (p : X ⟶ Spec (CommRingCat.of R))
  (pt : ∀ (A : Type) [CommRing A] [Algebra R A],
    F A ≃ {g : Spec (CommRingCat.of A) ⟶ X // g ≫ p = Spec.map (CommRingCat.ofHom (algebraMap R
      A))})
  (W : ∀ (A : Type) [CommRing A] [Algebra R A], F A → Prop)

Lean source · statement

def PtNatural : Prop

def

Closed

L91 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isClosedImmersion_represents_of_forall_exists_ideal.ClosedRep.Closed

Documentation

The subfunctor condition is locally cut out by the vanishing of an 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_represents_of_forall_exists_ideal
open CategoryTheory AlgebraicGeometry Opposite
namespace ClosedRep
universe u
section Setting
variable {R : Type} [CommRing R]
  (F : ∀ (A : Type) [CommRing A] [Algebra R A], Type)
  (Fmap : ∀ (A B : Type) [CommRing A] [CommRing B] [Algebra R A] [Algebra R B], (A →ₐ[R] B) → F A →
    F B)
  {X : Scheme.{0}} (p : X ⟶ Spec (CommRingCat.of R))
  (pt : ∀ (A : Type) [CommRing A] [Algebra R A],
    F A ≃ {g : Spec (CommRingCat.of A) ⟶ X // g ≫ p = Spec.map (CommRingCat.ofHom (algebraMap R
      A))})
  (W : ∀ (A : Type) [CommRing A] [Algebra R A], F A → Prop)

Lean source · statement

def Closed : Prop

theorem

Fmap_id

L97 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isClosedImmersion_represents_of_forall_exists_ideal.ClosedRep.Fmap_id

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_represents_of_forall_exists_ideal
open CategoryTheory AlgebraicGeometry Opposite
namespace ClosedRep
universe u
section Setting
variable {R : Type} [CommRing R]
  (F : ∀ (A : Type) [CommRing A] [Algebra R A], Type)
  (Fmap : ∀ (A B : Type) [CommRing A] [CommRing B] [Algebra R A] [Algebra R B], (A →ₐ[R] B) → F A →
    F B)
  {X : Scheme.{0}} (p : X ⟶ Spec (CommRingCat.of R))
  (pt : ∀ (A : Type) [CommRing A] [Algebra R A],
    F A ≃ {g : Spec (CommRingCat.of A) ⟶ X // g ≫ p = Spec.map (CommRingCat.ofHom (algebraMap R
      A))})
  (W : ∀ (A : Type) [CommRing A] [Algebra R A], F A → Prop)
variable {F Fmap p pt W}

Lean source · statement

theorem Fmap_id (hn : PtNatural F Fmap p pt) (A : Type) [CommRing A] [Algebra R A] (s : F A) :
    Fmap A A (AlgHom.id R A) s = s

theorem

Fmap_comp

L107 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isClosedImmersion_represents_of_forall_exists_ideal.ClosedRep.Fmap_comp

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_represents_of_forall_exists_ideal
open CategoryTheory AlgebraicGeometry Opposite
namespace ClosedRep
universe u
section Setting
variable {R : Type} [CommRing R]
  (F : ∀ (A : Type) [CommRing A] [Algebra R A], Type)
  (Fmap : ∀ (A B : Type) [CommRing A] [CommRing B] [Algebra R A] [Algebra R B], (A →ₐ[R] B) → F A →
    F B)
  {X : Scheme.{0}} (p : X ⟶ Spec (CommRingCat.of R))
  (pt : ∀ (A : Type) [CommRing A] [Algebra R A],
    F A ≃ {g : Spec (CommRingCat.of A) ⟶ X // g ≫ p = Spec.map (CommRingCat.ofHom (algebraMap R
      A))})
  (W : ∀ (A : Type) [CommRing A] [Algebra R A], F A → Prop)
variable {F Fmap p pt W}

Lean source · statement

theorem Fmap_comp (hn : PtNatural F Fmap p pt) (A B C : Type) [CommRing A] [CommRing B] [CommRing C]
    [Algebra R A] [Algebra R B] [Algebra R C] (φ : A →ₐ[R] B) (ψ : B →ₐ[R] C) (s : F A) :
    Fmap B C ψ (Fmap A B φ s) = Fmap A C (ψ.comp φ) s

theorem

eq_of_pt_eq

L115 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isClosedImmersion_represents_of_forall_exists_ideal.ClosedRep.eq_of_pt_eq

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_represents_of_forall_exists_ideal
open CategoryTheory AlgebraicGeometry Opposite
namespace ClosedRep
universe u
section Setting
variable {R : Type} [CommRing R]
  (F : ∀ (A : Type) [CommRing A] [Algebra R A], Type)
  (Fmap : ∀ (A B : Type) [CommRing A] [CommRing B] [Algebra R A] [Algebra R B], (A →ₐ[R] B) → F A →
    F B)
  {X : Scheme.{0}} (p : X ⟶ Spec (CommRingCat.of R))
  (pt : ∀ (A : Type) [CommRing A] [Algebra R A],
    F A ≃ {g : Spec (CommRingCat.of A) ⟶ X // g ≫ p = Spec.map (CommRingCat.ofHom (algebraMap R
      A))})
  (W : ∀ (A : Type) [CommRing A] [Algebra R A], F A → Prop)
variable {F Fmap p pt W}

Lean source · statement

theorem eq_of_pt_eq (A : Type) [CommRing A] [Algebra R A] (s t : F A) (h : (pt A s).1 = (pt A t).1)
  : s = t

def

cl

L120 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isClosedImmersion_represents_of_forall_exists_ideal.ClosedRep.cl

Documentation

The chosen ideal cutting out the subfunctor condition at an algebra-valued point.

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_represents_of_forall_exists_ideal
open CategoryTheory AlgebraicGeometry Opposite
namespace ClosedRep
universe u
section Setting
variable {R : Type} [CommRing R]
  (F : ∀ (A : Type) [CommRing A] [Algebra R A], Type)
  (Fmap : ∀ (A B : Type) [CommRing A] [CommRing B] [Algebra R A] [Algebra R B], (A →ₐ[R] B) → F A →
    F B)
  {X : Scheme.{0}} (p : X ⟶ Spec (CommRingCat.of R))
  (pt : ∀ (A : Type) [CommRing A] [Algebra R A],
    F A ≃ {g : Spec (CommRingCat.of A) ⟶ X // g ≫ p = Spec.map (CommRingCat.ofHom (algebraMap R
      A))})
  (W : ∀ (A : Type) [CommRing A] [Algebra R A], F A → Prop)
variable {F Fmap p pt W}

Lean source · statement

def cl (hc : Closed F Fmap W) (A : Type) [CommRing A] [Algebra R A] (s : F A) : Ideal
  A

theorem

cl_spec

L124 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isClosedImmersion_represents_of_forall_exists_ideal.ClosedRep.cl_spec

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_represents_of_forall_exists_ideal
open CategoryTheory AlgebraicGeometry Opposite
namespace ClosedRep
universe u
section Setting
variable {R : Type} [CommRing R]
  (F : ∀ (A : Type) [CommRing A] [Algebra R A], Type)
  (Fmap : ∀ (A B : Type) [CommRing A] [CommRing B] [Algebra R A] [Algebra R B], (A →ₐ[R] B) → F A →
    F B)
  {X : Scheme.{0}} (p : X ⟶ Spec (CommRingCat.of R))
  (pt : ∀ (A : Type) [CommRing A] [Algebra R A],
    F A ≃ {g : Spec (CommRingCat.of A) ⟶ X // g ≫ p = Spec.map (CommRingCat.ofHom (algebraMap R
      A))})
  (W : ∀ (A : Type) [CommRing A] [Algebra R A], F A → Prop)
variable {F Fmap p pt W}

Lean source · statement

theorem cl_spec (hc : Closed F Fmap W) (A : Type) [CommRing A] [Algebra R A] (s : F A)
    (B : Type) [CommRing B] [Algebra R B] (φ : A →ₐ[R] B) :
    W B (Fmap A B φ s) ↔ ∀ a ∈ cl hc A s, φ a = 0

theorem

ideal_unique

L129 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isClosedImmersion_represents_of_forall_exists_ideal.ClosedRep.ideal_unique

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_represents_of_forall_exists_ideal
open CategoryTheory AlgebraicGeometry Opposite
namespace ClosedRep
universe u
section Setting
variable {R : Type} [CommRing R]
  (F : ∀ (A : Type) [CommRing A] [Algebra R A], Type)
  (Fmap : ∀ (A B : Type) [CommRing A] [CommRing B] [Algebra R A] [Algebra R B], (A →ₐ[R] B) → F A →
    F B)
  {X : Scheme.{0}} (p : X ⟶ Spec (CommRingCat.of R))
  (pt : ∀ (A : Type) [CommRing A] [Algebra R A],
    F A ≃ {g : Spec (CommRingCat.of A) ⟶ X // g ≫ p = Spec.map (CommRingCat.ofHom (algebraMap R
      A))})
  (W : ∀ (A : Type) [CommRing A] [Algebra R A], F A → Prop)
variable {F Fmap p pt W}

Lean source · statement

theorem ideal_unique (A : Type) [CommRing A] [Algebra R A] (𝔞 𝔟 : Ideal A)
    (P : ∀ (B : Type) [CommRing B] [Algebra R B], (A →ₐ[R] B) → Prop)
    (h𝔞 : ∀ (B : Type) [CommRing B] [Algebra R B] (φ : A →ₐ[R] B), P B φ ↔ ∀ a ∈ 𝔞, φ a = 0)
    (h𝔟 : ∀ (B : Type) [CommRing B] [Algebra R B] (φ : A →ₐ[R] B), P B φ ↔ ∀ a ∈ 𝔟, φ a = 0) :
    𝔞 = 𝔟

theorem

W_iff_cl_eq_bot

L146 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isClosedImmersion_represents_of_forall_exists_ideal.ClosedRep.W_iff_cl_eq_bot

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_represents_of_forall_exists_ideal
open CategoryTheory AlgebraicGeometry Opposite
namespace ClosedRep
universe u
section Setting
variable {R : Type} [CommRing R]
  (F : ∀ (A : Type) [CommRing A] [Algebra R A], Type)
  (Fmap : ∀ (A B : Type) [CommRing A] [CommRing B] [Algebra R A] [Algebra R B], (A →ₐ[R] B) → F A →
    F B)
  {X : Scheme.{0}} (p : X ⟶ Spec (CommRingCat.of R))
  (pt : ∀ (A : Type) [CommRing A] [Algebra R A],
    F A ≃ {g : Spec (CommRingCat.of A) ⟶ X // g ≫ p = Spec.map (CommRingCat.ofHom (algebraMap R
      A))})
  (W : ∀ (A : Type) [CommRing A] [Algebra R A], F A → Prop)
variable {F Fmap p pt W}

Lean source · statement

theorem W_iff_cl_eq_bot (hn : PtNatural F Fmap p pt) (hc : Closed F Fmap W) (A : Type) [CommRing A]
    [Algebra R A] (s : F A) : W A s ↔ cl hc A s = ⊥

theorem

cl_map

L153 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isClosedImmersion_represents_of_forall_exists_ideal.ClosedRep.cl_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_represents_of_forall_exists_ideal
open CategoryTheory AlgebraicGeometry Opposite
namespace ClosedRep
universe u
section Setting
variable {R : Type} [CommRing R]
  (F : ∀ (A : Type) [CommRing A] [Algebra R A], Type)
  (Fmap : ∀ (A B : Type) [CommRing A] [CommRing B] [Algebra R A] [Algebra R B], (A →ₐ[R] B) → F A →
    F B)
  {X : Scheme.{0}} (p : X ⟶ Spec (CommRingCat.of R))
  (pt : ∀ (A : Type) [CommRing A] [Algebra R A],
    F A ≃ {g : Spec (CommRingCat.of A) ⟶ X // g ≫ p = Spec.map (CommRingCat.ofHom (algebraMap R
      A))})
  (W : ∀ (A : Type) [CommRing A] [Algebra R A], F A → Prop)
variable {F Fmap p pt W}

Lean source · statement

theorem cl_map (hn : PtNatural F Fmap p pt) (hc : Closed F Fmap W) (A B : Type) [CommRing A]
  [CommRing B]
    [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) (s : F A) :
    cl hc B (Fmap A B φ s) = (cl hc A s).map φ.toRingHom

def

ρ

L178 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isClosedImmersion_represents_of_forall_exists_ideal.ClosedRep.ρ

Documentation

The structure homomorphism from the base ring to sections on an affine open.

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_represents_of_forall_exists_ideal
open CategoryTheory AlgebraicGeometry Opposite
namespace ClosedRep
universe u
section Charts
variable {R : Type} [CommRing R] {X : Scheme.{0}} (p : X ⟶ Spec (CommRingCat.of R))

Lean source · statement

def ρ (U : X.affineOpens) : CommRingCat.of R ⟶ Γ(X, U)

def

algU

L182 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isClosedImmersion_represents_of_forall_exists_ideal.ClosedRep.algU

Documentation

The base-ring algebra structure on sections of an affine open.

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_represents_of_forall_exists_ideal
open CategoryTheory AlgebraicGeometry Opposite
namespace ClosedRep
universe u
section Charts
variable {R : Type} [CommRing R] {X : Scheme.{0}} (p : X ⟶ Spec (CommRingCat.of R))

Lean source · statement

def algU (U : X.affineOpens) : Algebra R Γ(X, U)

theorem

fromSpec_over

L184 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isClosedImmersion_represents_of_forall_exists_ideal.ClosedRep.fromSpec_over

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_represents_of_forall_exists_ideal
open CategoryTheory AlgebraicGeometry Opposite
namespace ClosedRep
universe u
section Charts
variable {R : Type} [CommRing R] {X : Scheme.{0}} (p : X ⟶ Spec (CommRingCat.of R))

Lean source · full declaration

theorem fromSpec_over (U : X.affineOpens) :
    letI := algU p U
    U.2.fromSpec ≫ p = Spec.map (CommRingCat.ofHom (algebraMap R Γ(X, U))) := by
  change _ = Spec.map (ρ p U)
  rw [ρ, Spec.map_preimage]

abbrev

Da

L191 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isClosedImmersion_represents_of_forall_exists_ideal.ClosedRep.Da

Documentation

The basic open in an affine spectrum defined by the given ring element.

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_represents_of_forall_exists_ideal
open CategoryTheory AlgebraicGeometry Opposite
namespace ClosedRep
universe u
section Charts
variable {R : Type} [CommRing R] {X : Scheme.{0}} (p : X ⟶ Spec (CommRingCat.of R))

Lean source · statement

abbrev Da (A : Type) [CommRing A] (a : A) : (Spec (CommRingCat.of A)).Opens

theorem

isAffineOpen_Da

L194 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isClosedImmersion_represents_of_forall_exists_ideal.ClosedRep.isAffineOpen_Da

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_represents_of_forall_exists_ideal
open CategoryTheory AlgebraicGeometry Opposite
namespace ClosedRep
universe u
section Charts
variable {R : Type} [CommRing R] {X : Scheme.{0}} (p : X ⟶ Spec (CommRingCat.of R))

Lean source · statement

theorem isAffineOpen_Da (A : Type) [CommRing A] (a : A) : IsAffineOpen (Da A a)

def

θ'

L198 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isClosedImmersion_represents_of_forall_exists_ideal.ClosedRep.θ'

Documentation

The homomorphism from the affine ring to sections on its basic open.

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_represents_of_forall_exists_ideal
open CategoryTheory AlgebraicGeometry Opposite
namespace ClosedRep
universe u
section Charts
variable {R : Type} [CommRing R] {X : Scheme.{0}} (p : X ⟶ Spec (CommRingCat.of R))

Lean source · statement

def θ' (A : Type) [CommRing A] (a : A) : CommRingCat.of A ⟶ Γ(Spec (CommRingCat.of
  A), Da A a)

theorem

θ'_apply

L203 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isClosedImmersion_represents_of_forall_exists_ideal.ClosedRep.θ'_apply

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_represents_of_forall_exists_ideal
open CategoryTheory AlgebraicGeometry Opposite
namespace ClosedRep
universe u
section Charts
variable {R : Type} [CommRing R] {X : Scheme.{0}} (p : X ⟶ Spec (CommRingCat.of R))

Lean source · statement

theorem θ'_apply (A : Type) [CommRing A] (a : A) (x : A) :
    (θ' A a).hom x = ((Spec (CommRingCat.of A)).presheaf.map (homOfLE le_top).op).hom
      ((Scheme.ΓSpecIso (CommRingCat.of A)).inv.hom x)

def

algL

L208 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isClosedImmersion_represents_of_forall_exists_ideal.ClosedRep.algL

Documentation

The base-ring algebra structure on sections of the basic open.

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_represents_of_forall_exists_ideal
open CategoryTheory AlgebraicGeometry Opposite
namespace ClosedRep
universe u
section Charts
variable {R : Type} [CommRing R] {X : Scheme.{0}} (p : X ⟶ Spec (CommRingCat.of R))

Lean source · statement

def algL (A : Type) [CommRing A] [Algebra R A] (a : A) :
    Algebra R Γ(Spec (CommRingCat.of A), Da A a)

def

θ

L213 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isClosedImmersion_represents_of_forall_exists_ideal.ClosedRep.θ

Documentation

The restriction to a basic open viewed as a homomorphism of algebras over the base.

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_represents_of_forall_exists_ideal
open CategoryTheory AlgebraicGeometry Opposite
namespace ClosedRep
universe u
section Charts
variable {R : Type} [CommRing R] {X : Scheme.{0}} (p : X ⟶ Spec (CommRingCat.of R))

Lean source · full declaration

def θ (A : Type) [CommRing A] [Algebra R A] (a : A) :
    letI := algL (R := R) A a
    A →ₐ[R] Γ(Spec (CommRingCat.of A), Da A a) :=
  letI := algL (R := R) A a
  { (θ' A a).hom with commutes' := fun _ => rfl }

theorem

fromSpec_Da

L219 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isClosedImmersion_represents_of_forall_exists_ideal.ClosedRep.fromSpec_Da

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_represents_of_forall_exists_ideal
open CategoryTheory AlgebraicGeometry Opposite
namespace ClosedRep
universe u
section Charts
variable {R : Type} [CommRing R] {X : Scheme.{0}} (p : X ⟶ Spec (CommRingCat.of R))

Lean source · statement

theorem fromSpec_Da (A : Type) [CommRing A] (a : A) : (isAffineOpen_Da A a).fromSpec = Spec.map (θ'
  A a)

def

sU

L242 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isClosedImmersion_represents_of_forall_exists_ideal.ClosedRep.sU

Documentation

The functor element corresponding to the canonical affine chart of the representing scheme.

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_represents_of_forall_exists_ideal
open CategoryTheory AlgebraicGeometry Opposite
namespace ClosedRep
universe u
section Sheaf
variable {R : Type} [CommRing R]
  {F : ∀ (A : Type) [CommRing A] [Algebra R A], Type}
  {Fmap : ∀ (A B : Type) [CommRing A] [CommRing B] [Algebra R A] [Algebra R B], (A →ₐ[R] B) → F A →
    F B}
  {X : Scheme.{0}} {p : X ⟶ Spec (CommRingCat.of R)}
  {pt : ∀ (A : Type) [CommRing A] [Algebra R A],
    F A ≃ {g : Spec (CommRingCat.of A) ⟶ X // g ≫ p = Spec.map (CommRingCat.ofHom (algebraMap R
      A))}}
  {W : ∀ (A : Type) [CommRing A] [Algebra R A], F A → Prop}
  (hn : PtNatural F Fmap p pt) (hc : Closed F Fmap W)
variable (pt) in

Lean source · full declaration

def sU (U : X.affineOpens) : letI := algU p U; F Γ(X, U) :=
  letI := algU p U
  (pt Γ(X, U)).symm ⟨U.2.fromSpec, fromSpec_over p U⟩

theorem

pt_sU

L246 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isClosedImmersion_represents_of_forall_exists_ideal.ClosedRep.pt_sU

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_represents_of_forall_exists_ideal
open CategoryTheory AlgebraicGeometry Opposite
namespace ClosedRep
universe u
section Sheaf
variable {R : Type} [CommRing R]
  {F : ∀ (A : Type) [CommRing A] [Algebra R A], Type}
  {Fmap : ∀ (A B : Type) [CommRing A] [CommRing B] [Algebra R A] [Algebra R B], (A →ₐ[R] B) → F A →
    F B}
  {X : Scheme.{0}} {p : X ⟶ Spec (CommRingCat.of R)}
  {pt : ∀ (A : Type) [CommRing A] [Algebra R A],
    F A ≃ {g : Spec (CommRingCat.of A) ⟶ X // g ≫ p = Spec.map (CommRingCat.ofHom (algebraMap R
      A))}}
  {W : ∀ (A : Type) [CommRing A] [Algebra R A], F A → Prop}
  (hn : PtNatural F Fmap p pt) (hc : Closed F Fmap W)
variable (pt) in

Lean source · full declaration

theorem pt_sU (U : X.affineOpens) : letI := algU p U; (pt Γ(X, U) (sU pt U)).1 = U.2.fromSpec := by
  let _ := algU p U
  change (pt Γ(X, U) ((pt Γ(X, U)).symm _)).1 = _
  rw [Equiv.apply_symm_apply]

def

resAlg

L253 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isClosedImmersion_represents_of_forall_exists_ideal.ClosedRep.resAlg

Documentation

The algebra restriction homomorphism between affine opens of the representing scheme.

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_represents_of_forall_exists_ideal
open CategoryTheory AlgebraicGeometry Opposite
namespace ClosedRep
universe u
section Sheaf
variable {R : Type} [CommRing R]
  {F : ∀ (A : Type) [CommRing A] [Algebra R A], Type}
  {Fmap : ∀ (A B : Type) [CommRing A] [CommRing B] [Algebra R A] [Algebra R B], (A →ₐ[R] B) → F A →
    F B}
  {X : Scheme.{0}} {p : X ⟶ Spec (CommRingCat.of R)}
  {pt : ∀ (A : Type) [CommRing A] [Algebra R A],
    F A ≃ {g : Spec (CommRingCat.of A) ⟶ X // g ≫ p = Spec.map (CommRingCat.ofHom (algebraMap R
      A))}}
  {W : ∀ (A : Type) [CommRing A] [Algebra R A], F A → Prop}
  (hn : PtNatural F Fmap p pt) (hc : Closed F Fmap W)
variable (pt) in
variable (p) in

Lean source · full declaration

def resAlg (U V : X.affineOpens) (h : V.1 ≤ U.1) :
    letI := algU p U; letI := algU p V; Γ(X, U) →ₐ[R] Γ(X, V) :=
  letI := algU p U; letI := algU p V
  algHomOfSpec (X.presheaf.map (homOfLE h).op).hom (by
    change Spec.map (X.presheaf.map (homOfLE h).op) ≫ Spec.map (ρ p U) = Spec.map (ρ p V)
    rw [ρ, ρ, Spec.map_preimage, Spec.map_preimage, ← Category.assoc, IsAffineOpen.map_fromSpec U.2
      V.2])

theorem

Fmap_resAlg_sU

L261 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isClosedImmersion_represents_of_forall_exists_ideal.ClosedRep.Fmap_resAlg_sU

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isClosedImmersion_represents_of_forall_exists_ideal
open CategoryTheory AlgebraicGeometry Opposite
namespace ClosedRep
universe u
section Sheaf
variable {R : Type} [CommRing R]
  {F : ∀ (A : Type) [CommRing A] [Algebra R A], Type}
  {Fmap : ∀ (A B : Type) [CommRing A] [CommRing B] [Algebra R A] [Algebra R B], (A →ₐ[R] B) → F A →
    F B}
  {X : Scheme.{0}} {p : X ⟶ Spec (CommRingCat.of R)}
  {pt : ∀ (A : Type) [CommRing A] [Algebra R A],
    F A ≃ {g : Spec (CommRingCat.of A) ⟶ X // g ≫ p = Spec.map (CommRingCat.ofHom (algebraMap R
      A))}}
  {W : ∀ (A : Type) [CommRing A] [Algebra R A], F A → Prop}
  (hn : PtNatural F Fmap p pt) (hc : Closed F Fmap W)
variable (pt) in
variable (p) in
include hn in

Lean source · full declaration

theorem Fmap_resAlg_sU (U V : X.affineOpens) (h : V.1 ≤ U.1) :
    letI := algU p U; letI := algU p V
    Fmap Γ(X, U) Γ(X, V) (resAlg p U V h) (sU pt U) = sU pt V := by
  let _ := algU p U; let _ := algU p V
  apply eq_of_pt_eq (pt := pt)
  rw [hn, pt_sU, pt_sU]
  exact IsAffineOpen.map_fromSpec U.2 V.2 (homOfLE h).op

def

J

L270 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isClosedImmersion_represents_of_forall_exists_ideal.ClosedRep.J

Documentation

The ideal sheaf obtained by gluing the ideals cutting out the subfunctor on affine charts.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isClosedImmersion_represents_of_forall_exists_ideal
open CategoryTheory AlgebraicGeometry Opposite
namespace ClosedRep
universe u
section Sheaf
variable {R : Type} [CommRing R]
  {F : ∀ (A : Type) [CommRing A] [Algebra R A], Type}
  {Fmap : ∀ (A B : Type) [CommRing A] [CommRing B] [Algebra R A] [Algebra R B], (A →ₐ[R] B) → F A →
    F B}
  {X : Scheme.{0}} {p : X ⟶ Spec (CommRingCat.of R)}
  {pt : ∀ (A : Type) [CommRing A] [Algebra R A],
    F A ≃ {g : Spec (CommRingCat.of A) ⟶ X // g ≫ p = Spec.map (CommRingCat.ofHom (algebraMap R
      A))}}
  {W : ∀ (A : Type) [CommRing A] [Algebra R A], F A → Prop}
  (hn : PtNatural F Fmap p pt) (hc : Closed F Fmap W)
variable (pt) in
variable (p) in
include hn in

Lean source · full declaration

def J : X.IdealSheafData where
  ideal U := letI := algU p U; cl hc Γ(X, U) (sU pt U)
  map_ideal_basicOpen U f := by
    let _ := algU p U; let _ := algU p (X.affineBasicOpen f)
    have h := cl_map hn hc Γ(X, U) Γ(X, X.affineBasicOpen f)
      (resAlg p U (X.affineBasicOpen f) (X.basicOpen_le f)) (sU pt U)
    erw [Fmap_resAlg_sU hn U (X.affineBasicOpen f) (X.basicOpen_le f)] at h
    exact h.symm

theorem

local_iff

L284 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isClosedImmersion_represents_of_forall_exists_ideal.ClosedRep.local_iff

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isClosedImmersion_represents_of_forall_exists_ideal
open CategoryTheory AlgebraicGeometry Opposite
namespace ClosedRep
universe u
section Sheaf
variable {R : Type} [CommRing R]
  {F : ∀ (A : Type) [CommRing A] [Algebra R A], Type}
  {Fmap : ∀ (A B : Type) [CommRing A] [CommRing B] [Algebra R A] [Algebra R B], (A →ₐ[R] B) → F A →
    F B}
  {X : Scheme.{0}} {p : X ⟶ Spec (CommRingCat.of R)}
  {pt : ∀ (A : Type) [CommRing A] [Algebra R A],
    F A ≃ {g : Spec (CommRingCat.of A) ⟶ X // g ≫ p = Spec.map (CommRingCat.ofHom (algebraMap R
      A))}}
  {W : ∀ (A : Type) [CommRing A] [Algebra R A], F A → Prop}
  (hn : PtNatural F Fmap p pt) (hc : Closed F Fmap W)
variable (pt) in
variable (p) in
section Key
variable (A : Type) [CommRing A] [Algebra R A] (s : F A)
include hn in

Lean source · full declaration

theorem local_iff (U : X.affineOpens) (a : A) (ha : Da A a ≤ (pt A s).1 ⁻¹ᵁ U.1) :
    letI := algU p U
    (∀ x ∈ cl hc Γ(X, U) (sU pt U), ((pt A s).1.appLE U.1 (Da A a) ha).hom x = 0) ↔
      ∀ x ∈ cl hc A s, (θ' A a).hom x = 0 := by
  let _ := algU p U; let _ := algL (R := R) A a
  let g := (pt A s).1
  have hg : g ≫ p = Spec.map (CommRingCat.ofHom (algebraMap R A)) := (pt A s).2
  let ψ' : Γ(X, U.1) ⟶ Γ(Spec (CommRingCat.of A), Da A a) := g.appLE U.1 (Da A a) ha
  have hP1 : Spec.map ψ' ≫ U.2.fromSpec = (isAffineOpen_Da A a).fromSpec ≫ g :=
    IsAffineOpen.SpecMap_appLE_fromSpec g U.2 (isAffineOpen_Da A a) ha
  let ψ : Γ(X, U) →ₐ[R] Γ(Spec (CommRingCat.of A), Da A a) := algHomOfSpec ψ'.hom (by
    change Spec.map ψ' ≫ Spec.map (ρ p U) = Spec.map (CommRingCat.ofHom ((θ' A a).hom.comp
      (algebraMap R A)))
    rw [ρ, Spec.map_preimage, ← Category.assoc, hP1, Category.assoc, hg, fromSpec_Da, ←
      Spec.map_comp,
      CommRingCat.ofHom_comp, CommRingCat.ofHom_hom])
  have hP2 : Fmap Γ(X, U) Γ(Spec (CommRingCat.of A), Da A a) ψ (sU pt U) =
      Fmap A Γ(Spec (CommRingCat.of A), Da A a) (θ (R := R) A a) s := by
    apply eq_of_pt_eq (pt := pt)
    rw [hn, hn, pt_sU]
    change Spec.map ψ' ≫ U.2.fromSpec = Spec.map (θ' A a) ≫ (pt A s).1
    rw [hP1, fromSpec_Da]
  have h1 := cl_spec hc Γ(X, U) (sU pt U) Γ(Spec (CommRingCat.of A), Da A a) ψ
  have h2 := cl_spec hc A s Γ(Spec (CommRingCat.of A), Da A a) (θ (R := R) A a)
  rw [hP2, h2] at h1
  exact h1.symm

theorem

preimage_le_iSup

L311 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isClosedImmersion_represents_of_forall_exists_ideal.ClosedRep.preimage_le_iSup

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isClosedImmersion_represents_of_forall_exists_ideal
open CategoryTheory AlgebraicGeometry Opposite
namespace ClosedRep
universe u
section Sheaf
variable {R : Type} [CommRing R]
  {F : ∀ (A : Type) [CommRing A] [Algebra R A], Type}
  {Fmap : ∀ (A B : Type) [CommRing A] [CommRing B] [Algebra R A] [Algebra R B], (A →ₐ[R] B) → F A →
    F B}
  {X : Scheme.{0}} {p : X ⟶ Spec (CommRingCat.of R)}
  {pt : ∀ (A : Type) [CommRing A] [Algebra R A],
    F A ≃ {g : Spec (CommRingCat.of A) ⟶ X // g ≫ p = Spec.map (CommRingCat.ofHom (algebraMap R
      A))}}
  {W : ∀ (A : Type) [CommRing A] [Algebra R A], F A → Prop}
  (hn : PtNatural F Fmap p pt) (hc : Closed F Fmap W)
variable (pt) in
variable (p) in
section Key
variable (A : Type) [CommRing A] [Algebra R A] (s : F A)

Lean source · statement

theorem preimage_le_iSup (g : Spec (CommRingCat.of A) ⟶ X) (U : X.Opens) :
    g ⁻¹ᵁ U ≤ ⨆ a : {a : A // Da A a ≤ g ⁻¹ᵁ U}, Da A a.1

theorem

J_le_ker_iff

L326 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isClosedImmersion_represents_of_forall_exists_ideal.ClosedRep.J_le_ker_iff

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isClosedImmersion_represents_of_forall_exists_ideal
open CategoryTheory AlgebraicGeometry Opposite
namespace ClosedRep
universe u
section Sheaf
variable {R : Type} [CommRing R]
  {F : ∀ (A : Type) [CommRing A] [Algebra R A], Type}
  {Fmap : ∀ (A B : Type) [CommRing A] [CommRing B] [Algebra R A] [Algebra R B], (A →ₐ[R] B) → F A →
    F B}
  {X : Scheme.{0}} {p : X ⟶ Spec (CommRingCat.of R)}
  {pt : ∀ (A : Type) [CommRing A] [Algebra R A],
    F A ≃ {g : Spec (CommRingCat.of A) ⟶ X // g ≫ p = Spec.map (CommRingCat.ofHom (algebraMap R
      A))}}
  {W : ∀ (A : Type) [CommRing A] [Algebra R A], F A → Prop}
  (hn : PtNatural F Fmap p pt) (hc : Closed F Fmap W)
variable (pt) in
variable (p) in
section Key
variable (A : Type) [CommRing A] [Algebra R A] (s : F A)
include hn in

Lean source · statement

theorem J_le_ker_iff : J hn hc ≤ (pt A s).1.ker ↔ W A s

theorem

main

L369 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_isClosedImmersion_represents_of_forall_exists_ideal.ClosedRep.main

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_represents_of_forall_exists_ideal
open CategoryTheory AlgebraicGeometry Opposite
namespace ClosedRep
universe u

Lean source · statement

theorem main (R : Type) [CommRing R]
    (F : ∀ (A : Type) [CommRing A] [Algebra R A], Type)
    (Fmap : ∀ (A B : Type) [CommRing A] [CommRing B] [Algebra R A] [Algebra R B],
      (A →ₐ[R] B) → F A → F B)
    (X : Scheme.{0}) (p : X ⟶ Spec (CommRingCat.of R))
    (pt : ∀ (A : Type) [CommRing A] [Algebra R A],
      F A ≃ {g : Spec (CommRingCat.of A) ⟶ X // g ≫ p = Spec.map (CommRingCat.ofHom (algebraMap R
        A))})
    (pt_natural : ∀ (A B : Type) [CommRing A] [CommRing B] [Algebra R A] [Algebra R B]
      (φ : A →ₐ[R] B) (s : F A),
      (pt B (Fmap A B φ s)).1 = Spec.map (CommRingCat.ofHom φ.toRingHom) ≫ (pt A s).1)
    (W : ∀ (A : Type) [CommRing A] [Algebra R A], F A → Prop)
    (closed : ∀ (A : Type) [CommRing A] [Algebra R A] (s : F A), ∃ 𝔞 : Ideal A,
      ∀ (B : Type) [CommRing B] [Algebra R B] (φ : A →ₐ[R] B),
        W B (Fmap A B φ s) ↔ ∀ a ∈ 𝔞, φ a = 0) :
    ∃ (Z : Scheme.{0}) (ι : Z ⟶ X)
      (ptZ : ∀ (A : Type) [CommRing A] [Algebra R A],
        {s : F A // W A s} ≃
          {g : Spec (CommRingCat.of A) ⟶ Z //
            g ≫ ι ≫ p = Spec.map (CommRingCat.ofHom (algebraMap R A))}),
      IsClosedImmersion ι ∧
      ∀ (A : Type) [CommRing A] [Algebra R A] (s : {s : F A // W A s}),
        (ptZ A s).1 ≫ ι = (pt A s.1).1

theorem

exists_isClosedImmersion_represents_of_forall_exists_ideal

L439 ↗

AlgebraicGeometry.Scheme.exists_isClosedImmersion_represents_of_forall_exists_ideal

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_isClosedImmersion_represents_of_forall_exists_ideal
open CategoryTheory AlgebraicGeometry Opposite
attribute [local simp] ClosedRep.algHomOfSpec_toRingHom

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.exists_isClosedImmersion_represents_of_forall_exists_ideal
    (R : Type) [CommRing R]
    (F : ∀ (A : Type) [CommRing A] [Algebra R A], Type)
    (Fmap : ∀ (A B : Type) [CommRing A] [CommRing B] [Algebra R A] [Algebra R B],
      (A →ₐ[R] B) → F A → F B)
    (X : Scheme.{0}) (p : X ⟶ Spec (CommRingCat.of R))
    (pt : ∀ (A : Type) [CommRing A] [Algebra R A],
      F A ≃ {g : Spec (CommRingCat.of A) ⟶ X // g ≫ p = Spec.map (CommRingCat.ofHom (algebraMap R
        A))})
    (pt_natural : ∀ (A B : Type) [CommRing A] [CommRing B] [Algebra R A] [Algebra R B]
      (φ : A →ₐ[R] B) (s : F A),
      (pt B (Fmap A B φ s)).1 = Spec.map (CommRingCat.ofHom φ.toRingHom) ≫ (pt A s).1)
    (W : ∀ (A : Type) [CommRing A] [Algebra R A], F A → Prop)
    (closed : ∀ (A : Type) [CommRing A] [Algebra R A] (s : F A), ∃ 𝔞 : Ideal A,
      ∀ (B : Type) [CommRing B] [Algebra R B] (φ : A →ₐ[R] B),
        W B (Fmap A B φ s) ↔ ∀ a ∈ 𝔞, φ a = 0) :
    ∃ (Z : Scheme.{0}) (ι : Z ⟶ X)
      (ptZ : ∀ (A : Type) [CommRing A] [Algebra R A],
        {s : F A // W A s} ≃
          {g : Spec (CommRingCat.of A) ⟶ Z //
            g ≫ ι ≫ p = Spec.map (CommRingCat.ofHom (algebraMap R A))}),
      IsClosedImmersion ι ∧
      ∀ (A : Type) [CommRing A] [Algebra R A] (s : {s : F A // W A s}),
        (ptZ A s).1 ≫ ι = (pt A s.1).1

Module documentation

Scheme exists is Closed Immersion represents of forall exists ideal

Declarations