Module

SubalgebraStages_nonempty_isLimit_cone.lean

Nyll.SchemeTheory.Descent.SubalgebraStages_nonempty_isLimit_cone

6 declarations indexed from sourceView source ↗

Module documentation

Subalgebra Stages nonempty is Limit cone

Imports7

Mathlib.Algebra.Category.Ring.FilteredColimits
Mathlib.CategoryTheory.Limits.Types.Filtered
Mathlib.CategoryTheory.Limits.Preserves.Basic
Mathlib.CategoryTheory.Limits.Opposites
Mathlib.CategoryTheory.Adjunction.Limits
Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Nyll.SchemeTheory.Descent.SubalgebraStages

Imported by8

def

ringDiagram

L39 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.SubalgebraStages_nonempty_isLimit_cone.LimBC.ringDiagram

Documentation

The diagram of stage subalgebras with their inclusion homomorphisms.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.SubalgebraStages_nonempty_isLimit_cone
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
universe u
namespace LimBC
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 ringDiagram : ι ⥤ CommRingCat.{u} where
  obj i := CommRingCat.of ↥(S i)
  map {i j} h := CommRingCat.ofHom (Subalgebra.inclusion (S.mono h.le)).toRingHom
  map_id _ := by ext; rfl
  map_comp _ _ := by ext; rfl

def

ringCocone

L46 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.SubalgebraStages_nonempty_isLimit_cone.LimBC.ringCocone

Documentation

The cocone of inclusions of the stage subalgebras into the ambient algebra.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.SubalgebraStages_nonempty_isLimit_cone
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
universe u
namespace LimBC
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 ringCocone : Cocone (ringDiagram S) where
  pt := CommRingCat.of A
  ι := { app i := CommRingCat.ofHom (S i).val.toRingHom
         naturality _ _ _ := by ext; rfl }

theorem

nonempty_isColimit_ringCocone

L51 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.SubalgebraStages_nonempty_isLimit_cone.LimBC.nonempty_isColimit_ringCocone

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.SubalgebraStages_nonempty_isLimit_cone
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
universe u
namespace LimBC
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

theorem nonempty_isColimit_ringCocone [IsDirected ι (· ≤ ·)] [Nonempty ι] (hS : ∀ a : A, ∃ i, a ∈ S
  i) :
    Nonempty (IsColimit (ringCocone S))

theorem

specCone_eq

L67 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.SubalgebraStages_nonempty_isLimit_cone.LimBC.specCone_eq

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.SubalgebraStages_nonempty_isLimit_cone
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
universe u
namespace LimBC
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

theorem specCone_eq : SubalgebraStages.specCone S = Scheme.Spec.mapCone (ringCocone S).op

theorem

nonempty_isLimit_specCone

L69 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.SubalgebraStages_nonempty_isLimit_cone.LimBC.nonempty_isLimit_specCone

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.SubalgebraStages_nonempty_isLimit_cone
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
universe u
namespace LimBC
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

theorem nonempty_isLimit_specCone [IsDirected ι (· ≤ ·)] [Nonempty ι] (hS : ∀ a : A, ∃ i, a ∈ S i) :
    Nonempty (IsLimit (SubalgebraStages.specCone S))

theorem

nonempty_isLimit_cone

L78 ↗

AlgebraicGeometry.SubalgebraStages.nonempty_isLimit_cone

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.SubalgebraStages_nonempty_isLimit_cone
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
universe u
open LimBC _root_.AlgebraicGeometry.SubalgebraStages in

Lean source · statement

theorem _root_.AlgebraicGeometry.SubalgebraStages.nonempty_isLimit_cone
    {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
    {ι : Type u} [Preorder ι] [IsDirected ι (· ≤ ·)] [Nonempty ι]
    (S : ι →o Subalgebra A₀ A) (hS : ∀ a : A, ∃ i, a ∈ S i)
    {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A₀)) :
    Nonempty (IsLimit (SubalgebraStages.cone S f))

Module documentation

Subalgebra Stages nonempty is Limit cone

Declarations

ringDiagram

ringCocone

nonempty_isColimit_ringCocone

specCone_eq

nonempty_isLimit_specCone

nonempty_isLimit_cone