Module

SubalgebraStages.lean

Nyll.SchemeTheory.Descent.SubalgebraStages

49 declarations indexed from sourceView source ↗

Module documentation

Subalgebra Stages

Imports2

Mathlib.AlgebraicGeometry.Morphisms.Affine
Mathlib.Tactic.CategoryTheory.Reassoc

Imported by8

abbrev

specHom

L32 ↗

AlgebraicGeometry.SubalgebraStages.specHom

Documentation

The structure morphism from the spectrum of a stage subalgebra to the base spectrum.

Source context 6 commands

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

universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace SubalgebraStages
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)

Lean source · statement

abbrev specHom (i : ι) : Spec (CommRingCat.of ↥(S i)) ⟶ Spec (CommRingCat.of A₀)

abbrev

specHomTop

L36 ↗

AlgebraicGeometry.SubalgebraStages.specHomTop

Documentation

The structure morphism from the spectrum of the ambient algebra to the base spectrum.

Source context 6 commands

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

universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace SubalgebraStages
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)

Lean source · statement

abbrev specHomTop : Spec (CommRingCat.of A) ⟶ Spec (CommRingCat.of A₀)

abbrev

specTrans

L40 ↗

AlgebraicGeometry.SubalgebraStages.specTrans

Documentation

The morphism of spectra induced by inclusion of stage subalgebras.

Source context 6 commands

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

universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace SubalgebraStages
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)

Lean source · statement

abbrev specTrans {i j : ι} (h : i ≤ j) : Spec (CommRingCat.of ↥(S j)) ⟶ Spec
  (CommRingCat.of ↥(S i))

abbrev

specLeg

L45 ↗

AlgebraicGeometry.SubalgebraStages.specLeg

Documentation

The morphism from the ambient spectrum to a stage spectrum.

Source context 6 commands

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

universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace SubalgebraStages
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)

Lean source · statement

abbrev specLeg (i : ι) : Spec (CommRingCat.of A) ⟶ Spec (CommRingCat.of ↥(S i))

lemma

specTrans_specHom

L48 ↗

AlgebraicGeometry.SubalgebraStages.specTrans_specHom

Source context 6 commands

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

universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace SubalgebraStages
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)

Lean source · statement

lemma specTrans_specHom {i j : ι} (h : i ≤ j) : specTrans S h ≫ specHom S i = specHom S j

lemma

specLeg_specHom

L52 ↗

AlgebraicGeometry.SubalgebraStages.specLeg_specHom

Source context 6 commands

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

universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace SubalgebraStages
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)

Lean source · statement

lemma specLeg_specHom (i : ι) : specLeg S i ≫ specHom S i = specHomTop (A₀ := A₀) (A := A)

lemma

specLeg_specTrans

L56 ↗

AlgebraicGeometry.SubalgebraStages.specLeg_specTrans

Source context 6 commands

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

universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace SubalgebraStages
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)

Lean source · statement

lemma specLeg_specTrans {i j : ι} (h : i ≤ j) : specLeg S j ≫ specTrans S h = specLeg S i

lemma

specTrans_comp

L60 ↗

AlgebraicGeometry.SubalgebraStages.specTrans_comp

Source context 6 commands

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

universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace SubalgebraStages
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)

Lean source · statement

lemma specTrans_comp {i j k : ι} (h : i ≤ j) (h' : j ≤ k) :
    specTrans S h' ≫ specTrans S h = specTrans S (h.trans h')

lemma

specTrans_refl

L64 ↗

AlgebraicGeometry.SubalgebraStages.specTrans_refl

Source context 6 commands

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

universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace SubalgebraStages
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)

Lean source · statement

lemma specTrans_refl (i : ι) : specTrans S (le_refl i) = 𝟙 _

def

specDiagram

L68 ↗

AlgebraicGeometry.SubalgebraStages.specDiagram

Documentation

The inverse diagram of spectra of the stage subalgebras.

Source context 6 commands

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

universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace SubalgebraStages
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)

Lean source · full declaration

def specDiagram : ιᵒᵖ ⥤ Scheme.{u} where
  obj i := Spec (CommRingCat.of ↥(S i.unop))
  map h := specTrans S h.unop.le
  map_id i := specTrans_refl S i.unop
  map_comp h h' := (specTrans_comp S h'.unop.le h.unop.le).symm

def

specCone

L75 ↗

AlgebraicGeometry.SubalgebraStages.specCone

Documentation

The cone from the ambient spectrum over the diagram of stage spectra.

Source context 6 commands

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

universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace SubalgebraStages
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)

Lean source · full declaration

def specCone : Cone (specDiagram S) where
  pt := Spec (CommRingCat.of A)
  π := { app i := specLeg S i.unop
         naturality {i j} h := by
           simp only [Functor.const_obj_obj, Functor.const_obj_map, Category.id_comp]
           exact (specLeg_specTrans S h.unop.le).symm }

lemma

specDiagram_obj

L82 ↗

AlgebraicGeometry.SubalgebraStages.specDiagram_obj

Source context 6 commands

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

universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace SubalgebraStages
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)

Lean source · statement

lemma specDiagram_obj (i : ιᵒᵖ) : (specDiagram S).obj i = Spec (CommRingCat.of ↥(S i.unop))

lemma

specDiagram_map

L84 ↗

AlgebraicGeometry.SubalgebraStages.specDiagram_map

Source context 6 commands

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

universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace SubalgebraStages
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)

Lean source · statement

lemma specDiagram_map {i j : ιᵒᵖ} (h : i ⟶ j) : (specDiagram S).map h = specTrans S
  h.unop.le

lemma

specCone_pt

L86 ↗

AlgebraicGeometry.SubalgebraStages.specCone_pt

Source context 6 commands

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

universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace SubalgebraStages
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)

Lean source · statement

lemma specCone_pt : (specCone S).pt = Spec (CommRingCat.of A)

lemma

specCone_π_app

L87 ↗

AlgebraicGeometry.SubalgebraStages.specCone_π_app

Source context 6 commands

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

universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace SubalgebraStages
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)

Lean source · statement

lemma specCone_π_app (i : ιᵒᵖ) : (specCone S).π.app i = specLeg S i.unop

abbrev

obj

L92 ↗

AlgebraicGeometry.SubalgebraStages.obj

Documentation

The base change of the scheme to a stage subalgebra.

Source context 7 commands

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

universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace SubalgebraStages
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A₀))

Lean source · statement

abbrev obj (i : ι) : Scheme.{u}

def

trans

L95 ↗

AlgebraicGeometry.SubalgebraStages.trans

Documentation

The transition morphism between two stage base changes.

Source context 7 commands

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

universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace SubalgebraStages
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A₀))

Lean source · statement

def trans {i j : ι} (h : i ≤ j) : obj S f j ⟶ obj S f i

lemma

trans_fst

L99 ↗

AlgebraicGeometry.SubalgebraStages.trans_fst

Source context 7 commands

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

universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace SubalgebraStages
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A₀))

Lean source · statement

lemma trans_fst {i j : ι} (h : i ≤ j) :
    trans S f h ≫ pullback.fst f (specHom S i) = pullback.fst f (specHom S j)

lemma

trans_snd

L103 ↗

AlgebraicGeometry.SubalgebraStages.trans_snd

Source context 7 commands

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

universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace SubalgebraStages
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A₀))

Lean source · statement

lemma trans_snd {i j : ι} (h : i ≤ j) :
    trans S f h ≫ pullback.snd f (specHom S i) = pullback.snd f (specHom S j) ≫ specTrans S h

lemma

trans_refl

L107 ↗

AlgebraicGeometry.SubalgebraStages.trans_refl

Source context 7 commands

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

universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace SubalgebraStages
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A₀))

Lean source · statement

lemma trans_refl (i : ι) : trans S f (le_refl i) = 𝟙 _

lemma

trans_comp

L112 ↗

AlgebraicGeometry.SubalgebraStages.trans_comp

Source context 7 commands

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

universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace SubalgebraStages
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A₀))

Lean source · statement

lemma trans_comp {i j k : ι} (h : i ≤ j) (h' : j ≤ k) :
    trans S f h' ≫ trans S f h = trans S f (h.trans h')

def

diagram

L119 ↗

AlgebraicGeometry.SubalgebraStages.diagram

Documentation

The inverse diagram of scheme base changes to the stage subalgebras.

Source context 7 commands

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

universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace SubalgebraStages
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A₀))

Lean source · full declaration

def diagram : ιᵒᵖ ⥤ Scheme.{u} where
  obj i := obj S f i.unop
  map h := trans S f h.unop.le
  map_id i := trans_refl S f i.unop
  map_comp h h' := (trans_comp S f h'.unop.le h.unop.le).symm

lemma

diagram_obj

L125 ↗

AlgebraicGeometry.SubalgebraStages.diagram_obj

Source context 7 commands

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

universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace SubalgebraStages
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A₀))

Lean source · statement

lemma diagram_obj (i : ιᵒᵖ) : (diagram S f).obj i = pullback f (specHom S i.unop)

lemma

diagram_map

L126 ↗

AlgebraicGeometry.SubalgebraStages.diagram_map

Source context 7 commands

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

universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace SubalgebraStages
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A₀))

Lean source · statement

lemma diagram_map {i j : ιᵒᵖ} (h : i ⟶ j) : (diagram S f).map h = trans S f h.unop.le

lemma

diagram_map_fst

L128 ↗

AlgebraicGeometry.SubalgebraStages.diagram_map_fst

Source context 7 commands

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

universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace SubalgebraStages
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A₀))

Lean source · statement

lemma diagram_map_fst {i j : ιᵒᵖ} (h : i ⟶ j) :
    (diagram S f).map h ≫ pullback.fst f (specHom S j.unop) = pullback.fst f (specHom S i.unop)

lemma

diagram_map_snd

L132 ↗

AlgebraicGeometry.SubalgebraStages.diagram_map_snd

Source context 7 commands

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

universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace SubalgebraStages
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A₀))

Lean source · statement

lemma diagram_map_snd {i j : ιᵒᵖ} (h : i ⟶ j) :
    (diagram S f).map h ≫ pullback.snd f (specHom S j.unop) = pullback.snd f (specHom S i.unop) ≫
      specTrans S h.unop.le

def

leg

L138 ↗

AlgebraicGeometry.SubalgebraStages.leg

Documentation

The projection from the ambient base change to a stage base change.

Source context 7 commands

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

universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace SubalgebraStages
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A₀))

Lean source · statement

def leg (i : ι) : pullback f (specHomTop (A₀ := A₀) (A := A)) ⟶ obj S f i

lemma

leg_fst

L142 ↗

AlgebraicGeometry.SubalgebraStages.leg_fst

Source context 7 commands

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

universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace SubalgebraStages
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A₀))

Lean source · statement

lemma leg_fst (i : ι) :
    leg S f i ≫ pullback.fst f (specHom S i) = pullback.fst f specHomTop

lemma

leg_snd

L145 ↗

AlgebraicGeometry.SubalgebraStages.leg_snd

Source context 7 commands

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

universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace SubalgebraStages
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A₀))

Lean source · statement

lemma leg_snd (i : ι) :
    leg S f i ≫ pullback.snd f (specHom S i) = pullback.snd f specHomTop ≫ specLeg S i

lemma

leg_trans

L149 ↗

AlgebraicGeometry.SubalgebraStages.leg_trans

Source context 7 commands

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

universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace SubalgebraStages
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A₀))

Lean source · statement

lemma leg_trans {i j : ι} (h : i ≤ j) : leg S f j ≫ trans S f h = leg S f i

def

cone

L155 ↗

AlgebraicGeometry.SubalgebraStages.cone

Documentation

The cone from the ambient base change over the diagram of stage base changes.

Source context 7 commands

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

universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace SubalgebraStages
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A₀))

Lean source · full declaration

def cone : Cone (diagram S f) where
  pt := pullback f (specHomTop (A₀ := A₀) (A := A))
  π := { app i := leg S f i.unop
         naturality {i j} h := by
           simp only [Functor.const_obj_obj, Functor.const_obj_map, Category.id_comp]
           exact (leg_trans S f h.unop.le).symm }

lemma

cone_pt

L162 ↗

AlgebraicGeometry.SubalgebraStages.cone_pt

Source context 7 commands

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

universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace SubalgebraStages
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A₀))

Lean source · statement

lemma cone_pt : (cone S f).pt = pullback f (specHomTop (A₀ := A₀) (A := A))

lemma

cone_π_app

L163 ↗

AlgebraicGeometry.SubalgebraStages.cone_π_app

Source context 7 commands

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

universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace SubalgebraStages
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A₀))

Lean source · statement

lemma cone_π_app (i : ιᵒᵖ) : (cone S f).π.app i = leg S f i.unop

lemma

cone_π_app_fst

L165 ↗

AlgebraicGeometry.SubalgebraStages.cone_π_app_fst

Source context 7 commands

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

universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace SubalgebraStages
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A₀))

Lean source · statement

lemma cone_π_app_fst (i : ιᵒᵖ) :
    (cone S f).π.app i ≫ pullback.fst f (specHom S i.unop) = pullback.fst f specHomTop

lemma

cone_π_app_snd

L169 ↗

AlgebraicGeometry.SubalgebraStages.cone_π_app_snd

Source context 7 commands

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

universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace SubalgebraStages
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A₀))

Lean source · statement

lemma cone_π_app_snd (i : ιᵒᵖ) :
    (cone S f).π.app i ≫ pullback.snd f (specHom S i.unop) = pullback.snd f specHomTop ≫ specLeg S
      i.unop

lemma

specCone_π_app_specHom

L174 ↗

AlgebraicGeometry.SubalgebraStages.specCone_π_app_specHom

Source context 7 commands

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

universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace SubalgebraStages
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A₀))

Lean source · statement

lemma specCone_π_app_specHom (i : ιᵒᵖ) :
    (specCone S).π.app i ≫ specHom S i.unop = specHomTop (A₀ := A₀) (A := A)

lemma

specDiagram_map_specHom

L178 ↗

AlgebraicGeometry.SubalgebraStages.specDiagram_map_specHom

Source context 7 commands

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

universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace SubalgebraStages
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A₀))

Lean source · statement

lemma specDiagram_map_specHom {i j : ιᵒᵖ} (h : i ⟶ j) :
    (specDiagram S).map h ≫ specHom S j.unop = specHom S i.unop

lemma

isPullback_trans

L181 ↗

AlgebraicGeometry.SubalgebraStages.isPullback_trans

Source context 7 commands

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

universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace SubalgebraStages
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A₀))

Lean source · statement

lemma isPullback_trans {i j : ι} (h : i ≤ j) :
    IsPullback (trans S f h) (pullback.snd f (specHom S j)) (pullback.snd f (specHom S i))
      (specTrans S h)

lemma

isPullback_leg

L189 ↗

AlgebraicGeometry.SubalgebraStages.isPullback_leg

Source context 7 commands

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

universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace SubalgebraStages
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A₀))

Lean source · statement

lemma isPullback_leg (i : ι) :
    IsPullback (leg S f i) (pullback.snd f specHomTop) (pullback.snd f (specHom S i)) (specLeg S i)

instance

isAffineHom_trans

L197 ↗

AlgebraicGeometry.SubalgebraStages.isAffineHom_trans

Source context 7 commands

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

universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace SubalgebraStages
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A₀))

Lean source · statement

instance isAffineHom_trans {i j : ι} (h : i ≤ j) : IsAffineHom (trans S f h)

instance

isAffineHom_diagram_map

L200 ↗

AlgebraicGeometry.SubalgebraStages.isAffineHom_diagram_map

Source context 7 commands

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

universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace SubalgebraStages
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A₀))

Lean source · statement

instance isAffineHom_diagram_map {i j : ιᵒᵖ} (h : i ⟶ j) : IsAffineHom ((diagram S f).map h)

instance

isAffineHom_leg

L203 ↗

AlgebraicGeometry.SubalgebraStages.isAffineHom_leg

Source context 7 commands

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

universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace SubalgebraStages
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A₀))

Lean source · statement

instance isAffineHom_leg (i : ι) : IsAffineHom (leg S f i)

instance

quasiCompact_snd

L206 ↗

AlgebraicGeometry.SubalgebraStages.quasiCompact_snd

Source context 7 commands

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

universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace SubalgebraStages
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A₀))

Lean source · statement

instance quasiCompact_snd [QuasiCompact f] (i : ι) : QuasiCompact (pullback.snd f (specHom S i))

instance

quasiSeparated_snd

L210 ↗

AlgebraicGeometry.SubalgebraStages.quasiSeparated_snd

Source context 7 commands

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

universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace SubalgebraStages
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A₀))

Lean source · statement

instance quasiSeparated_snd [QuasiSeparated f] (i : ι) : QuasiSeparated (pullback.snd f (specHom S
  i))

instance

compactSpace_pullback

L215 ↗

AlgebraicGeometry.SubalgebraStages.compactSpace_pullback

Source context 7 commands

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

universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace SubalgebraStages
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A₀))

Lean source · statement

instance compactSpace_pullback [QuasiCompact f] (i : ι) : CompactSpace ↥(pullback f (specHom S i))

instance

compactSpace_obj

L221 ↗

AlgebraicGeometry.SubalgebraStages.compactSpace_obj

Source context 7 commands

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

universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace SubalgebraStages
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A₀))

Lean source · statement

instance compactSpace_obj [QuasiCompact f] (i : ιᵒᵖ) : CompactSpace ↥((diagram S f).obj i)

instance

quasiSeparatedSpace_pullback

L224 ↗

AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_pullback

Source context 7 commands

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

universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace SubalgebraStages
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A₀))

Lean source · statement

instance quasiSeparatedSpace_pullback [QuasiSeparated f] (i : ι) : QuasiSeparatedSpace ↥(pullback f
  (specHom S i))

instance

quasiSeparatedSpace_obj

L229 ↗

AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_obj

Source context 7 commands

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

universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace SubalgebraStages
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A₀))

Lean source · statement

instance quasiSeparatedSpace_obj [QuasiSeparated f] (i : ιᵒᵖ) : QuasiSeparatedSpace ↥((diagram S
  f).obj i)

instance

isCofiltered_op

L233 ↗

AlgebraicGeometry.SubalgebraStages.isCofiltered_op

Source context 7 commands

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

universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
namespace SubalgebraStages
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
variable {ι : Type u} [Preorder ι] (S : ι →o Subalgebra A₀ A)
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A₀))

Lean source · statement

instance isCofiltered_op [IsDirected ι (· ≤ ·)] [Nonempty ι] : IsCofiltered ιᵒᵖ

Module documentation

Subalgebra Stages

Declarations