Module

Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.lean

Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away

75 declarations indexed from sourceView source ↗

Module documentation

Scheme exists presheaf over equiv is Sheaf over Total of is Localization away

Imports18

Lean.Elab.Command
Mathlib.Algebra.Algebra.Tower
Mathlib.AlgebraicGeometry.Sites.BigZariski
Mathlib.AlgebraicGeometry.Cover.Open
Mathlib.AlgebraicGeometry.Gluing
Mathlib.CategoryTheory.Sites.Continuous
Mathlib.CategoryTheory.Sites.InducedTopology
Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
Mathlib.CategoryTheory.Sites.IsSheafFor
Mathlib.CategoryTheory.Sites.Sheaf
Mathlib.CategoryTheory.Sites.Sieves.Basic
Mathlib.CategoryTheory.Sites.Sieves.Functoriality
Mathlib.CategoryTheory.Sites.Sieves.Presieve
Mathlib.LinearAlgebra.Span.Defs
Mathlib.RingTheory.Localization.Away.Basic
Mathlib.RingTheory.Spectrum.Prime.Topology
Nyll.SchemeTheory.CategoryTheory.OverTotalPresheaf

Imported by2

structure

Datum

L54 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.Datum

Documentation

A covariant functor on commutative algebras, specified by its values, maps, and functoriality laws.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1

Lean source · full declaration

structure Datum (R : Type) [CommRing R] where
  /-- The value of the functor on each commutative algebra over the base. -/
  F : ∀ (A : Type) [CommRing A] [Algebra R A], Type
  /-- The action of an algebra homomorphism on functor elements. -/
  Fmap : ∀ (A B : Type) [CommRing A] [CommRing B] [Algebra R A] [Algebra R B],
    (A →ₐ[R] B) → F A → F B
  /-- The identity algebra homomorphism acts as the identity. -/
  Fmap_id : ∀ (A : Type) [CommRing A] [Algebra R A] (s : F A), Fmap A A (AlgHom.id R A) s = s
  /-- The functor action preserves composition of algebra homomorphisms. -/
  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)

def

IsSheaf

L72 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.Datum.IsSheaf

Documentation

The unique gluing property for compatible elements on finite basic-open localization covers.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1
namespace Datum
variable {R : Type} [CommRing R] (D : Datum R)

Lean source · statement

def IsSheaf : Prop

abbrev

F'

L83 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.Datum.F'

Documentation

The functor value with its algebra structure supplied explicitly.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1
namespace Datum
variable {R : Type} [CommRing R] (D : Datum R)

Lean source · statement

abbrev F' (A : Type) [CommRing A] (i : Algebra R A) : Type

abbrev

am

L86 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.Datum.am

Documentation

The structure homomorphism evaluated using an explicitly supplied algebra structure.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1
namespace Datum
variable {R : Type} [CommRing R] (D : Datum R)

Lean source · statement

abbrev am {A : Type} [CommRing A] (i : Algebra R A) (r : R) : A

def

mkₐ

L92 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.Datum.mkₐ

Documentation

An algebra homomorphism built from a ring homomorphism compatible with two explicit algebra structures.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1
namespace Datum
variable {R : Type} [CommRing R] (D : Datum R)

Lean source · statement

def mkₐ {A B : Type} [CommRing A] [CommRing B] (iA : Algebra R A) (iB : Algebra R B) (g : A →+* B)
    (hg : ∀ r, g (am iA r) = am iB r) : @AlgHom R A B _ _ _ iA iB

lemma

mkₐ_apply

L96 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.Datum.mkₐ_apply

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1
namespace Datum
variable {R : Type} [CommRing R] (D : Datum R)

Lean source · statement

lemma mkₐ_apply {A B : Type} [CommRing A] [CommRing B] (iA : Algebra R A) (iB :
  Algebra R B)
    (g : A →+* B) (hg : ∀ r, g (am iA r) = am iB r) (a : A) : mkₐ iA iB g hg a = g a

def

T

L103 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.Datum.T

Documentation

The functor map associated with a ring homomorphism compatible with explicit algebra structures.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1
namespace Datum
variable {R : Type} [CommRing R] (D : Datum R)

Lean source · statement

def T {A B : Type} [CommRing A] [CommRing B] (iA : Algebra R A) (iB : Algebra R B) (g : A →+* B)
    (hg : ∀ r, g (am iA r) = am iB r) : D.F' A iA → D.F' B iB

lemma

Fmap_eq_T

L107 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.Datum.Fmap_eq_T

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1
namespace Datum
variable {R : Type} [CommRing R] (D : Datum R)

Lean source · statement

lemma Fmap_eq_T {A B : Type} [CommRing A] [CommRing B] {iA : Algebra R A} {iB : Algebra R B}
    (f : @AlgHom R A B _ _ _ iA iB) (x : D.F' A iA) :
    @Datum.Fmap R _ D A B _ _ iA iB f x = D.T iA iB f.toRingHom (@AlgHom.commutes R A B _ _ _ iA iB
      f) x

lemma

T_id

L113 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.Datum.T_id

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1
namespace Datum
variable {R : Type} [CommRing R] (D : Datum R)

Lean source · statement

lemma T_id {A : Type} [CommRing A] (iA : Algebra R A) (hg : ∀ r, RingHom.id A (am iA r) = am iA r)
    (x : D.F' A iA) : D.T iA iA (RingHom.id A) hg x = x

lemma

T_T

L117 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.Datum.T_T

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1
namespace Datum
variable {R : Type} [CommRing R] (D : Datum R)

Lean source · full declaration

lemma T_T {A B C : Type} [CommRing A] [CommRing B] [CommRing C] (iA : Algebra R A) (iB : Algebra R
  B)
    (iC : Algebra R C) (g : A →+* B) (hg : ∀ r, g (am iA r) = am iB r) (g' : B →+* C)
    (hg' : ∀ r, g' (am iB r) = am iC r) (x : D.F' A iA) :
    D.T iB iC g' hg' (D.T iA iB g hg x) =
      D.T iA iC (g'.comp g) (fun r => by rw [RingHom.comp_apply, hg, hg']) x :=
  (@Datum.Fmap_comp R _ D A B C _ _ _ iA iB iC (mkₐ iA iB g hg) (mkₐ iB iC g' hg') x).symm

lemma

T_congr

L125 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.Datum.T_congr

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1
namespace Datum
variable {R : Type} [CommRing R] (D : Datum R)

Lean source · statement

lemma T_congr {A B : Type} [CommRing A] [CommRing B] (iA : Algebra R A) (iB : Algebra R B)
    {g g' : A →+* B} (h : g = g') (hg : ∀ r, g (am iA r) = am iB r)
    (hg' : ∀ r, g' (am iA r) = am iB r) (x : D.F' A iA) : D.T iA iB g hg x = D.T iA iB g' hg' x

lemma

T_comp_eq

L131 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.Datum.T_comp_eq

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1
namespace Datum
variable {R : Type} [CommRing R] (D : Datum R)

Lean source · full declaration

lemma T_comp_eq {A B C : Type} [CommRing A] [CommRing B] [CommRing C] {iA : Algebra R A}
    {iB : Algebra R B} {iC : Algebra R C} {g : A →+* B} {hg : ∀ r, g (am iA r) = am iB r} {g' : B
      →+* C}
    {hg' : ∀ r, g' (am iB r) = am iC r} {g'' : A →+* C} (h : g'.comp g = g'') (x : D.F' A iA) :
    D.T iB iC g' hg' (D.T iA iB g hg x) =
      D.T iA iC g'' (fun r => by subst h; rw [RingHom.comp_apply, hg, hg']) x := by
  rw [T_T]; exact D.T_congr _ _ h _ _ x

lemma

T_eq_self

L139 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.Datum.T_eq_self

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1
namespace Datum
variable {R : Type} [CommRing R] (D : Datum R)

Lean source · statement

lemma T_eq_self {A : Type} [CommRing A] {iA : Algebra R A} {g : A →+* A} (h : g = RingHom.id A)
    (hg : ∀ r, g (am iA r) = am iA r) (x : D.F' A iA) : D.T iA iA g hg x = x

structure

Tot

L144 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.Datum.Tot

Documentation

An element of the functor together with its base-ring structure morphism.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1
namespace Datum
variable {R : Type} [CommRing R] (D : Datum R)

Lean source · full declaration

structure Tot (A : CommRingCat.{0}) : Type where
  /-- The structure morphism from the base ring. -/
  φ : CommRingCat.of R ⟶ A
  /-- The functor element for the algebra structure induced by the structure morphism. -/
  val : D.F' A φ.hom.toAlgebra

def

out

L155 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.Datum.Tot.out

Documentation

Transport an element of the total functor to an equal explicitly supplied algebra structure.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1
namespace Datum
variable {R : Type} [CommRing R] (D : Datum R)
namespace Tot
variable {D}

Lean source · statement

def out {A : CommRingCat.{0}} (t : D.Tot A) (i : Algebra R A) (h : ∀ r, t.φ.hom r = am i r) : D.F'
  A i

lemma

out_self

L159 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.Datum.Tot.out_self

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1
namespace Datum
variable {R : Type} [CommRing R] (D : Datum R)
namespace Tot
variable {D}

Lean source · statement

lemma out_self {A : CommRingCat.{0}} (t : D.Tot A) (h : ∀ r, t.φ.hom r = am t.φ.hom.toAlgebra r) :
    t.out _ h = t.val

lemma

out_congr

L163 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.Datum.Tot.out_congr

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1
namespace Datum
variable {R : Type} [CommRing R] (D : Datum R)
namespace Tot
variable {D}

Lean source · statement

lemma out_congr {A : CommRingCat.{0}} {t t' : D.Tot A} (e : t = t') (i : Algebra R A)
    (h : ∀ r, t.φ.hom r = am i r) (h' : ∀ r, t'.φ.hom r = am i r) : t.out i h = t'.out i h'

lemma

ext_of_out

L167 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.Datum.Tot.ext_of_out

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1
namespace Datum
variable {R : Type} [CommRing R] (D : Datum R)
namespace Tot
variable {D}

Lean source · full declaration

lemma ext_of_out {A : CommRingCat.{0}} {t t' : D.Tot A} (h : t.φ = t'.φ)
    (hv : t.out t'.φ.hom.toAlgebra (fun r => by rw [h]; rfl) = t'.val) : t = t' := by
  obtain ⟨φ, v⟩ := t
  obtain ⟨φ', v'⟩ := t'
  cases h
  rw [out_self] at hv
  cases hv
  rfl

def

P₀

L182 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.Datum.P₀

Documentation

The functor on commutative rings formed by adjoining an explicit base-ring structure to each element.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1
namespace Datum
variable {R : Type} [CommRing R] (D : Datum R)

Lean source · full declaration

def P₀ : (CommRingCat.{0}ᵒᵖ)ᵒᵖ ⥤ Type where
  obj X := D.Tot X.unop.unop
  map {X Y} g := ↾fun t => ⟨t.φ ≫ g.unop.unop, D.T _ _ g.unop.unop.hom (fun _ => rfl) t.val⟩
  map_id X := by
    refine ConcreteCategory.hom_ext _ _ fun t => ?_
    simp only [TypeCat.ofHom_apply, types_id_apply]
    refine Tot.ext_of_out (Category.comp_id _) ?_
    simp only [Tot.out]
    exact (D.T_comp_eq rfl _).trans (D.T_eq_self (by ext; simp) _ _)
  map_comp {X Y Z} g g' := by
    refine ConcreteCategory.hom_ext _ _ fun t => ?_
    simp only [TypeCat.ofHom_apply, types_comp_apply]
    symm
    refine Tot.ext_of_out (Category.assoc _ _ _) ?_
    simp only [Tot.out]
    rw [D.T_comp_eq rfl, D.T_comp_eq rfl]
    rfl

lemma

P₀_map_φ

L200 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.Datum.P₀_map_φ

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1
namespace Datum
variable {R : Type} [CommRing R] (D : Datum R)

Lean source · statement

lemma P₀_map_φ {X Y : (CommRingCat.{0}ᵒᵖ)ᵒᵖ} (g : X ⟶ Y) (t : D.P₀.obj X) :
    (D.P₀.map g t).φ = t.φ ≫ g.unop.unop

lemma

P₀_map_val

L203 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.Datum.P₀_map_val

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1
namespace Datum
variable {R : Type} [CommRing R] (D : Datum R)

Lean source · full declaration

lemma P₀_map_val {X Y : (CommRingCat.{0}ᵒᵖ)ᵒᵖ} (g : X ⟶ Y) (t : D.P₀.obj X) :
    (D.P₀.map g t).val = D.T _ _ g.unop.unop.hom (fun _ => rfl) t.val := rfl

lemma

out_P₀_map

L206 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.Datum.out_P₀_map

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1
namespace Datum
variable {R : Type} [CommRing R] (D : Datum R)

Lean source · statement

lemma out_P₀_map {X Y : (CommRingCat.{0}ᵒᵖ)ᵒᵖ} (g : X ⟶ Y) (t : D.P₀.obj X)
    (i : Algebra R Y.unop.unop) (h : ∀ r, (t.φ ≫ g.unop.unop).hom r = am i r) :
    (D.P₀.map g t).out i h = D.T _ i g.unop.unop.hom h t.val

instance

isCoverDense_Spec

L232 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.isCoverDense_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_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1

Lean source · full declaration

instance isCoverDense_Spec : Scheme.Spec.IsCoverDense Scheme.zariskiTopology.{0} where
  is_cover X := by
    rw [Scheme.mem_grothendieckTopology_iff]
    refine ⟨X.affineCover, ?_⟩
    rintro Y f ⟨i⟩
    exact ⟨{obj := op _, lift := 𝟙 _, map := X.affineCover.f i, fac := Category.id_comp _}⟩

abbrev

J₀

L240 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.J₀

Documentation

The topology on affine schemes induced from the Zariski topology via the spectrum functor.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1

Lean source · statement

abbrev J₀ : GrothendieckTopology CommRingCat.{0}ᵒᵖ

instance

isOneHypercoverDense_Spec

L243 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.isOneHypercoverDense_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_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1

Lean source · statement

instance isOneHypercoverDense_Spec :
    Functor.IsOneHypercoverDense.{0} Scheme.Spec J₀ Scheme.zariskiTopology.{0}

lemma

isSheaf_J₀_yoneda

L249 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.isSheaf_J₀_yoneda

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1

Lean source · statement

lemma isSheaf_J₀_yoneda (S : Scheme.{0}) :
    Presheaf.IsSheaf J₀ (Scheme.Spec.op ⋙ yoneda.obj S)

def

stdObj

L254 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.stdObj

Documentation

The opposite ring object given by localization at one member of a finite basic-open cover.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1

Lean source · statement

def stdObj (A : CommRingCat.{0}) {n : ℕ} (f : Fin n → A) (i : Fin n) :
  CommRingCat.{0}ᵒᵖ

def

stdHom

L259 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.stdHom

Documentation

The localization map, viewed as a morphism in the opposite category of rings.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1

Lean source · statement

def stdHom (A : CommRingCat.{0}) {n : ℕ} (f : Fin n → A) (i : Fin n) : stdObj A f i ⟶
  op A

lemma

range_Spec_map_algebraMap_away

L263 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.range_Spec_map_algebraMap_away

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1

Lean source · statement

lemma range_Spec_map_algebraMap_away (A : CommRingCat.{0}) (r : A) :
    Set.range (Spec.map (CommRingCat.ofHom (algebraMap A (Localization.Away r)))) =
      (PrimeSpectrum.basicOpen r : Set (PrimeSpectrum A))

lemma

generate_std_mem

L268 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.generate_std_mem

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1

Lean source · statement

lemma generate_std_mem (A : CommRingCat.{0}) {n : ℕ} (f : Fin n → A)
    (hf : Ideal.span (Set.range f) = ⊤) :
    Sieve.ofArrows (stdObj A f) (stdHom A f) ∈ J₀ (op A)

lemma

mem_of_functorPushforward_Spec_map

L276 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.mem_of_functorPushforward_Spec_map

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1

Lean source · statement

lemma mem_of_functorPushforward_Spec_map {A : CommRingCat.{0}} (S : Sieve (op A)) {B :
  CommRingCat.{0}}
    (g : A ⟶ B) (h : S.functorPushforward Scheme.Spec (Spec.map g)) : S g.op

lemma

exists_std_of_mem

L283 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.exists_std_of_mem

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1

Lean source · statement

lemma exists_std_of_mem {A : CommRingCat.{0}} {S : Sieve (op A)} (hS : S ∈ J₀ (op A)) :
    ∃ (n : ℕ) (f : Fin n → A), Ideal.span (Set.range f) = ⊤ ∧ ∀ i, S (stdHom A f i)

lemma

isSeparatedFor_of_le

L316 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.isSeparatedFor_of_le

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1

Lean source · statement

lemma isSeparatedFor_of_le {C : Type*} [Category C] {P : Cᵒᵖ ⥤ Type*} {X : C} {R₁ R₂ : Presieve X}
    (h : R₁ ≤ R₂) (h₁ : Presieve.IsSeparatedFor P R₁) : Presieve.IsSeparatedFor P R₂

theorem

isSheafFor_std

L325 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.Datum.isSheafFor_std

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1
namespace Datum
variable {R : Type} [CommRing R] (D : Datum R)

Lean source · statement

theorem isSheafFor_std (hD : D.IsSheaf) (A : CommRingCat.{0}) {n : ℕ} (f : Fin n → A)
    (hf : Ideal.span (Set.range f) = ⊤) :
    Presieve.IsSheafFor D.P₀ (Presieve.ofArrows (stdObj A f) (stdHom A f))

theorem

isSheaf_P₀

L413 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.Datum.isSheaf_P₀

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1
namespace Datum
variable {R : Type} [CommRing R] (D : Datum R)

Lean source · statement

theorem isSheaf_P₀ (hD : D.IsSheaf) : Presheaf.IsSheaf J₀ D.P₀

abbrev

affRing

L463 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.affRing

Documentation

The coordinate ring chosen for one member of the canonical affine cover.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1

Lean source · statement

abbrev affRing (T : Scheme.{0}) (i : T.affineCover.I₀) : CommRingCat.{0}

abbrev

acov

L467 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.acov

Documentation

The canonical open cover written explicitly as spectra of its affine coordinate rings.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1

Lean source · full declaration

abbrev acov (T : Scheme.{0}) : T.OpenCover where
  I₀ := T.affineCover.I₀
  X i := Spec (affRing T i)
  f i := T.affineCover.f i
  mem₀ := T.affineCover.mem₀

def

G₀

L478 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.Datum.G₀

Documentation

The sheaf on affine schemes associated with the localization-gluing datum.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1
namespace Datum
variable {R : Type} [CommRing R] (D : Datum R) (hD : D.IsSheaf)

Lean source · statement

def G₀ : Sheaf J₀ (Type 0)

def

H

L484 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.Datum.H

Documentation

The presheaf on schemes extending the sheaf on affine schemes through the dense spectrum functor.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1
namespace Datum
variable {R : Type} [CommRing R] (D : Datum R) (hD : D.IsSheaf)

Lean source · statement

def H : Scheme.{0}ᵒᵖ ⥤ Type

lemma

H_isSheaf

L488 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.Datum.H_isSheaf

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1
namespace Datum
variable {R : Type} [CommRing R] (D : Datum R) (hD : D.IsSheaf)

Lean source · statement

lemma H_isSheaf : Presheaf.IsSheaf Scheme.zariskiTopology (D.H hD)

def

Hiso

L495 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.Datum.Hiso

Documentation

The natural isomorphism identifying the extended presheaf on affine spectra with the original functor.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1
namespace Datum
variable {R : Type} [CommRing R] (D : Datum R) (hD : D.IsSheaf)

Lean source · statement

def Hiso : Scheme.Spec.op ⋙ D.H hD ≅ D.P₀

def

toH

L499 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.Datum.toH

Documentation

The extended presheaf section associated with an affine functor element.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1
namespace Datum
variable {R : Type} [CommRing R] (D : Datum R) (hD : D.IsSheaf)

Lean source · statement

def toH {A : CommRingCat.{0}} (t : D.Tot A) : (D.H hD).obj (op (Spec A))

def

ofH

L503 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.Datum.ofH

Documentation

The affine functor element corresponding to a section of the extended presheaf.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1
namespace Datum
variable {R : Type} [CommRing R] (D : Datum R) (hD : D.IsSheaf)

Lean source · statement

def ofH {A : CommRingCat.{0}} (y : (D.H hD).obj (op (Spec A))) : D.Tot A

lemma

ofH_toH

L506 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.Datum.ofH_toH

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1
namespace Datum
variable {R : Type} [CommRing R] (D : Datum R) (hD : D.IsSheaf)

Lean source · statement

lemma ofH_toH {A : CommRingCat.{0}} (t : D.Tot A) : D.ofH hD (D.toH hD t) = t

lemma

toH_ofH

L510 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.Datum.toH_ofH

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1
namespace Datum
variable {R : Type} [CommRing R] (D : Datum R) (hD : D.IsSheaf)

Lean source · statement

lemma toH_ofH {A : CommRingCat.{0}} (y : (D.H hD).obj (op (Spec A))) : D.toH hD (D.ofH hD y) = y

lemma

ofH_map

L515 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.Datum.ofH_map

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1
namespace Datum
variable {R : Type} [CommRing R] (D : Datum R) (hD : D.IsSheaf)

Lean source · statement

lemma ofH_map {A B : CommRingCat.{0}} (g : A ⟶ B) (y : (D.H hD).obj (op (Spec A))) :
    D.ofH hD ((D.H hD).map (Spec.map g).op y) = D.P₀.map g.op.op (D.ofH hD y)

lemma

map_toH

L519 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.Datum.map_toH

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1
namespace Datum
variable {R : Type} [CommRing R] (D : Datum R) (hD : D.IsSheaf)

Lean source · statement

lemma map_toH {A B : CommRingCat.{0}} (g : A ⟶ B) (t : D.Tot A) :
    (D.H hD).map (Spec.map g).op (D.toH hD t) = D.toH hD (D.P₀.map g.op.op t)

def

aff

L527 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.Datum.aff

Documentation

The affine functor element obtained by restricting a section along a map from an affine spectrum.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1
namespace Datum
variable {R : Type} [CommRing R] (D : Datum R) (hD : D.IsSheaf)

Lean source · statement

def aff {T : Scheme.{0}} (y : (D.H hD).obj (op T)) {A : CommRingCat.{0}} (u : Spec A
  ⟶ T) :
    D.Tot A

lemma

aff_map

L532 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.Datum.aff_map

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1
namespace Datum
variable {R : Type} [CommRing R] (D : Datum R) (hD : D.IsSheaf)

Lean source · statement

lemma aff_map {T T' : Scheme.{0}} (y : (D.H hD).obj (op T)) (k : T' ⟶ T) {A : CommRingCat.{0}}
    (u : Spec A ⟶ T') : D.aff hD ((D.H hD).map k.op y) u = D.aff hD y (u ≫ k)

lemma

aff_id

L536 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.Datum.aff_id

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1
namespace Datum
variable {R : Type} [CommRing R] (D : Datum R) (hD : D.IsSheaf)

Lean source · statement

lemma aff_id {A : CommRingCat.{0}} (y : (D.H hD).obj (op (Spec A))) :
    D.aff hD y (𝟙 _) = D.ofH hD y

lemma

aff_Spec_map

L540 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.Datum.aff_Spec_map

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1
namespace Datum
variable {R : Type} [CommRing R] (D : Datum R) (hD : D.IsSheaf)

Lean source · statement

lemma aff_Spec_map {T : Scheme.{0}} (y : (D.H hD).obj (op T)) {A B : CommRingCat.{0}} (g : A ⟶ B)
    (u : Spec A ⟶ T) : D.aff hD y (Spec.map g ≫ u) = D.P₀.map g.op.op (D.aff hD y u)

lemma

Spec_map_aff_φ_comp

L545 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.Datum.Spec_map_aff_φ_comp

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1
namespace Datum
variable {R : Type} [CommRing R] (D : Datum R) (hD : D.IsSheaf)

Lean source · statement

lemma Spec_map_aff_φ_comp {T : Scheme.{0}} (y : (D.H hD).obj (op T)) {A B : CommRingCat.{0}}
    (v : Spec B ⟶ Spec A) (u : Spec A ⟶ T) :
    Spec.map (D.aff hD y (v ≫ u)).φ = v ≫ Spec.map (D.aff hD y u).φ

def

base

L557 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.Datum.base

Documentation

The base morphism of a presheaf section, obtained by gluing the structure maps of its affine restrictions.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1
namespace Datum
variable {R : Type} [CommRing R] (D : Datum R) (hD : D.IsSheaf)

Lean source · statement

def base {T : Scheme.{0}} (y : (D.H hD).obj (op T)) : T ⟶ Spec (.of R)

lemma

ι_base

L565 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.Datum.ι_base

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1
namespace Datum
variable {R : Type} [CommRing R] (D : Datum R) (hD : D.IsSheaf)

Lean source · statement

lemma ι_base {T : Scheme.{0}} (y : (D.H hD).obj (op T)) (i : (acov T).I₀) :
    (acov T).f i ≫ D.base hD y = Spec.map (D.aff hD y ((acov T).f i)).φ

lemma

base_spec

L569 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.Datum.base_spec

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1
namespace Datum
variable {R : Type} [CommRing R] (D : Datum R) (hD : D.IsSheaf)

Lean source · statement

lemma base_spec {T : Scheme.{0}} (y : (D.H hD).obj (op T)) {A : CommRingCat.{0}} (u : Spec A ⟶ T) :
    Spec.map (D.aff hD y u).φ = u ≫ D.base hD y

lemma

base_unique

L581 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.Datum.base_unique

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1
namespace Datum
variable {R : Type} [CommRing R] (D : Datum R) (hD : D.IsSheaf)

Lean source · statement

lemma base_unique {T : Scheme.{0}} (y : (D.H hD).obj (op T)) (t : T ⟶ Spec (.of R))
    (ht : ∀ (A : CommRingCat.{0}) (u : Spec A ⟶ T), Spec.map (D.aff hD y u).φ = u ≫ t) :
    t = D.base hD y

def

G

L592 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.Datum.G

Documentation

The presheaf on schemes over the base consisting of sections compatible with the specified structure map.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1
namespace Datum
variable {R : Type} [CommRing R] (D : Datum R) (hD : D.IsSheaf)

Lean source · full declaration

def G : (Over (Spec (CommRingCat.of R)))ᵒᵖ ⥤ Type where
  obj X := { y : (D.H hD).obj (op X.unop.left) //
    ∀ (A : CommRingCat.{0}) (u : Spec A ⟶ X.unop.left), Spec.map (D.aff hD y u).φ = u ≫ X.unop.hom }
  map {X Y} k := ↾fun y => ⟨(D.H hD).map k.unop.left.op y.1, fun A u => by
    rw [aff_map, y.2, Category.assoc, Over.w k.unop]⟩
  map_id X := by
    refine ConcreteCategory.hom_ext _ _ fun y => Subtype.ext ?_
    simp
  map_comp {X Y Z} k k' := by
    refine ConcreteCategory.hom_ext _ _ fun y => Subtype.ext ?_
    simp

def

totEquiv

L608 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.Datum.totEquiv

Documentation

The equivalence identifying the total presheaf of sections over the base with the extended presheaf.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1
namespace Datum
variable {R : Type} [CommRing R] (D : Datum R) (hD : D.IsSheaf)

Lean source · full declaration

def totEquiv (T : Scheme.{0}) : (D.G hD).OverTotal T ≃ (D.H hD).obj (op T) where
  toFun a := a.2.1
  invFun y := ⟨D.base hD y, ⟨y, fun A u => D.base_spec hD y u⟩⟩
  left_inv a := by
    obtain ⟨t, y, hy⟩ := a
    refine Functor.OverTotal.ext' (D.base_unique hD y t hy).symm (Subtype.ext ?_)
    change (D.H hD).map (𝟙 T).op y = y
    simp
  right_inv y := rfl

def

totIso

L619 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.Datum.totIso

Documentation

The natural isomorphism between the total presheaf over the base and the extended presheaf.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1
namespace Datum
variable {R : Type} [CommRing R] (D : Datum R) (hD : D.IsSheaf)

Lean source · statement

def totIso : (D.G hD).overTotal ≅ D.H hD

theorem

isSheaf_overTotal

L625 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.Datum.isSheaf_overTotal

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1
namespace Datum
variable {R : Type} [CommRing R] (D : Datum R) (hD : D.IsSheaf)

Lean source · statement

theorem isSheaf_overTotal : Presheaf.IsSheaf Scheme.zariskiTopology (D.G hD).overTotal

lemma

Spec_map_aff_φ

L628 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.Datum.Spec_map_aff_φ

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1
namespace Datum
variable {R : Type} [CommRing R] (D : Datum R) (hD : D.IsSheaf)

Lean source · statement

lemma Spec_map_aff_φ {A B : CommRingCat.{0}} (y : (D.H hD).obj (op (Spec A))) (u : Spec B ⟶ Spec A)
  :
    Spec.map (D.aff hD y u).φ = u ≫ Spec.map (D.aff hD y (𝟙 _)).φ

lemma

aff_toH_id

L633 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.Datum.aff_toH_id

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1
namespace Datum
variable {R : Type} [CommRing R] (D : Datum R) (hD : D.IsSheaf)

Lean source · statement

lemma aff_toH_id {A : CommRingCat.{0}} (t : D.Tot A) : D.aff hD (D.toH hD t) (𝟙 (Spec A)) = t

abbrev

ovr

L641 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.Datum.ovr

Documentation

The affine spectrum with its specified structure morphism to the base spectrum.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1
namespace Datum
variable {R : Type} [CommRing R] (D : Datum R) (hD : D.IsSheaf)
section ev
variable (A : Type) [CommRing A] [instA : Algebra R A]

Lean source · statement

abbrev ovr : Over (Spec (CommRingCat.of R))

def

tot

L645 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.Datum.tot

Documentation

The total functor element carrying the given algebra structure and original functor element.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1
namespace Datum
variable {R : Type} [CommRing R] (D : Datum R) (hD : D.IsSheaf)
section ev
variable (A : Type) [CommRing A] [instA : Algebra R A]

Lean source · statement

def tot (s : D.F A) : D.Tot (CommRingCat.of A)

def

evFun

L649 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.Datum.evFun

Documentation

The section over the base associated with an element of the original algebra-valued 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_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1
namespace Datum
variable {R : Type} [CommRing R] (D : Datum R) (hD : D.IsSheaf)
section ev
variable (A : Type) [CommRing A] [instA : Algebra R A]

Lean source · statement

def evFun (s : D.F A) : (D.G hD).obj (op (ovr A))

def

germ

L658 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.Datum.germ

Documentation

The affine total-functor element extracted from a section over its own spectrum.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1
namespace Datum
variable {R : Type} [CommRing R] (D : Datum R) (hD : D.IsSheaf)
section ev
variable (A : Type) [CommRing A] [instA : Algebra R A]

Lean source · statement

def germ (z : (D.G hD).obj (op (ovr A))) : D.Tot (CommRingCat.of A)

lemma

germ_φ

L661 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.Datum.germ_φ

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1
namespace Datum
variable {R : Type} [CommRing R] (D : Datum R) (hD : D.IsSheaf)
section ev
variable (A : Type) [CommRing A] [instA : Algebra R A]

Lean source · statement

lemma germ_φ (z : (D.G hD).obj (op (ovr A))) : (D.germ hD A z).φ = CommRingCat.ofHom (algebraMap R
  A)

lemma

germ_φ_apply

L666 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.Datum.germ_φ_apply

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1
namespace Datum
variable {R : Type} [CommRing R] (D : Datum R) (hD : D.IsSheaf)
section ev
variable (A : Type) [CommRing A] [instA : Algebra R A]

Lean source · statement

lemma germ_φ_apply (z : (D.G hD).obj (op (ovr A))) (r : R) :
    (D.germ hD A z).φ.hom r = algebraMap R A r

def

evInv

L671 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.Datum.evInv

Documentation

The original functor element recovered from a section over the base spectrum.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1
namespace Datum
variable {R : Type} [CommRing R] (D : Datum R) (hD : D.IsSheaf)
section ev
variable (A : Type) [CommRing A] [instA : Algebra R A]

Lean source · statement

def evInv (z : (D.G hD).obj (op (ovr A))) : D.F A

lemma

germ_evFun

L674 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.Datum.germ_evFun

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1
namespace Datum
variable {R : Type} [CommRing R] (D : Datum R) (hD : D.IsSheaf)
section ev
variable (A : Type) [CommRing A] [instA : Algebra R A]

Lean source · statement

lemma germ_evFun (s : D.F A) : D.germ hD A (D.evFun hD A s) = D.tot A s

lemma

tot_evInv

L677 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.Datum.tot_evInv

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1
namespace Datum
variable {R : Type} [CommRing R] (D : Datum R) (hD : D.IsSheaf)
section ev
variable (A : Type) [CommRing A] [instA : Algebra R A]

Lean source · statement

lemma tot_evInv (z : (D.G hD).obj (op (ovr A))) : D.tot A (D.evInv hD A z) = D.germ hD A z

def

ev

L687 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.Datum.ev

Documentation

The equivalence identifying the original functor with sections of the constructed presheaf 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_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1
namespace Datum
variable {R : Type} [CommRing R] (D : Datum R) (hD : D.IsSheaf)
section ev
variable (A : Type) [CommRing A] [instA : Algebra R A]

Lean source · full declaration

def ev : D.F A ≃ (D.G hD).obj (op (ovr A)) where
  toFun := D.evFun hD A
  invFun := D.evInv hD A
  left_inv s := by
    unfold evInv
    rw [Tot.out_congr (D.germ_evFun hD A s) instA _ (fun _ => rfl)]
    exact (D.T_comp_eq (RingHom.comp_id (RingHom.id A)) s).trans (D.T_eq_self rfl _ _)
  right_inv z := by
    apply Subtype.ext
    change D.toH hD (D.tot A (D.evInv hD A z)) = (z.1 : (D.H hD).obj (op (Spec (.of A))))
    rw [tot_evInv]
    exact (congrArg (D.toH hD) (D.aff_id hD _)).trans (D.toH_ofH hD _)

lemma

ev_apply_val

L700 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.Datum.ev_apply_val

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1
namespace Datum
variable {R : Type} [CommRing R] (D : Datum R) (hD : D.IsSheaf)
section ev
variable (A : Type) [CommRing A] [instA : Algebra R A]

Lean source · statement

lemma ev_apply_val (s : D.F A) :
    ((D.ev hD A s).1 : (D.H hD).obj (op (Spec (.of A)))) = D.toH hD (D.tot A s)

theorem

ev_natural

L723 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away.GrassBridgeH1.Datum.ev_natural

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.CategoryTheory.Limits
namespace GrassBridgeH1
namespace Datum
variable {R : Type} [CommRing R] (D : Datum R) (hD : D.IsSheaf)

Lean source · statement

theorem ev_natural (A B : Type) [CommRing A] [CommRing B] [instA : Algebra R A] [instB : Algebra R
  B]
    (φ : A →ₐ[R] B) (s : D.F A)
    (h : Spec.map (CommRingCat.ofHom φ.toRingHom) ≫ Spec.map (CommRingCat.ofHom (algebraMap R A)) =
      Spec.map (CommRingCat.ofHom (algebraMap R B))) :
    D.ev hD B (D.Fmap A B φ s) =
      (D.G hD).map (Over.homMk (Spec.map (CommRingCat.ofHom φ.toRingHom)) h :
        ovr B ⟶ ovr A).op (D.ev hD A s)

theorem

exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away

L803 ↗

AlgebraicGeometry.Scheme.exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicGeometry.Scheme
open _root_.AlgebraicCurves.Geometry.Schemes.Proofs in
open Scheme_exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away in
open _root_.CategoryTheory in
open _root_.AlgebraicGeometry in
open _root_.Opposite in
open _root_.CategoryTheory.Limits in
open GrassBridgeH1 in

Lean source · statement

theorem exists_presheaf_over_equiv_isSheaf_overTotal_of_isLocalization_away
    (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) :
    ∃ (G : (Over (Spec (CommRingCat.of R)))ᵒᵖ ⥤ Type)
      (ev : ∀ (A : Type) [CommRing A] [Algebra R A],
        F A ≃ G.obj (op (Over.mk (Spec.map (CommRingCat.ofHom (algebraMap R A)))))),
      Presheaf.IsSheaf Scheme.zariskiTopology G.overTotal ∧
      ∀ (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)

Module documentation

Scheme exists presheaf over equiv is Sheaf over Total of is Localization away

Declarations