Module

AffineTransitionImageDiagram.lean

Nyll.SchemeTheory.Descent.AffineTransitionImageDiagram

10 declarations indexed from sourceView source ↗

Module documentation

Actual scheme-theoretic image diagrams

A map into the vertex of a scheme cone gives compatible scheme-theoretic images at every stage. The image transition maps are constructed by the closed-immersion kernel factorization, and preserve affine transitions.

Imports4

Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Mathlib.AlgebraicGeometry.Morphisms.Separated
Mathlib.CategoryTheory.Limits.Cones

Imported by2

abbrev

stage

L32 ↗

AlgebraicGeometry.AffineTransitionImage.stage

Documentation

The scheme-theoretic image at the specified ambient stage.

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.AffineTransitionImage
universe u
variable {I : Type u} [Category.{u} I] (D : I ⥤ Scheme.{u}) (c : Cone D)
  {Z : Scheme.{u}} (j : Z ⟶ c.pt)

Lean source · statement

abbrev stage (i : I) : Scheme.{u}

abbrev

inclusion

L35 ↗

AlgebraicGeometry.AffineTransitionImage.inclusion

Documentation

The actual image inclusion into the ambient stage.

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.AffineTransitionImage
universe u
variable {I : Type u} [Category.{u} I] (D : I ⥤ Scheme.{u}) (c : Cone D)
  {Z : Scheme.{u}} (j : Z ⟶ c.pt)

Lean source · statement

abbrev inclusion (i : I) : stage D c j i ⟶ D.obj i

lemma

transition_kernel

L37 ↗

AlgebraicGeometry.AffineTransitionImage.transition_kernel

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.AffineTransitionImage
universe u
variable {I : Type u} [Category.{u} I] (D : I ⥤ Scheme.{u}) (c : Cone D)
  {Z : Scheme.{u}} (j : Z ⟶ c.pt)

Lean source · statement

lemma transition_kernel {i k : I} (f : i ⟶ k) :
    (inclusion D c j k).ker ≤ (inclusion D c j i ≫ D.map f).ker

def

transition

L47 ↗

AlgebraicGeometry.AffineTransitionImage.transition

Documentation

The transition morphism is the unique factorization through the next image.

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.AffineTransitionImage
universe u
variable {I : Type u} [Category.{u} I] (D : I ⥤ Scheme.{u}) (c : Cone D)
  {Z : Scheme.{u}} (j : Z ⟶ c.pt)

Lean source · statement

def transition {i k : I} (f : i ⟶ k) : stage D c j i ⟶ stage D c j k

lemma

transition_inclusion

L52 ↗

AlgebraicGeometry.AffineTransitionImage.transition_inclusion

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.AffineTransitionImage
universe u
variable {I : Type u} [Category.{u} I] (D : I ⥤ Scheme.{u}) (c : Cone D)
  {Z : Scheme.{u}} (j : Z ⟶ c.pt)

Lean source · statement

lemma transition_inclusion {i k : I} (f : i ⟶ k) :
    transition D c j f ≫ inclusion D c j k = inclusion D c j i ≫ D.map f

def

diagram

L58 ↗

AlgebraicGeometry.AffineTransitionImage.diagram

Documentation

The actual functor of scheme-theoretic images.

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.AffineTransitionImage
universe u
variable {I : Type u} [Category.{u} I] (D : I ⥤ Scheme.{u}) (c : Cone D)
  {Z : Scheme.{u}} (j : Z ⟶ c.pt)

Lean source · full declaration

def diagram : I ⥤ Scheme.{u} where
  obj i := stage D c j i
  map f := transition D c j f
  map_id i := by
    apply (cancel_mono (inclusion D c j i)).mp
    rw [transition_inclusion, D.map_id, Category.comp_id, Category.id_comp]
  map_comp f g := by
    apply (cancel_mono (inclusion D c j _)).mp
    rw [transition_inclusion, Category.assoc, transition_inclusion,
      ← Category.assoc, transition_inclusion, D.map_comp, Category.assoc]

def

inclusions

L70 ↗

AlgebraicGeometry.AffineTransitionImage.inclusions

Documentation

The image diagram has its actual closed inclusions into the ambient diagram.

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.AffineTransitionImage
universe u
variable {I : Type u} [Category.{u} I] (D : I ⥤ Scheme.{u}) (c : Cone D)
  {Z : Scheme.{u}} (j : Z ⟶ c.pt)

Lean source · full declaration

def inclusions : diagram D c j ⟶ D where
  app i := inclusion D c j i
  naturality _ _ f := transition_inclusion D c j f

def

cone

L76 ↗

AlgebraicGeometry.AffineTransitionImage.cone

Documentation

The original source maps to every image through the canonical image factor.

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.AffineTransitionImage
universe u
variable {I : Type u} [Category.{u} I] (D : I ⥤ Scheme.{u}) (c : Cone D)
  {Z : Scheme.{u}} (j : Z ⟶ c.pt)

Lean source · full declaration

def cone : Cone (diagram D c j) where
  pt := Z
  π.app i := (j ≫ c.π.app i).toImage
  π.naturality i k f := by
    change 𝟙 Z ≫ (j ≫ c.π.app k).toImage =
      (j ≫ c.π.app i).toImage ≫ transition D c j f
    rw [Category.id_comp]
    apply (cancel_mono (inclusion D c j k)).mp
    rw [Category.assoc, transition_inclusion, ← Category.assoc,
      Scheme.Hom.toImage_imageι, Scheme.Hom.toImage_imageι, Category.assoc, c.w f]

lemma

cone_projection_inclusion

L88 ↗

AlgebraicGeometry.AffineTransitionImage.cone_projection_inclusion

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.AffineTransitionImage
universe u
variable {I : Type u} [Category.{u} I] (D : I ⥤ Scheme.{u}) (c : Cone D)
  {Z : Scheme.{u}} (j : Z ⟶ c.pt)

Lean source · statement

lemma cone_projection_inclusion (i : I) :
    (cone D c j).π.app i ≫ inclusion D c j i = j ≫ c.π.app i

instance

(anonymous instance)

L93 ↗

Documentation

Affine ambient transitions induce affine transitions of the actual images.

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.AffineTransitionImage
universe u
variable {I : Type u} [Category.{u} I] (D : I ⥤ Scheme.{u}) (c : Cone D)
  {Z : Scheme.{u}} (j : Z ⟶ c.pt)

Lean source · statement

instance {i k : I} (f : i ⟶ k) [IsAffineHom (D.map f)] :
    IsAffineHom ((diagram D c j).map f)

Module documentation

Actual scheme-theoretic image diagrams

Declarations