NYLL
Module

Scheme_exists_represents_of_zariskiSheaf_of_openAffineCover.lean

Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_exists_represents_of_zariskiSheaf_of_openAffineCover
11 declarations indexed from sourceView source ↗

Module documentation

Scheme exists represents of zariski Sheaf of open Affine Cover

Imports16
Imported by1

Declarations

abbrev

strMap

L51 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_represents_of_zariskiSheaf_of_openAffineCover.GrassBridgeS1.strMap
Documentation

The spectrum morphism associated with the given algebra structure.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_represents_of_zariskiSheaf_of_openAffineCover
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeS1
variable {R : Type} [CommRing R]
Lean source · statement
abbrev strMap (A : Type) [CommRing A] [Algebra R A] :
    Spec (CommRingCat.of A) ⟶ Spec (CommRingCat.of R)
lemma

spec_comp_strMap

L55 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_represents_of_zariskiSheaf_of_openAffineCover.GrassBridgeS1.spec_comp_strMap
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_represents_of_zariskiSheaf_of_openAffineCover
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeS1
variable {R : Type} [CommRing R]
Lean source · statement
lemma spec_comp_strMap {A B : Type} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B]
    (φ : A →ₐ[R] B) : Spec.map (CommRingCat.ofHom φ.toRingHom) ≫ strMap (R := R) A = strMap B
abbrev

Pts

L70 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_represents_of_zariskiSheaf_of_openAffineCover.GrassBridgeS1.Pts
Documentation

The points of the representing scheme over the specified algebra structure.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_represents_of_zariskiSheaf_of_openAffineCover
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeS1
variable {R : Type} [CommRing R]
section pts
variable (G : (Over (Spec (CommRingCat.of R)))ᵒᵖ ⥤ Type) {X : Scheme.{0}}
  (e : G.overTotal.RepresentableBy X)
  (F : ∀ (A : Type) [CommRing A] [Algebra R A], Type)
  (ev : ∀ (A : Type) [CommRing A] [Algebra R A],
    F A ≃ G.obj (op (Over.mk (Spec.map (CommRingCat.ofHom (algebraMap R A))))))
Lean source · statement
abbrev Pts (A : Type) [CommRing A] [Algebra R A] : Type
def

toPts

L76 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_represents_of_zariskiSheaf_of_openAffineCover.GrassBridgeS1.toPts
Documentation

The point of the representing scheme associated with an element of the functor.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_represents_of_zariskiSheaf_of_openAffineCover
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeS1
variable {R : Type} [CommRing R]
section pts
variable (G : (Over (Spec (CommRingCat.of R)))ᵒᵖ ⥤ Type) {X : Scheme.{0}}
  (e : G.overTotal.RepresentableBy X)
  (F : ∀ (A : Type) [CommRing A] [Algebra R A], Type)
  (ev : ∀ (A : Type) [CommRing A] [Algebra R A],
    F A ≃ G.obj (op (Over.mk (Spec.map (CommRingCat.ofHom (algebraMap R A))))))
variable (A : Type) [CommRing A] [Algebra R A]
Lean source · statement
def toPts (s : F A) : Pts G e A
def

ofPts

L85 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_represents_of_zariskiSheaf_of_openAffineCover.GrassBridgeS1.ofPts
Documentation

The element of the functor associated with a point over the base.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_represents_of_zariskiSheaf_of_openAffineCover
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeS1
variable {R : Type} [CommRing R]
section pts
variable (G : (Over (Spec (CommRingCat.of R)))ᵒᵖ ⥤ Type) {X : Scheme.{0}}
  (e : G.overTotal.RepresentableBy X)
  (F : ∀ (A : Type) [CommRing A] [Algebra R A], Type)
  (ev : ∀ (A : Type) [CommRing A] [Algebra R A],
    F A ≃ G.obj (op (Over.mk (Spec.map (CommRingCat.ofHom (algebraMap R A))))))
variable (A : Type) [CommRing A] [Algebra R A]
Lean source · statement
def ofPts (g : Pts G e A) : F A
lemma

ofPts_toPts

L89 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_represents_of_zariskiSheaf_of_openAffineCover.GrassBridgeS1.ofPts_toPts
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_represents_of_zariskiSheaf_of_openAffineCover
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeS1
variable {R : Type} [CommRing R]
section pts
variable (G : (Over (Spec (CommRingCat.of R)))ᵒᵖ ⥤ Type) {X : Scheme.{0}}
  (e : G.overTotal.RepresentableBy X)
  (F : ∀ (A : Type) [CommRing A] [Algebra R A], Type)
  (ev : ∀ (A : Type) [CommRing A] [Algebra R A],
    F A ≃ G.obj (op (Over.mk (Spec.map (CommRingCat.ofHom (algebraMap R A))))))
variable (A : Type) [CommRing A] [Algebra R A]
Lean source · statement
lemma ofPts_toPts (s : F A) : ofPts G e F ev A (toPts G e F ev A s) = s
lemma

toPts_ofPts

L94 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_represents_of_zariskiSheaf_of_openAffineCover.GrassBridgeS1.toPts_ofPts
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_represents_of_zariskiSheaf_of_openAffineCover
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeS1
variable {R : Type} [CommRing R]
section pts
variable (G : (Over (Spec (CommRingCat.of R)))ᵒᵖ ⥤ Type) {X : Scheme.{0}}
  (e : G.overTotal.RepresentableBy X)
  (F : ∀ (A : Type) [CommRing A] [Algebra R A], Type)
  (ev : ∀ (A : Type) [CommRing A] [Algebra R A],
    F A ≃ G.obj (op (Over.mk (Spec.map (CommRingCat.ofHom (algebraMap R A))))))
variable (A : Type) [CommRing A] [Algebra R A]
Lean source · statement
lemma toPts_ofPts (g : Pts G e A) : toPts G e F ev A (ofPts G e F ev A g) = g
def

ptEquiv

L106 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_represents_of_zariskiSheaf_of_openAffineCover.GrassBridgeS1.ptEquiv
Documentation

The equivalence between elements of the functor and points of its representing scheme over the base.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_represents_of_zariskiSheaf_of_openAffineCover
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeS1
variable {R : Type} [CommRing R]
section pts
variable (G : (Over (Spec (CommRingCat.of R)))ᵒᵖ ⥤ Type) {X : Scheme.{0}}
  (e : G.overTotal.RepresentableBy X)
  (F : ∀ (A : Type) [CommRing A] [Algebra R A], Type)
  (ev : ∀ (A : Type) [CommRing A] [Algebra R A],
    F A ≃ G.obj (op (Over.mk (Spec.map (CommRingCat.ofHom (algebraMap R A))))))
variable (A : Type) [CommRing A] [Algebra R A]
Lean source · statement
def ptEquiv : F A ≃ Pts G e A
lemma

ptEquiv_natural

L111 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_represents_of_zariskiSheaf_of_openAffineCover.GrassBridgeS1.ptEquiv_natural
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_represents_of_zariskiSheaf_of_openAffineCover
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeS1
variable {R : Type} [CommRing R]
section pts
variable (G : (Over (Spec (CommRingCat.of R)))ᵒᵖ ⥤ Type) {X : Scheme.{0}}
  (e : G.overTotal.RepresentableBy X)
  (F : ∀ (A : Type) [CommRing A] [Algebra R A], Type)
  (ev : ∀ (A : Type) [CommRing A] [Algebra R A],
    F A ≃ G.obj (op (Over.mk (Spec.map (CommRingCat.ofHom (algebraMap R A))))))
variable (A : Type) [CommRing A] [Algebra R A]
variable {A}
Lean source · statement
lemma ptEquiv_natural
    (Fmap : ∀ (A B : Type) [CommRing A] [CommRing B] [Algebra R A] [Algebra R B],
      (A →ₐ[R] B) → F A → F B)
    (hev : ∀ (A B : Type) [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) (s
      : F A)
      (h : Spec.map (CommRingCat.ofHom φ.toRingHom) ≫ Spec.map (CommRingCat.ofHom (algebraMap R A))
        =
        Spec.map (CommRingCat.ofHom (algebraMap R B))),
      ev B (Fmap A B φ s) =
        G.map (Over.homMk (Spec.map (CommRingCat.ofHom φ.toRingHom)) h :
          Over.mk (Spec.map (CommRingCat.ofHom (algebraMap R B))) ⟶
            Over.mk (Spec.map (CommRingCat.ofHom (algebraMap R A)))).op (ev A s))
    (B : Type) [CommRing B] [Algebra R B] (φ : A →ₐ[R] B) (s : F A) :
    (ptEquiv G e F ev B (Fmap A B φ s)).1 =
      Spec.map (CommRingCat.ofHom φ.toRingHom) ≫ (ptEquiv G e F ev A s).1
lemma

P_map

L148 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_represents_of_zariskiSheaf_of_openAffineCover.GrassBridgeS1.P_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_represents_of_zariskiSheaf_of_openAffineCover
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeS1
variable {R : Type} [CommRing R]
Lean source · statement
lemma P_map
    (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)
    (Fmap_id : ∀ (A : Type) [CommRing A] [Algebra R A] (s : F A), Fmap A A (AlgHom.id R A) s = s)
    {ι : Type} (P : ι → ∀ (A : Type) [CommRing A] [Algebra R A], F A → Prop)
    (isOpen : ∀ (i : ι) (A : Type) [CommRing A] [Algebra R A] (s : F A),
      ∃ U : Set (PrimeSpectrum A), IsOpen U ∧
        ∀ (B : Type) [CommRing B] [Algebra R B] (φ : A →ₐ[R] B),
          P i B (Fmap A B φ s) ↔ Set.range (PrimeSpectrum.comap φ.toRingHom) ⊆ U)
    (i : ι) {A B : Type} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B)
    (u : {s : F A // P i A s}) : P i B (Fmap A B φ u.1)
theorem

exists_represents_of_zariskiSheaf_of_openAffineCover

L171 ↗
AlgebraicGeometry.Scheme.exists_represents_of_zariskiSheaf_of_openAffineCover
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_represents_of_zariskiSheaf_of_openAffineCover
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
open GrassBridgeS1 in
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.exists_represents_of_zariskiSheaf_of_openAffineCover
    (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)
    (Fmap_id : ∀ (A : Type) [CommRing A] [Algebra R A] (s : F A), Fmap A A (AlgHom.id R A) s = s)
    (Fmap_comp : ∀ (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 A C (ψ.comp φ) s = Fmap B C ψ (Fmap A B φ s))
    (sheaf : ∀ (A : Type) [CommRing A] [Algebra R A] (n : ℕ) (f : Fin n → A),
      Ideal.span (Set.range f) = ⊤ →
      ∀ (B : Fin n → Type) [∀ i, CommRing (B i)] [∀ i, Algebra A (B i)] [∀ i, Algebra R (B i)]
        [∀ i, IsScalarTower R A (B i)] [∀ i, IsLocalization.Away (f i) (B i)] (s : ∀ i, F (B i)),
      (∀ (i j : Fin n) (C : Type) [CommRing C] [Algebra A C] [Algebra R C] [IsScalarTower R A C]
          [IsLocalization.Away (f i * f j) C] (ρ₁ : B i →ₐ[A] C) (ρ₂ : B j →ₐ[A] C),
          Fmap _ _ (ρ₁.restrictScalars R) (s i) = Fmap _ _ (ρ₂.restrictScalars R) (s j)) →
      ∃! s₀ : F A, ∀ i, Fmap _ _ (IsScalarTower.toAlgHom R A (B i)) s₀ = s i)
    (ι : Type) (P : ι → ∀ (A : Type) [CommRing A] [Algebra R A], F A → Prop)
    (isOpen : ∀ (i : ι) (A : Type) [CommRing A] [Algebra R A] (s : F A),
      ∃ U : Set (PrimeSpectrum A), IsOpen U ∧
        ∀ (B : Type) [CommRing B] [Algebra R B] (φ : A →ₐ[R] B),
          P i B (Fmap A B φ s) ↔ Set.range (PrimeSpectrum.comap φ.toRingHom) ⊆ U)
    (S : ι → Type) [∀ i, CommRing (S i)] [∀ i, Algebra R (S i)]
    (chart : ∀ (i : ι) (A : Type) [CommRing A] [Algebra R A], {s : F A // P i A s} ≃ (S i →ₐ[R] A))
    (chart_natural : ∀ (i : ι) (A B : Type) [CommRing A] [CommRing B] [Algebra R A] [Algebra R B]
      (φ : A →ₐ[R] B) (s : {s : F A // P i A s}) (h : P i B (Fmap A B φ s.1)),
      chart i B ⟨Fmap A B φ s.1, h⟩ = φ.comp (chart i A s))
    (cover : ∀ (K : Type) [Field K] [Algebra R K] (s : F K), ∃ i, P i K s) :
    ∃ (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))})
      (j : ∀ i, Spec (CommRingCat.of (S i)) ⟶ X),
      (∀ (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) ∧
      (∀ i, IsOpenImmersion (j i)) ∧
      (∀ i, j i ≫ p = Spec.map (CommRingCat.ofHom (algebraMap R (S i)))) ∧
      (∀ y : X, ∃ i, y ∈ Set.range (j i).base) ∧
      (∀ (i : ι) (A : Type) [CommRing A] [Algebra R A] (s : {s : F A // P i A s}),
          (pt A s.1).1 = Spec.map (CommRingCat.ofHom (chart i A s).toRingHom) ≫ j i)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.