Module

AffineSourceColimit.lean

Nyll.SchemeTheory.Modules.AffineSourceColimit

13 declarations indexed from sourceView source ↗

Module documentation

The original affine-morphism source as a colimit of its section spectra

For an actual affine morphism, pull back the base's affine locally directed cover. The pullback charts are identified with the literal spectra of the sections on the inverse-image opens. Their natural isomorphism transports the existing colimit of the pulled-back cover to a colimit with vertex the original source. No relative-spectrum comparison or effectivity is assumed.

Imports6

Mathlib.AlgebraicGeometry.AffineScheme
Mathlib.AlgebraicGeometry.Cover.Directed
Mathlib.AlgebraicGeometry.Morphisms.Affine
Mathlib.AlgebraicGeometry.Restrict
Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Mathlib.CategoryTheory.Limits.IsLimit

Imported by2

def

ringDiagram

L35 ↗

AlgebraicGeometry.Scheme.AffineSourceColimit.ringDiagram

Documentation

The actual direct-image section rings on the base's affine site.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite TopologicalSpace
namespace AlgebraicGeometry.Scheme.AffineSourceColimit
variable {T X : Scheme.{u}} (g : T ⟶ X)

Lean source · statement

def ringDiagram : X.AffineZariskiSiteᵒᵖ ⥤ CommRingCat.{u}

def

diagram

L39 ↗

AlgebraicGeometry.Scheme.AffineSourceColimit.diagram

Documentation

The diagram of spectra of these actual section rings.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite TopologicalSpace
namespace AlgebraicGeometry.Scheme.AffineSourceColimit
variable {T X : Scheme.{u}} (g : T ⟶ X)

Lean source · statement

def diagram : X.AffineZariskiSite ⥤ Scheme.{u}

abbrev

sourceCover

L42 ↗

AlgebraicGeometry.Scheme.AffineSourceColimit.sourceCover

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite TopologicalSpace
namespace AlgebraicGeometry.Scheme.AffineSourceColimit
variable {T X : Scheme.{u}} (g : T ⟶ X)

Lean source · statement

abbrev sourceCover : T.OpenCover

def

sourceDiagram

L45 ↗

AlgebraicGeometry.Scheme.AffineSourceColimit.sourceDiagram

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite TopologicalSpace
namespace AlgebraicGeometry.Scheme.AffineSourceColimit
variable {T X : Scheme.{u}} (g : T ⟶ X)

Lean source · statement

def sourceDiagram : X.AffineZariskiSite ⥤ Scheme.{u}

def

sourceCocone

L48 ↗

AlgebraicGeometry.Scheme.AffineSourceColimit.sourceCocone

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite TopologicalSpace
namespace AlgebraicGeometry.Scheme.AffineSourceColimit
variable {T X : Scheme.{u}} (g : T ⟶ X)

Lean source · statement

def sourceCocone : Cocone (sourceDiagram g)

def

sourceCoconeIsColimit

L51 ↗

AlgebraicGeometry.Scheme.AffineSourceColimit.sourceCoconeIsColimit

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite TopologicalSpace
namespace AlgebraicGeometry.Scheme.AffineSourceColimit
variable {T X : Scheme.{u}} (g : T ⟶ X)

Lean source · statement

def sourceCoconeIsColimit : IsColimit (sourceCocone g)

theorem

sourceCocone_app

L54 ↗

AlgebraicGeometry.Scheme.AffineSourceColimit.sourceCocone_app

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite TopologicalSpace
namespace AlgebraicGeometry.Scheme.AffineSourceColimit
variable {T X : Scheme.{u}} (g : T ⟶ X)

Lean source · statement

theorem sourceCocone_app (U : X.AffineZariskiSite) :
    (sourceCocone g).ι.app U = pullback.fst g U.1.ι

def

chartIso

L59 ↗

AlgebraicGeometry.Scheme.AffineSourceColimit.chartIso

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite TopologicalSpace
namespace AlgebraicGeometry.Scheme.AffineSourceColimit
variable {T X : Scheme.{u}} (g : T ⟶ X)
variable [IsAffineHom g]

Lean source · statement

def chartIso (U : X.AffineZariskiSite) :
    (sourceDiagram g).obj U ≅ Spec Γ(T, g ⁻¹ᵁ U.1)

theorem

chartIso_hom_fromSpec

L63 ↗

AlgebraicGeometry.Scheme.AffineSourceColimit.chartIso_hom_fromSpec

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite TopologicalSpace
namespace AlgebraicGeometry.Scheme.AffineSourceColimit
variable {T X : Scheme.{u}} (g : T ⟶ X)
variable [IsAffineHom g]

Lean source · statement

theorem chartIso_hom_fromSpec (U : X.AffineZariskiSite) :
    (chartIso g U).hom ≫ (U.2.preimage g).fromSpec = (sourceCocone g).ι.app U

theorem

diagram_map_fromSpec

L71 ↗

AlgebraicGeometry.Scheme.AffineSourceColimit.diagram_map_fromSpec

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite TopologicalSpace
namespace AlgebraicGeometry.Scheme.AffineSourceColimit
variable {T X : Scheme.{u}} (g : T ⟶ X)
variable [IsAffineHom g]

Lean source · statement

theorem diagram_map_fromSpec {U V : X.AffineZariskiSite} (i : U ⟶ V) :
    (diagram g).map i ≫ (V.2.preimage g).fromSpec = (U.2.preimage g).fromSpec

def

chartDiagramIso

L76 ↗

AlgebraicGeometry.Scheme.AffineSourceColimit.chartDiagramIso

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite TopologicalSpace
namespace AlgebraicGeometry.Scheme.AffineSourceColimit
variable {T X : Scheme.{u}} (g : T ⟶ X)
variable [IsAffineHom g]

Lean source · statement

def chartDiagramIso : sourceDiagram g ≅ diagram g

def

cocone

L103 ↗

AlgebraicGeometry.Scheme.AffineSourceColimit.cocone

Documentation

The literal source scheme and its affine inverse-image chart maps.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite TopologicalSpace
namespace AlgebraicGeometry.Scheme.AffineSourceColimit
variable {T X : Scheme.{u}} (g : T ⟶ X)
variable [IsAffineHom g]

Lean source · full declaration

def cocone : Cocone (diagram g) where
  pt := T
  ι :=
    { app U := (U.2.preimage g).fromSpec
      naturality {U V} i := by
        change (diagram g).map i ≫ (V.2.preimage g).fromSpec =
          (U.2.preimage g).fromSpec ≫ 𝟙 T
        rw [Category.comp_id]
        exact diagram_map_fromSpec g i }

def

coconeIsColimit

L116 ↗

AlgebraicGeometry.Scheme.AffineSourceColimit.coconeIsColimit

Documentation

The original source is the actual colimit of its affine section spectra. This is transported from the existing locally directed pullback-cover colimit, using the concrete chart isomorphisms above.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite TopologicalSpace
namespace AlgebraicGeometry.Scheme.AffineSourceColimit
variable {T X : Scheme.{u}} (g : T ⟶ X)
variable [IsAffineHom g]

Lean source · statement

def coconeIsColimit : IsColimit (cocone g)

Module documentation

The original affine-morphism source as a colimit of its section spectra

Declarations