Finitely generated subalgebras, their inclusion diagram and its affine inverse-limit construction.
Finitely generated subalgebras of the given algebra.
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A]abbrev FGSubalgebra : Type uSurrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
namespace FGSubalgebrainstance : Nonempty (FGSubalgebra R A)Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
namespace FGSubalgebrainstance : IsDirected (FGSubalgebra R A) (· ≤ ·)Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
namespace FGSubalgebrainstance : IsFiltered (FGSubalgebra R A)Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
namespace FGSubalgebrainstance (A₀ : Subalgebra R A) : IsDirected {A₁ : FGSubalgebra R A // A₀ ≤ A₁.1} (· ≤ ·)Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
namespace FGSubalgebrainstance (A₀ : FGSubalgebra R A) : Nonempty {A₁ : FGSubalgebra R A // A₀.1 ≤ A₁.1}Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
namespace FGSubalgebralemma nonempty_subtype_le (A₀ : Subalgebra R A) (h : A₀.FG) :
Nonempty {A₁ : FGSubalgebra R A // A₀ ≤ A₁.1}Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
namespace FGSubalgebrainstance : IsCofiltered (FGSubalgebra R A)ᵒᵖThe diagram of finitely generated subalgebras and their inclusions.
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
namespace FGSubalgebradef diagram : FGSubalgebra R A ⥤ CommRingCat.{u} where
obj A₀ := CommRingCat.of A₀.1
map {A₀ A₁} h := CommRingCat.ofHom (Subalgebra.inclusion (R := R) (show A₀.1 ≤ A₁.1 from
h.le)).toRingHom
map_id _ := by ext; rfl
map_comp _ _ := by ext; rflThe inclusion cocone from finitely generated subalgebras to the ambient algebra.
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
namespace FGSubalgebradef cocone : Cocone (diagram R A) where
pt := CommRingCat.of A
ι := { app A₀ := CommRingCat.ofHom A₀.1.val.toRingHom
naturality _ _ _ := by ext; rfl }Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
namespace FGSubalgebralemma diagram_obj (A₀ : FGSubalgebra R A) : (diagram R A).obj A₀ = CommRingCat.of A₀.1Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
namespace FGSubalgebralemma diagram_map {A₀ A₁ : FGSubalgebra R A} (h : A₀ ⟶ A₁) :
(diagram R A).map h =
CommRingCat.ofHom (Subalgebra.inclusion (R := R) (show A₀.1 ≤ A₁.1 from h.le)).toRingHom
:= rflSurrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
namespace FGSubalgebralemma cocone_pt : (cocone R A).pt = CommRingCat.of ASurrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
namespace FGSubalgebralemma cocone_ι_app (A₀ : FGSubalgebra R A) :
(cocone R A).ι.app A₀ = CommRingCat.ofHom A₀.1.val.toRingHomSurrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
namespace FGSubalgebralemma cocone_ι_app_apply (A₀ : FGSubalgebra R A) (x : A₀.1) :
(cocone R A).ι.app A₀ x = (x : A)The inverse diagram of spectra of finitely generated subalgebras.
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
namespace FGSubalgebradef specDiagram : (FGSubalgebra R A)ᵒᵖ ⥤ Scheme.{u}The cone of affine schemes induced by the subalgebra inclusion cocone.
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
namespace FGSubalgebradef specCone : Cone (specDiagram R A)The structure maps from the affine subalgebra spectra to the base spectrum.
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
namespace FGSubalgebradef specOver :
specDiagram R A ⟶ (Functor.const _).obj (Spec (CommRingCat.of R)) where
app i := Spec.map (CommRingCat.ofHom (algebraMap R i.unop.1))
naturality i j f := by
obtain ⟨A₁⟩ := i; obtain ⟨A₀⟩ := j
simp only [Functor.const_obj_obj, Functor.const_obj_map]
change (Spec.map (CommRingCat.ofHom (Subalgebra.inclusion (R := R)
(show A₀.1 ≤ A₁.1 from f.unop.le)).toRingHom) : Spec (CommRingCat.of A₁.1) ⟶ Spec
(CommRingCat.of A₀.1)) ≫
Spec.map (CommRingCat.ofHom (algebraMap R A₀.1)) = Spec.map (CommRingCat.ofHom (algebraMap
R A₁.1))
rw [← Spec.map_comp, ← CommRingCat.ofHom_comp]
congr 2Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
namespace FGSubalgebralemma specDiagram_obj (A₀ : FGSubalgebra R A) :
(specDiagram R A).obj (op A₀) = Spec (CommRingCat.of A₀.1)Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
namespace FGSubalgebralemma specDiagram_map {A₀ A₁ : FGSubalgebra R A} (h : A₀ ⟶ A₁) :
(specDiagram R A).map h.op =
Spec.map (CommRingCat.ofHom (Subalgebra.inclusion (R := R) (show A₀.1 ≤ A₁.1 from
h.le)).toRingHom) :=
rflSurrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
namespace FGSubalgebralemma specCone_pt : (specCone R A).pt = Spec (CommRingCat.of A)Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
namespace FGSubalgebralemma specCone_π_app (A₀ : FGSubalgebra R A) :
(specCone R A).π.app (op A₀) = Spec.map (CommRingCat.ofHom A₀.1.val.toRingHom)Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
namespace FGSubalgebralemma specOver_app (A₀ : FGSubalgebra R A) :
(specOver R A).app (op A₀) = Spec.map (CommRingCat.ofHom (algebraMap R A₀.1))Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
namespace FGSubalgebralemma specCone_π_comp_specOver :
(specCone R A).π ≫ specOver R A =
(Functor.const _).map (Spec.map (CommRingCat.ofHom (algebraMap R A)))Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
namespace FGSubalgebrainstance (i : (FGSubalgebra R A)ᵒᵖ) : IsAffine ((specDiagram R A).obj i)Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
namespace FGSubalgebrainstance (i : (FGSubalgebra R A)ᵒᵖ) : CompactSpace ((specDiagram R A).obj i)Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
namespace FGSubalgebrainstance (i : (FGSubalgebra R A)ᵒᵖ) : QuasiSeparatedSpace ((specDiagram R A).obj i)Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
namespace FGSubalgebrainstance {i j : (FGSubalgebra R A)ᵒᵖ} (f : i ⟶ j) : IsAffineHom ((specDiagram R A).map f)