NYLL
Module

Over.lean

Nyll.SchemeTheory.Pi1.Affine.Over
57 declarations indexed from sourceView source ↗

Module documentation

Category of schemes affine over an affine base

Imports3
  • Mathlib.AlgebraicGeometry.ColimitsOver
  • Mathlib.AlgebraicGeometry.Morphisms.Affine
  • Mathlib.AlgebraicGeometry.Morphisms.Flat
Imported by10

Declarations

def

pullbackId

L52 ↗
CategoryTheory.MorphismProperty.Over.pullbackId
Documentation

Pullback along the identity is naturally isomorphic to the identity on the relative category.

Source context 7 commands

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

@[expose] public section
universe w t u
noncomputable section
open CategoryTheory Limits Opposite TensorProduct
section
namespace CategoryTheory
variable {C : Type*} [Category C] (P Q : MorphismProperty C) [Q.IsMultiplicative]
  [P.IsStableUnderBaseChange] [Q.IsStableUnderBaseChange]
Lean source · statement
def MorphismProperty.Over.pullbackId [HasPullbacks C] (X : C) :
    MorphismProperty.Over.pullback P Q (𝟙 X) ≅ 𝟭 _
def

pullbackIso

L66 ↗
CategoryTheory.MorphismProperty.Over.pullbackIso
Documentation

Transport the relative category along an isomorphism of base objects.

Source context 7 commands

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

@[expose] public section
universe w t u
noncomputable section
open CategoryTheory Limits Opposite TensorProduct
section
namespace CategoryTheory
variable {C : Type*} [Category C] (P Q : MorphismProperty C) [Q.IsMultiplicative]
  [P.IsStableUnderBaseChange] [Q.IsStableUnderBaseChange]
Lean source · statement
def MorphismProperty.Over.pullbackIso [HasPullbacks C] {X Y : C} (e : X ≅ Y) :
    P.Over Q X ≌ P.Over Q Y
instance

top_isStableUnderBaseChange

L86 ↗
MorphismProperty.top_isStableUnderBaseChange
Source context 6 commands

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

@[expose] public section
universe w t u
noncomputable section
open CategoryTheory Limits Opposite TensorProduct
section
variable {C : Type*} [Category C]
Lean source · full declaration
instance MorphismProperty.top_isStableUnderBaseChange :
    (⊤ : MorphismProperty C).IsStableUnderBaseChange where
  of_isPullback _ _ := trivial
instance

(anonymous instance)

L90 ↗
Source context 6 commands

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

@[expose] public section
universe w t u
noncomputable section
open CategoryTheory Limits Opposite TensorProduct
section
variable {C : Type*} [Category C]
Lean source · full declaration
instance (P : MorphismProperty C) : (⊤ : MorphismProperty C).HasOfPostcompProperty P where
  of_postcomp _ _ _ _ := trivial
lemma

pullbackGluedIso_hom

L112 ↗
AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso_hom
Source context 11 commands

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

@[expose] public section
universe w t u
noncomputable section
open CategoryTheory Limits Opposite TensorProduct
namespace AlgebraicGeometry
section
variable {P Q : MorphismProperty Scheme.{u}} [Q.IsMultiplicative] [P.IsStableUnderBaseChange]
  [Q.IsStableUnderBaseChange] [P.IsMultiplicative]
variable {S : Scheme.{u}} {J : Type t} [Category J] (D : J ⥤ P.Over ⊤ S)
  {𝒰 : Scheme.OpenCover.{w} S} [Small.{u} 𝒰.I₀] [Category 𝒰.I₀] [Quiver.IsThin 𝒰.I₀]
  [𝒰.LocallyDirected]
variable (d : 𝒰.ColimitGluingData D)
--variable [∀ {i j : d.ι} (hij : d.ℬ i ≤ d.ℬ j),
--  PreservesColimitsOfShape J (MorphismProperty.Over.map Q (d.hPhom hij))]
variable [∀ (i j : 𝒰.I₀) (hij : i ⟶ j),
  PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (𝒰.trans hij))]
variable [IsZariskiLocalAtTarget P]
Lean source · statement
lemma Scheme.Cover.ColimitGluingData.pullbackGluedIso_hom (i : 𝒰.I₀) :
    (d.pullbackGluedIso i).hom.left ≫ colimit.ι d.relativeGluingData.functor i =
      pullback.fst _ _
def

mapCoconePullback

L126 ↗
AlgebraicGeometry.Scheme.Cover.ColimitGluingData.mapCoconePullback
Documentation

Identify the pullback of the glued cocone with the cocone on an individual cover chart.

Source context 11 commands

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

@[expose] public section
universe w t u
noncomputable section
open CategoryTheory Limits Opposite TensorProduct
namespace AlgebraicGeometry
section
variable {P Q : MorphismProperty Scheme.{u}} [Q.IsMultiplicative] [P.IsStableUnderBaseChange]
  [Q.IsStableUnderBaseChange] [P.IsMultiplicative]
variable {S : Scheme.{u}} {J : Type t} [Category J] (D : J ⥤ P.Over ⊤ S)
  {𝒰 : Scheme.OpenCover.{w} S} [Small.{u} 𝒰.I₀] [Category 𝒰.I₀] [Quiver.IsThin 𝒰.I₀]
  [𝒰.LocallyDirected]
variable (d : 𝒰.ColimitGluingData D)
--variable [∀ {i j : d.ι} (hij : d.ℬ i ≤ d.ℬ j),
--  PreservesColimitsOfShape J (MorphismProperty.Over.map Q (d.hPhom hij))]
variable [∀ (i j : 𝒰.I₀) (hij : i ⟶ j),
  PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (𝒰.trans hij))]
variable [IsZariskiLocalAtTarget P]
Lean source · statement
def Scheme.Cover.ColimitGluingData.mapCoconePullback (i : 𝒰.I₀) :
    (MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).mapCocone
      d.gluedCocone ≅ d.cocone i
lemma

Γ_isPushout

L168 ↗
AlgebraicGeometry.Γ_isPushout
Source context 7 commands

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

@[expose] public section
universe w t u
noncomputable section
open CategoryTheory Limits Opposite TensorProduct
namespace AlgebraicGeometry
section
variable {X Y S : Scheme.{u}} [IsAffine X] [IsAffine Y] [IsAffine S] {f : X ⟶ S} {g : Y ⟶ S}
Lean source · statement
lemma Γ_isPushout {P : Scheme.{u}} {fst : P ⟶ X} {snd : P ⟶ Y} (h : IsPullback fst snd f g) :
    IsPushout (f.app ⊤) (g.app ⊤) (fst.app ⊤) (snd.app ⊤)
def

ΓpullbackIsoPushout

L185 ↗
AlgebraicGeometry.ΓpullbackIsoPushout
Documentation

Global sections identify a pullback of affine schemes with the pushout of their section rings.

Source context 8 commands

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

@[expose] public section
universe w t u
noncomputable section
open CategoryTheory Limits Opposite TensorProduct
namespace AlgebraicGeometry
section
variable {X Y S : Scheme.{u}} [IsAffine X] [IsAffine Y] [IsAffine S] {f : X ⟶ S} {g : Y ⟶ S}
variable (f g)
Lean source · statement
def ΓpullbackIsoPushout : Γ(pullback f g, ⊤) ≅ pushout f.appTop g.appTop
lemma

inl_ΓpullbackIsoPushout_inv

L189 ↗
AlgebraicGeometry.inl_ΓpullbackIsoPushout_inv
Source context 8 commands

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

@[expose] public section
universe w t u
noncomputable section
open CategoryTheory Limits Opposite TensorProduct
namespace AlgebraicGeometry
section
variable {X Y S : Scheme.{u}} [IsAffine X] [IsAffine Y] [IsAffine S] {f : X ⟶ S} {g : Y ⟶ S}
variable (f g)
Lean source · statement
lemma inl_ΓpullbackIsoPushout_inv :
    pushout.inl f.appTop g.appTop ≫ (ΓpullbackIsoPushout f g).inv = (pullback.fst f g).appTop
lemma

inr_ΓpullbackIsoPushout_inv

L194 ↗
AlgebraicGeometry.inr_ΓpullbackIsoPushout_inv
Source context 8 commands

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

@[expose] public section
universe w t u
noncomputable section
open CategoryTheory Limits Opposite TensorProduct
namespace AlgebraicGeometry
section
variable {X Y S : Scheme.{u}} [IsAffine X] [IsAffine Y] [IsAffine S] {f : X ⟶ S} {g : Y ⟶ S}
variable (f g)
Lean source · statement
lemma inr_ΓpullbackIsoPushout_inv :
    pushout.inr f.appTop g.appTop ≫ (ΓpullbackIsoPushout f g).inv = (pullback.snd f g).appTop
lemma

app_fst_ΓpullbackIsoPushout_hom

L199 ↗
AlgebraicGeometry.app_fst_ΓpullbackIsoPushout_hom
Source context 8 commands

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

@[expose] public section
universe w t u
noncomputable section
open CategoryTheory Limits Opposite TensorProduct
namespace AlgebraicGeometry
section
variable {X Y S : Scheme.{u}} [IsAffine X] [IsAffine Y] [IsAffine S] {f : X ⟶ S} {g : Y ⟶ S}
variable (f g)
Lean source · statement
lemma app_fst_ΓpullbackIsoPushout_hom :
     (pullback.fst f g).appTop ≫ (ΓpullbackIsoPushout f g).hom =
        pushout.inl f.appTop g.appTop
lemma

app_snd_ΓpullbackIsoPushout_hom

L205 ↗
AlgebraicGeometry.app_snd_ΓpullbackIsoPushout_hom
Source context 8 commands

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

@[expose] public section
universe w t u
noncomputable section
open CategoryTheory Limits Opposite TensorProduct
namespace AlgebraicGeometry
section
variable {X Y S : Scheme.{u}} [IsAffine X] [IsAffine Y] [IsAffine S] {f : X ⟶ S} {g : Y ⟶ S}
variable (f g)
Lean source · statement
lemma app_snd_ΓpullbackIsoPushout_hom :
     (pullback.snd f g).appTop ≫ (ΓpullbackIsoPushout f g).hom =
        pushout.inr f.appTop g.appTop
def

Spec

L219 ↗
AlgebraicGeometry.Over.Spec
Documentation

Apply the spectrum functor to objects over the opposite of a commutative ring.

Source context 8 commands

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

@[expose] public section
universe w t u
noncomputable section
open CategoryTheory Limits Opposite TensorProduct
namespace AlgebraicGeometry
variable (S : Scheme.{u})
section General
variable (A : CommRingCat.{u})
Lean source · statement
def Over.Spec : Over (op A) ⥤ Over (Spec A)
def

Γ

L223 ↗
AlgebraicGeometry.Over.Γ
Documentation

Send a scheme over the base to its global sections under the section ring of the base.

Source context 8 commands

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

@[expose] public section
universe w t u
noncomputable section
open CategoryTheory Limits Opposite TensorProduct
namespace AlgebraicGeometry
variable (S : Scheme.{u})
section General
variable (A : CommRingCat.{u})
Lean source · statement
def Over.Γ : (Over S)ᵒᵖ ⥤ Under Γ(S, ⊤)
def

Affine

L229 ↗
AlgebraicGeometry.Affine
Documentation

The category of affine morphisms with target S.

Source context 6 commands

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

@[expose] public section
universe w t u
noncomputable section
open CategoryTheory Limits Opposite TensorProduct
namespace AlgebraicGeometry
variable (S : Scheme.{u})
Lean source · statement
def Affine : Type _
abbrev

mk

L233 ↗
AlgebraicGeometry.Affine.mk
Documentation

View an affine morphism as an object of the category of affine morphisms over its target.

Source context 7 commands

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

@[expose] public section
universe w t u
noncomputable section
open CategoryTheory Limits Opposite TensorProduct
namespace AlgebraicGeometry
variable (S : Scheme.{u})
variable {S} in
Lean source · statement
abbrev Affine.mk {X : Scheme.{u}} (f : X ⟶ S) [IsAffineHom f] : Affine S
instance

(anonymous instance)

L236 ↗
Source context 7 commands

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

@[expose] public section
universe w t u
noncomputable section
open CategoryTheory Limits Opposite TensorProduct
namespace AlgebraicGeometry
variable (S : Scheme.{u})
variable {S} in
Lean source · statement
instance : Category (Affine S)
instance

(anonymous instance)

L241 ↗
Source context 7 commands

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

@[expose] public section
universe w t u
noncomputable section
open CategoryTheory Limits Opposite TensorProduct
namespace AlgebraicGeometry
variable (S : Scheme.{u})
variable {S} in
Lean source · statement
instance (X : Affine S) : IsAffineHom X.hom
instance

affineHomOverCategory

L245 ↗
AlgebraicGeometry.Affine.affineHomOverCategory
Source context 8 commands

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

@[expose] public section
universe w t u
noncomputable section
open CategoryTheory Limits Opposite TensorProduct
namespace AlgebraicGeometry
variable (S : Scheme.{u})
variable {S} in
namespace Affine
Lean source · statement
instance affineHomOverCategory (S : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (⊤ : MorphismProperty Scheme.{u}) S)
instance

affineHomHasPullbacksAlong

L251 ↗
AlgebraicGeometry.Affine.affineHomHasPullbacksAlong
Source context 9 commands

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

@[expose] public section
universe w t u
noncomputable section
open CategoryTheory Limits Opposite TensorProduct
namespace AlgebraicGeometry
variable (S : Scheme.{u})
variable {S} in
namespace Affine
local instance affineHomOverCategory (S : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (⊤ : MorphismProperty Scheme.{u}) S) :=
  instCategoryAffine S
Lean source · statement
instance affineHomHasPullbacksAlong {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f
instance

affineHomIsStableUnderBaseChangeAlong

L256 ↗
AlgebraicGeometry.Affine.affineHomIsStableUnderBaseChangeAlong
Source context 10 commands

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

@[expose] public section
universe w t u
noncomputable section
open CategoryTheory Limits Opposite TensorProduct
namespace AlgebraicGeometry
variable (S : Scheme.{u})
variable {S} in
namespace Affine
local instance affineHomOverCategory (S : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (⊤ : MorphismProperty Scheme.{u}) S) :=
  instCategoryAffine S
local instance affineHomHasPullbacksAlong {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
Lean source · statement
instance affineHomIsStableUnderBaseChangeAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f
instance

affineHomIsStableUnderComposition

L262 ↗
AlgebraicGeometry.Affine.affineHomIsStableUnderComposition
Source context 11 commands

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

@[expose] public section
universe w t u
noncomputable section
open CategoryTheory Limits Opposite TensorProduct
namespace AlgebraicGeometry
variable (S : Scheme.{u})
variable {S} in
namespace Affine
local instance affineHomOverCategory (S : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (⊤ : MorphismProperty Scheme.{u}) S) :=
  instCategoryAffine S
local instance affineHomHasPullbacksAlong {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance affineHomIsStableUnderBaseChangeAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ isAffineHom_isStableUnderBaseChange.of_isPullback h hf⟩
Lean source · statement
instance affineHomIsStableUnderComposition :
    MorphismProperty.IsStableUnderComposition
      (@IsAffineHom : MorphismProperty Scheme.{u})
instance

affineHomHasAffineProperty

L270 ↗
AlgebraicGeometry.Affine.affineHomHasAffineProperty
Source context 12 commands

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

@[expose] public section
universe w t u
noncomputable section
open CategoryTheory Limits Opposite TensorProduct
namespace AlgebraicGeometry
variable (S : Scheme.{u})
variable {S} in
namespace Affine
local instance affineHomOverCategory (S : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (⊤ : MorphismProperty Scheme.{u}) S) :=
  instCategoryAffine S
local instance affineHomHasPullbacksAlong {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance affineHomIsStableUnderBaseChangeAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ isAffineHom_isStableUnderBaseChange.of_isPullback h hf⟩
local instance affineHomIsStableUnderComposition :
    MorphismProperty.IsStableUnderComposition
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  ⟨fun _ _ hf hg ↦ by
    let _ := hf
    let _ := hg
    infer_instance⟩
Lean source · full declaration
instance affineHomHasAffineProperty :
    HasAffineProperty
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (fun X _ _ _ ↦ IsAffine X) :=
  AlgebraicGeometry.instHasAffinePropertyIsAffineHomIsAffine
instance

affineHomIsZariskiLocalAtTarget

L276 ↗
AlgebraicGeometry.Affine.affineHomIsZariskiLocalAtTarget
Source context 13 commands

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

@[expose] public section
universe w t u
noncomputable section
open CategoryTheory Limits Opposite TensorProduct
namespace AlgebraicGeometry
variable (S : Scheme.{u})
variable {S} in
namespace Affine
local instance affineHomOverCategory (S : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (⊤ : MorphismProperty Scheme.{u}) S) :=
  instCategoryAffine S
local instance affineHomHasPullbacksAlong {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance affineHomIsStableUnderBaseChangeAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ isAffineHom_isStableUnderBaseChange.of_isPullback h hf⟩
local instance affineHomIsStableUnderComposition :
    MorphismProperty.IsStableUnderComposition
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  ⟨fun _ _ hf hg ↦ by
    let _ := hf
    let _ := hg
    infer_instance⟩
local instance affineHomHasAffineProperty :
    HasAffineProperty
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (fun X _ _ _ ↦ IsAffine X) :=
  AlgebraicGeometry.instHasAffinePropertyIsAffineHomIsAffine
Lean source · statement
instance affineHomIsZariskiLocalAtTarget :
    IsZariskiLocalAtTarget
      (@IsAffineHom : MorphismProperty Scheme.{u})
abbrev

pullback

L286 ↗
AlgebraicGeometry.Affine.pullback
Documentation

Base change affine morphisms along a morphism of schemes.

Source context 16 commands

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

@[expose] public section
universe w t u
noncomputable section
open CategoryTheory Limits Opposite TensorProduct
namespace AlgebraicGeometry
variable (S : Scheme.{u})
variable {S} in
namespace Affine
local instance affineHomOverCategory (S : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (⊤ : MorphismProperty Scheme.{u}) S) :=
  instCategoryAffine S
local instance affineHomHasPullbacksAlong {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance affineHomIsStableUnderBaseChangeAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ isAffineHom_isStableUnderBaseChange.of_isPullback h hf⟩
local instance affineHomIsStableUnderComposition :
    MorphismProperty.IsStableUnderComposition
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  ⟨fun _ _ hf hg ↦ by
    let _ := hf
    let _ := hg
    infer_instance⟩
local instance affineHomHasAffineProperty :
    HasAffineProperty
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (fun X _ _ _ ↦ IsAffine X) :=
  AlgebraicGeometry.instHasAffinePropertyIsAffineHomIsAffine
local instance affineHomIsZariskiLocalAtTarget :
    IsZariskiLocalAtTarget
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  (HasAffineProperty.iff.mp affineHomHasAffineProperty).1
section
variable {S} {T : Scheme.{u}}
Lean source · statement
abbrev pullback (f : T ⟶ S) : Affine S ⥤ Affine T
abbrev

map

L295 ↗
AlgebraicGeometry.Affine.map
Documentation

Compose affine morphisms with the given affine morphism of bases.

Source context 17 commands

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

@[expose] public section
universe w t u
noncomputable section
open CategoryTheory Limits Opposite TensorProduct
namespace AlgebraicGeometry
variable (S : Scheme.{u})
variable {S} in
namespace Affine
local instance affineHomOverCategory (S : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (⊤ : MorphismProperty Scheme.{u}) S) :=
  instCategoryAffine S
local instance affineHomHasPullbacksAlong {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance affineHomIsStableUnderBaseChangeAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ isAffineHom_isStableUnderBaseChange.of_isPullback h hf⟩
local instance affineHomIsStableUnderComposition :
    MorphismProperty.IsStableUnderComposition
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  ⟨fun _ _ hf hg ↦ by
    let _ := hf
    let _ := hg
    infer_instance⟩
local instance affineHomHasAffineProperty :
    HasAffineProperty
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (fun X _ _ _ ↦ IsAffine X) :=
  AlgebraicGeometry.instHasAffinePropertyIsAffineHomIsAffine
local instance affineHomIsZariskiLocalAtTarget :
    IsZariskiLocalAtTarget
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  (HasAffineProperty.iff.mp affineHomHasAffineProperty).1
section
variable {S} {T : Scheme.{u}}
variable (f : T ⟶ S)
Lean source · statement
abbrev map [IsAffineHom f] : Affine T ⥤ Affine S
abbrev

mapPullbackAdjunction

L303 ↗
AlgebraicGeometry.Affine.mapPullbackAdjunction
Documentation

Composition with an affine base morphism is left adjoint to base change.

Source context 17 commands

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

@[expose] public section
universe w t u
noncomputable section
open CategoryTheory Limits Opposite TensorProduct
namespace AlgebraicGeometry
variable (S : Scheme.{u})
variable {S} in
namespace Affine
local instance affineHomOverCategory (S : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (⊤ : MorphismProperty Scheme.{u}) S) :=
  instCategoryAffine S
local instance affineHomHasPullbacksAlong {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance affineHomIsStableUnderBaseChangeAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ isAffineHom_isStableUnderBaseChange.of_isPullback h hf⟩
local instance affineHomIsStableUnderComposition :
    MorphismProperty.IsStableUnderComposition
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  ⟨fun _ _ hf hg ↦ by
    let _ := hf
    let _ := hg
    infer_instance⟩
local instance affineHomHasAffineProperty :
    HasAffineProperty
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (fun X _ _ _ ↦ IsAffine X) :=
  AlgebraicGeometry.instHasAffinePropertyIsAffineHomIsAffine
local instance affineHomIsZariskiLocalAtTarget :
    IsZariskiLocalAtTarget
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  (HasAffineProperty.iff.mp affineHomHasAffineProperty).1
section
variable {S} {T : Scheme.{u}}
variable (f : T ⟶ S)
Lean source · statement
abbrev mapPullbackAdjunction [IsAffineHom f] :
    map (f := f) ⊣ Affine.pullback f
instance

(anonymous instance)

L311 ↗
Source context 17 commands

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

@[expose] public section
universe w t u
noncomputable section
open CategoryTheory Limits Opposite TensorProduct
namespace AlgebraicGeometry
variable (S : Scheme.{u})
variable {S} in
namespace Affine
local instance affineHomOverCategory (S : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (⊤ : MorphismProperty Scheme.{u}) S) :=
  instCategoryAffine S
local instance affineHomHasPullbacksAlong {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance affineHomIsStableUnderBaseChangeAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ isAffineHom_isStableUnderBaseChange.of_isPullback h hf⟩
local instance affineHomIsStableUnderComposition :
    MorphismProperty.IsStableUnderComposition
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  ⟨fun _ _ hf hg ↦ by
    let _ := hf
    let _ := hg
    infer_instance⟩
local instance affineHomHasAffineProperty :
    HasAffineProperty
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (fun X _ _ _ ↦ IsAffine X) :=
  AlgebraicGeometry.instHasAffinePropertyIsAffineHomIsAffine
local instance affineHomIsZariskiLocalAtTarget :
    IsZariskiLocalAtTarget
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  (HasAffineProperty.iff.mp affineHomHasAffineProperty).1
section
variable {S} {T : Scheme.{u}}
variable (f : T ⟶ S)
Lean source · statement
instance [IsAffineHom f] : (map (f := f)).IsLeftAdjoint
instance

(anonymous instance)

L314 ↗
Source context 17 commands

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

@[expose] public section
universe w t u
noncomputable section
open CategoryTheory Limits Opposite TensorProduct
namespace AlgebraicGeometry
variable (S : Scheme.{u})
variable {S} in
namespace Affine
local instance affineHomOverCategory (S : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (⊤ : MorphismProperty Scheme.{u}) S) :=
  instCategoryAffine S
local instance affineHomHasPullbacksAlong {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance affineHomIsStableUnderBaseChangeAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ isAffineHom_isStableUnderBaseChange.of_isPullback h hf⟩
local instance affineHomIsStableUnderComposition :
    MorphismProperty.IsStableUnderComposition
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  ⟨fun _ _ hf hg ↦ by
    let _ := hf
    let _ := hg
    infer_instance⟩
local instance affineHomHasAffineProperty :
    HasAffineProperty
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (fun X _ _ _ ↦ IsAffine X) :=
  AlgebraicGeometry.instHasAffinePropertyIsAffineHomIsAffine
local instance affineHomIsZariskiLocalAtTarget :
    IsZariskiLocalAtTarget
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  (HasAffineProperty.iff.mp affineHomHasAffineProperty).1
section
variable {S} {T : Scheme.{u}}
variable (f : T ⟶ S)
Lean source · statement
instance [IsAffineHom f] : (Affine.pullback f).IsRightAdjoint
instance

(anonymous instance)

L323 ↗
Source context 16 commands

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

@[expose] public section
universe w t u
noncomputable section
open CategoryTheory Limits Opposite TensorProduct
namespace AlgebraicGeometry
variable (S : Scheme.{u})
variable {S} in
namespace Affine
local instance affineHomOverCategory (S : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (⊤ : MorphismProperty Scheme.{u}) S) :=
  instCategoryAffine S
local instance affineHomHasPullbacksAlong {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance affineHomIsStableUnderBaseChangeAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ isAffineHom_isStableUnderBaseChange.of_isPullback h hf⟩
local instance affineHomIsStableUnderComposition :
    MorphismProperty.IsStableUnderComposition
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  ⟨fun _ _ hf hg ↦ by
    let _ := hf
    let _ := hg
    infer_instance⟩
local instance affineHomHasAffineProperty :
    HasAffineProperty
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (fun X _ _ _ ↦ IsAffine X) :=
  AlgebraicGeometry.instHasAffinePropertyIsAffineHomIsAffine
local instance affineHomIsZariskiLocalAtTarget :
    IsZariskiLocalAtTarget
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  (HasAffineProperty.iff.mp affineHomHasAffineProperty).1
section AffineBase
variable [IsAffine S]
Lean source · statement
instance (X : Affine S) : IsAffine ((Functor.fromPUnit S).obj X.right)
instance

(anonymous instance)

L325 ↗
Source context 16 commands

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

@[expose] public section
universe w t u
noncomputable section
open CategoryTheory Limits Opposite TensorProduct
namespace AlgebraicGeometry
variable (S : Scheme.{u})
variable {S} in
namespace Affine
local instance affineHomOverCategory (S : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (⊤ : MorphismProperty Scheme.{u}) S) :=
  instCategoryAffine S
local instance affineHomHasPullbacksAlong {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance affineHomIsStableUnderBaseChangeAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ isAffineHom_isStableUnderBaseChange.of_isPullback h hf⟩
local instance affineHomIsStableUnderComposition :
    MorphismProperty.IsStableUnderComposition
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  ⟨fun _ _ hf hg ↦ by
    let _ := hf
    let _ := hg
    infer_instance⟩
local instance affineHomHasAffineProperty :
    HasAffineProperty
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (fun X _ _ _ ↦ IsAffine X) :=
  AlgebraicGeometry.instHasAffinePropertyIsAffineHomIsAffine
local instance affineHomIsZariskiLocalAtTarget :
    IsZariskiLocalAtTarget
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  (HasAffineProperty.iff.mp affineHomHasAffineProperty).1
section AffineBase
variable [IsAffine S]
Lean source · statement
instance (X : Affine S) : IsAffine X.left
instance

(anonymous instance)

L328 ↗
Source context 16 commands

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

@[expose] public section
universe w t u
noncomputable section
open CategoryTheory Limits Opposite TensorProduct
namespace AlgebraicGeometry
variable (S : Scheme.{u})
variable {S} in
namespace Affine
local instance affineHomOverCategory (S : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (⊤ : MorphismProperty Scheme.{u}) S) :=
  instCategoryAffine S
local instance affineHomHasPullbacksAlong {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance affineHomIsStableUnderBaseChangeAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ isAffineHom_isStableUnderBaseChange.of_isPullback h hf⟩
local instance affineHomIsStableUnderComposition :
    MorphismProperty.IsStableUnderComposition
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  ⟨fun _ _ hf hg ↦ by
    let _ := hf
    let _ := hg
    infer_instance⟩
local instance affineHomHasAffineProperty :
    HasAffineProperty
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (fun X _ _ _ ↦ IsAffine X) :=
  AlgebraicGeometry.instHasAffinePropertyIsAffineHomIsAffine
local instance affineHomIsZariskiLocalAtTarget :
    IsZariskiLocalAtTarget
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  (HasAffineProperty.iff.mp affineHomHasAffineProperty).1
section AffineBase
variable [IsAffine S]
Lean source · statement
instance (X : Affine S) : IsAffine ((𝟭 Scheme).obj X.left)
def

toAffine

L331 ↗
AlgebraicGeometry.Affine.toAffine
Documentation

View affine morphisms over an affine base in the over category of affine schemes.

Source context 16 commands

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

@[expose] public section
universe w t u
noncomputable section
open CategoryTheory Limits Opposite TensorProduct
namespace AlgebraicGeometry
variable (S : Scheme.{u})
variable {S} in
namespace Affine
local instance affineHomOverCategory (S : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (⊤ : MorphismProperty Scheme.{u}) S) :=
  instCategoryAffine S
local instance affineHomHasPullbacksAlong {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance affineHomIsStableUnderBaseChangeAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ isAffineHom_isStableUnderBaseChange.of_isPullback h hf⟩
local instance affineHomIsStableUnderComposition :
    MorphismProperty.IsStableUnderComposition
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  ⟨fun _ _ hf hg ↦ by
    let _ := hf
    let _ := hg
    infer_instance⟩
local instance affineHomHasAffineProperty :
    HasAffineProperty
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (fun X _ _ _ ↦ IsAffine X) :=
  AlgebraicGeometry.instHasAffinePropertyIsAffineHomIsAffine
local instance affineHomIsZariskiLocalAtTarget :
    IsZariskiLocalAtTarget
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  (HasAffineProperty.iff.mp affineHomHasAffineProperty).1
section AffineBase
variable [IsAffine S]
Lean source · statement
def toAffine : Affine S ⥤ Over (AffineScheme.mk S inferInstance)
def

fromAffine

L339 ↗
AlgebraicGeometry.Affine.fromAffine
Documentation

Forget the affine-scheme packaging of an object over an affine base.

Source context 16 commands

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

@[expose] public section
universe w t u
noncomputable section
open CategoryTheory Limits Opposite TensorProduct
namespace AlgebraicGeometry
variable (S : Scheme.{u})
variable {S} in
namespace Affine
local instance affineHomOverCategory (S : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (⊤ : MorphismProperty Scheme.{u}) S) :=
  instCategoryAffine S
local instance affineHomHasPullbacksAlong {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance affineHomIsStableUnderBaseChangeAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ isAffineHom_isStableUnderBaseChange.of_isPullback h hf⟩
local instance affineHomIsStableUnderComposition :
    MorphismProperty.IsStableUnderComposition
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  ⟨fun _ _ hf hg ↦ by
    let _ := hf
    let _ := hg
    infer_instance⟩
local instance affineHomHasAffineProperty :
    HasAffineProperty
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (fun X _ _ _ ↦ IsAffine X) :=
  AlgebraicGeometry.instHasAffinePropertyIsAffineHomIsAffine
local instance affineHomIsZariskiLocalAtTarget :
    IsZariskiLocalAtTarget
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  (HasAffineProperty.iff.mp affineHomHasAffineProperty).1
section AffineBase
variable [IsAffine S]
Lean source · statement
def fromAffine : Over (AffineScheme.mk S inferInstance) ⥤ Affine S
lemma

toAffine_fromAffine

L350 ↗
AlgebraicGeometry.Affine.toAffine_fromAffine
Source context 16 commands

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

@[expose] public section
universe w t u
noncomputable section
open CategoryTheory Limits Opposite TensorProduct
namespace AlgebraicGeometry
variable (S : Scheme.{u})
variable {S} in
namespace Affine
local instance affineHomOverCategory (S : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (⊤ : MorphismProperty Scheme.{u}) S) :=
  instCategoryAffine S
local instance affineHomHasPullbacksAlong {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance affineHomIsStableUnderBaseChangeAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ isAffineHom_isStableUnderBaseChange.of_isPullback h hf⟩
local instance affineHomIsStableUnderComposition :
    MorphismProperty.IsStableUnderComposition
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  ⟨fun _ _ hf hg ↦ by
    let _ := hf
    let _ := hg
    infer_instance⟩
local instance affineHomHasAffineProperty :
    HasAffineProperty
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (fun X _ _ _ ↦ IsAffine X) :=
  AlgebraicGeometry.instHasAffinePropertyIsAffineHomIsAffine
local instance affineHomIsZariskiLocalAtTarget :
    IsZariskiLocalAtTarget
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  (HasAffineProperty.iff.mp affineHomHasAffineProperty).1
section AffineBase
variable [IsAffine S]
Lean source · statement
lemma toAffine_fromAffine : toAffine S ⋙ fromAffine S = 𝟭 _
lemma

fromAffine_toAffine

L351 ↗
AlgebraicGeometry.Affine.fromAffine_toAffine
Source context 16 commands

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

@[expose] public section
universe w t u
noncomputable section
open CategoryTheory Limits Opposite TensorProduct
namespace AlgebraicGeometry
variable (S : Scheme.{u})
variable {S} in
namespace Affine
local instance affineHomOverCategory (S : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (⊤ : MorphismProperty Scheme.{u}) S) :=
  instCategoryAffine S
local instance affineHomHasPullbacksAlong {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance affineHomIsStableUnderBaseChangeAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ isAffineHom_isStableUnderBaseChange.of_isPullback h hf⟩
local instance affineHomIsStableUnderComposition :
    MorphismProperty.IsStableUnderComposition
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  ⟨fun _ _ hf hg ↦ by
    let _ := hf
    let _ := hg
    infer_instance⟩
local instance affineHomHasAffineProperty :
    HasAffineProperty
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (fun X _ _ _ ↦ IsAffine X) :=
  AlgebraicGeometry.instHasAffinePropertyIsAffineHomIsAffine
local instance affineHomIsZariskiLocalAtTarget :
    IsZariskiLocalAtTarget
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  (HasAffineProperty.iff.mp affineHomHasAffineProperty).1
section AffineBase
variable [IsAffine S]
Lean source · statement
lemma fromAffine_toAffine : fromAffine S ⋙ toAffine S = 𝟭 _
def

toAffineEquiv

L355 ↗
AlgebraicGeometry.Affine.toAffineEquiv
Documentation

If S is affine, the category of affine morphisms with target S is equivalent to the over category of S viewed as affine scheme.

Source context 16 commands

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

@[expose] public section
universe w t u
noncomputable section
open CategoryTheory Limits Opposite TensorProduct
namespace AlgebraicGeometry
variable (S : Scheme.{u})
variable {S} in
namespace Affine
local instance affineHomOverCategory (S : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (⊤ : MorphismProperty Scheme.{u}) S) :=
  instCategoryAffine S
local instance affineHomHasPullbacksAlong {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance affineHomIsStableUnderBaseChangeAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ isAffineHom_isStableUnderBaseChange.of_isPullback h hf⟩
local instance affineHomIsStableUnderComposition :
    MorphismProperty.IsStableUnderComposition
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  ⟨fun _ _ hf hg ↦ by
    let _ := hf
    let _ := hg
    infer_instance⟩
local instance affineHomHasAffineProperty :
    HasAffineProperty
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (fun X _ _ _ ↦ IsAffine X) :=
  AlgebraicGeometry.instHasAffinePropertyIsAffineHomIsAffine
local instance affineHomIsZariskiLocalAtTarget :
    IsZariskiLocalAtTarget
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  (HasAffineProperty.iff.mp affineHomHasAffineProperty).1
section AffineBase
variable [IsAffine S]
Lean source · statement
def toAffineEquiv : Affine S ≌ Over (AffineScheme.mk S inferInstance)
instance

(anonymous instance)

L360 ↗
Source context 16 commands

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

@[expose] public section
universe w t u
noncomputable section
open CategoryTheory Limits Opposite TensorProduct
namespace AlgebraicGeometry
variable (S : Scheme.{u})
variable {S} in
namespace Affine
local instance affineHomOverCategory (S : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (⊤ : MorphismProperty Scheme.{u}) S) :=
  instCategoryAffine S
local instance affineHomHasPullbacksAlong {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance affineHomIsStableUnderBaseChangeAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ isAffineHom_isStableUnderBaseChange.of_isPullback h hf⟩
local instance affineHomIsStableUnderComposition :
    MorphismProperty.IsStableUnderComposition
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  ⟨fun _ _ hf hg ↦ by
    let _ := hf
    let _ := hg
    infer_instance⟩
local instance affineHomHasAffineProperty :
    HasAffineProperty
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (fun X _ _ _ ↦ IsAffine X) :=
  AlgebraicGeometry.instHasAffinePropertyIsAffineHomIsAffine
local instance affineHomIsZariskiLocalAtTarget :
    IsZariskiLocalAtTarget
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  (HasAffineProperty.iff.mp affineHomHasAffineProperty).1
section AffineBase
variable [IsAffine S]
Lean source · statement
instance : (toAffine S).IsEquivalence
instance

(anonymous instance)

L361 ↗
Source context 16 commands

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

@[expose] public section
universe w t u
noncomputable section
open CategoryTheory Limits Opposite TensorProduct
namespace AlgebraicGeometry
variable (S : Scheme.{u})
variable {S} in
namespace Affine
local instance affineHomOverCategory (S : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (⊤ : MorphismProperty Scheme.{u}) S) :=
  instCategoryAffine S
local instance affineHomHasPullbacksAlong {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance affineHomIsStableUnderBaseChangeAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ isAffineHom_isStableUnderBaseChange.of_isPullback h hf⟩
local instance affineHomIsStableUnderComposition :
    MorphismProperty.IsStableUnderComposition
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  ⟨fun _ _ hf hg ↦ by
    let _ := hf
    let _ := hg
    infer_instance⟩
local instance affineHomHasAffineProperty :
    HasAffineProperty
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (fun X _ _ _ ↦ IsAffine X) :=
  AlgebraicGeometry.instHasAffinePropertyIsAffineHomIsAffine
local instance affineHomIsZariskiLocalAtTarget :
    IsZariskiLocalAtTarget
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  (HasAffineProperty.iff.mp affineHomHasAffineProperty).1
section AffineBase
variable [IsAffine S]
Lean source · statement
instance : (fromAffine S).IsEquivalence
def

AffineΓ

L365 ↗
AlgebraicGeometry.Affine.Over.AffineΓ
Documentation

Apply global sections to affine schemes over the base, with values in the opposite under category.

Source context 16 commands

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

@[expose] public section
universe w t u
noncomputable section
open CategoryTheory Limits Opposite TensorProduct
namespace AlgebraicGeometry
variable (S : Scheme.{u})
variable {S} in
namespace Affine
local instance affineHomOverCategory (S : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (⊤ : MorphismProperty Scheme.{u}) S) :=
  instCategoryAffine S
local instance affineHomHasPullbacksAlong {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance affineHomIsStableUnderBaseChangeAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ isAffineHom_isStableUnderBaseChange.of_isPullback h hf⟩
local instance affineHomIsStableUnderComposition :
    MorphismProperty.IsStableUnderComposition
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  ⟨fun _ _ hf hg ↦ by
    let _ := hf
    let _ := hg
    infer_instance⟩
local instance affineHomHasAffineProperty :
    HasAffineProperty
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (fun X _ _ _ ↦ IsAffine X) :=
  AlgebraicGeometry.instHasAffinePropertyIsAffineHomIsAffine
local instance affineHomIsZariskiLocalAtTarget :
    IsZariskiLocalAtTarget
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  (HasAffineProperty.iff.mp affineHomHasAffineProperty).1
section AffineBase
variable [IsAffine S]
Lean source · statement
def Over.AffineΓ : Over (AffineScheme.mk S inferInstance) ⥤ (Under Γ(S, ⊤))ᵒᵖ
instance

(anonymous instance)

L368 ↗
Source context 16 commands

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

@[expose] public section
universe w t u
noncomputable section
open CategoryTheory Limits Opposite TensorProduct
namespace AlgebraicGeometry
variable (S : Scheme.{u})
variable {S} in
namespace Affine
local instance affineHomOverCategory (S : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (⊤ : MorphismProperty Scheme.{u}) S) :=
  instCategoryAffine S
local instance affineHomHasPullbacksAlong {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance affineHomIsStableUnderBaseChangeAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ isAffineHom_isStableUnderBaseChange.of_isPullback h hf⟩
local instance affineHomIsStableUnderComposition :
    MorphismProperty.IsStableUnderComposition
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  ⟨fun _ _ hf hg ↦ by
    let _ := hf
    let _ := hg
    infer_instance⟩
local instance affineHomHasAffineProperty :
    HasAffineProperty
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (fun X _ _ _ ↦ IsAffine X) :=
  AlgebraicGeometry.instHasAffinePropertyIsAffineHomIsAffine
local instance affineHomIsZariskiLocalAtTarget :
    IsZariskiLocalAtTarget
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  (HasAffineProperty.iff.mp affineHomHasAffineProperty).1
section AffineBase
variable [IsAffine S]
Lean source · statement
instance : (Over.AffineΓ S).IsEquivalence
def

Γ

L373 ↗
AlgebraicGeometry.Affine.Γ
Documentation

The global-sections equivalence from affine morphisms over an affine base to rings under its section ring.

Source context 16 commands

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

@[expose] public section
universe w t u
noncomputable section
open CategoryTheory Limits Opposite TensorProduct
namespace AlgebraicGeometry
variable (S : Scheme.{u})
variable {S} in
namespace Affine
local instance affineHomOverCategory (S : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (⊤ : MorphismProperty Scheme.{u}) S) :=
  instCategoryAffine S
local instance affineHomHasPullbacksAlong {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance affineHomIsStableUnderBaseChangeAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ isAffineHom_isStableUnderBaseChange.of_isPullback h hf⟩
local instance affineHomIsStableUnderComposition :
    MorphismProperty.IsStableUnderComposition
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  ⟨fun _ _ hf hg ↦ by
    let _ := hf
    let _ := hg
    infer_instance⟩
local instance affineHomHasAffineProperty :
    HasAffineProperty
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (fun X _ _ _ ↦ IsAffine X) :=
  AlgebraicGeometry.instHasAffinePropertyIsAffineHomIsAffine
local instance affineHomIsZariskiLocalAtTarget :
    IsZariskiLocalAtTarget
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  (HasAffineProperty.iff.mp affineHomHasAffineProperty).1
section AffineBase
variable [IsAffine S]
Lean source · statement
def Γ : (Affine S)ᵒᵖ ⥤ Under Γ(S, ⊤)
instance

(anonymous instance)

L376 ↗
Source context 16 commands

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

@[expose] public section
universe w t u
noncomputable section
open CategoryTheory Limits Opposite TensorProduct
namespace AlgebraicGeometry
variable (S : Scheme.{u})
variable {S} in
namespace Affine
local instance affineHomOverCategory (S : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (⊤ : MorphismProperty Scheme.{u}) S) :=
  instCategoryAffine S
local instance affineHomHasPullbacksAlong {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance affineHomIsStableUnderBaseChangeAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ isAffineHom_isStableUnderBaseChange.of_isPullback h hf⟩
local instance affineHomIsStableUnderComposition :
    MorphismProperty.IsStableUnderComposition
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  ⟨fun _ _ hf hg ↦ by
    let _ := hf
    let _ := hg
    infer_instance⟩
local instance affineHomHasAffineProperty :
    HasAffineProperty
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (fun X _ _ _ ↦ IsAffine X) :=
  AlgebraicGeometry.instHasAffinePropertyIsAffineHomIsAffine
local instance affineHomIsZariskiLocalAtTarget :
    IsZariskiLocalAtTarget
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  (HasAffineProperty.iff.mp affineHomHasAffineProperty).1
section AffineBase
variable [IsAffine S]
Lean source · statement
instance : (Γ S).IsEquivalence
def

pullbackIsoPushout

L388 ↗
AlgebraicGeometry.Affine.pullbackIsoPushout
Documentation

Identify the section ring of an affine base change with the corresponding pushout under the new base.

Source context 19 commands

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

@[expose] public section
universe w t u
noncomputable section
open CategoryTheory Limits Opposite TensorProduct
namespace AlgebraicGeometry
variable (S : Scheme.{u})
variable {S} in
namespace Affine
local instance affineHomOverCategory (S : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (⊤ : MorphismProperty Scheme.{u}) S) :=
  instCategoryAffine S
local instance affineHomHasPullbacksAlong {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance affineHomIsStableUnderBaseChangeAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ isAffineHom_isStableUnderBaseChange.of_isPullback h hf⟩
local instance affineHomIsStableUnderComposition :
    MorphismProperty.IsStableUnderComposition
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  ⟨fun _ _ hf hg ↦ by
    let _ := hf
    let _ := hg
    infer_instance⟩
local instance affineHomHasAffineProperty :
    HasAffineProperty
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (fun X _ _ _ ↦ IsAffine X) :=
  AlgebraicGeometry.instHasAffinePropertyIsAffineHomIsAffine
local instance affineHomIsZariskiLocalAtTarget :
    IsZariskiLocalAtTarget
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  (HasAffineProperty.iff.mp affineHomHasAffineProperty).1
section AffineBase
variable [IsAffine S]
section
variable {T : Scheme.{u}} (f : T ⟶ S) [IsAffine T]
variable {S}
Lean source · statement
def pullbackIsoPushout (X : (Affine S)ᵒᵖ) :
    (Γ T).obj (op ((Affine.pullback f).obj X.unop)) ≅
      Under.mk (pushout.inr ((Γ S).obj X).hom (f.app ⊤))
def

pullbackΓIso

L406 ↗
AlgebraicGeometry.Affine.pullbackΓIso
Documentation

Global sections turn affine base change into the pushout functor on section rings.

Source context 19 commands

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

@[expose] public section
universe w t u
noncomputable section
open CategoryTheory Limits Opposite TensorProduct
namespace AlgebraicGeometry
variable (S : Scheme.{u})
variable {S} in
namespace Affine
local instance affineHomOverCategory (S : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (⊤ : MorphismProperty Scheme.{u}) S) :=
  instCategoryAffine S
local instance affineHomHasPullbacksAlong {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance affineHomIsStableUnderBaseChangeAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ isAffineHom_isStableUnderBaseChange.of_isPullback h hf⟩
local instance affineHomIsStableUnderComposition :
    MorphismProperty.IsStableUnderComposition
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  ⟨fun _ _ hf hg ↦ by
    let _ := hf
    let _ := hg
    infer_instance⟩
local instance affineHomHasAffineProperty :
    HasAffineProperty
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (fun X _ _ _ ↦ IsAffine X) :=
  AlgebraicGeometry.instHasAffinePropertyIsAffineHomIsAffine
local instance affineHomIsZariskiLocalAtTarget :
    IsZariskiLocalAtTarget
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  (HasAffineProperty.iff.mp affineHomHasAffineProperty).1
section AffineBase
variable [IsAffine S]
section
variable {T : Scheme.{u}} (f : T ⟶ S) [IsAffine T]
variable {S}
Lean source · statement
def pullbackΓIso : (Affine.pullback f).op ⋙ Γ T ≅
    Γ S ⋙ Under.pushout (f.app ⊤)
instance

(anonymous instance)

L542 ↗
Source context 17 commands

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

@[expose] public section
universe w t u
noncomputable section
open CategoryTheory Limits Opposite TensorProduct
namespace AlgebraicGeometry
variable (S : Scheme.{u})
variable {S} in
namespace Affine
local instance affineHomOverCategory (S : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (⊤ : MorphismProperty Scheme.{u}) S) :=
  instCategoryAffine S
local instance affineHomHasPullbacksAlong {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance affineHomIsStableUnderBaseChangeAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ isAffineHom_isStableUnderBaseChange.of_isPullback h hf⟩
local instance affineHomIsStableUnderComposition :
    MorphismProperty.IsStableUnderComposition
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  ⟨fun _ _ hf hg ↦ by
    let _ := hf
    let _ := hg
    infer_instance⟩
local instance affineHomHasAffineProperty :
    HasAffineProperty
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (fun X _ _ _ ↦ IsAffine X) :=
  AlgebraicGeometry.instHasAffinePropertyIsAffineHomIsAffine
local instance affineHomIsZariskiLocalAtTarget :
    IsZariskiLocalAtTarget
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  (HasAffineProperty.iff.mp affineHomHasAffineProperty).1
section AffineBase
variable [IsAffine S]
variable {J : Type t} [Category J] [UnivLE.{t, u}]
Lean source · statement
instance : HasLimitsOfShape J (Affine S)ᵒᵖ
instance

hasColimitsOfShape_of_isAffine

L545 ↗
AlgebraicGeometry.Affine.hasColimitsOfShape_of_isAffine
Source context 17 commands

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

@[expose] public section
universe w t u
noncomputable section
open CategoryTheory Limits Opposite TensorProduct
namespace AlgebraicGeometry
variable (S : Scheme.{u})
variable {S} in
namespace Affine
local instance affineHomOverCategory (S : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (⊤ : MorphismProperty Scheme.{u}) S) :=
  instCategoryAffine S
local instance affineHomHasPullbacksAlong {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance affineHomIsStableUnderBaseChangeAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ isAffineHom_isStableUnderBaseChange.of_isPullback h hf⟩
local instance affineHomIsStableUnderComposition :
    MorphismProperty.IsStableUnderComposition
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  ⟨fun _ _ hf hg ↦ by
    let _ := hf
    let _ := hg
    infer_instance⟩
local instance affineHomHasAffineProperty :
    HasAffineProperty
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (fun X _ _ _ ↦ IsAffine X) :=
  AlgebraicGeometry.instHasAffinePropertyIsAffineHomIsAffine
local instance affineHomIsZariskiLocalAtTarget :
    IsZariskiLocalAtTarget
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  (HasAffineProperty.iff.mp affineHomHasAffineProperty).1
section AffineBase
variable [IsAffine S]
variable {J : Type t} [Category J] [UnivLE.{t, u}]
Lean source · statement
instance hasColimitsOfShape_of_isAffine : HasColimitsOfShape J (Affine S)
instance

(anonymous instance)

L548 ↗
Source context 17 commands

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

@[expose] public section
universe w t u
noncomputable section
open CategoryTheory Limits Opposite TensorProduct
namespace AlgebraicGeometry
variable (S : Scheme.{u})
variable {S} in
namespace Affine
local instance affineHomOverCategory (S : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (⊤ : MorphismProperty Scheme.{u}) S) :=
  instCategoryAffine S
local instance affineHomHasPullbacksAlong {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance affineHomIsStableUnderBaseChangeAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ isAffineHom_isStableUnderBaseChange.of_isPullback h hf⟩
local instance affineHomIsStableUnderComposition :
    MorphismProperty.IsStableUnderComposition
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  ⟨fun _ _ hf hg ↦ by
    let _ := hf
    let _ := hg
    infer_instance⟩
local instance affineHomHasAffineProperty :
    HasAffineProperty
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (fun X _ _ _ ↦ IsAffine X) :=
  AlgebraicGeometry.instHasAffinePropertyIsAffineHomIsAffine
local instance affineHomIsZariskiLocalAtTarget :
    IsZariskiLocalAtTarget
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  (HasAffineProperty.iff.mp affineHomHasAffineProperty).1
section AffineBase
variable [IsAffine S]
variable {J : Type t} [Category J] [UnivLE.{t, u}]
Lean source · statement
instance : HasColimitsOfShape J (MorphismProperty.Over @IsAffineHom ⊤ S)
instance

(anonymous instance)

L553 ↗
Source context 18 commands

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

@[expose] public section
universe w t u
noncomputable section
open CategoryTheory Limits Opposite TensorProduct
namespace AlgebraicGeometry
variable (S : Scheme.{u})
variable {S} in
namespace Affine
local instance affineHomOverCategory (S : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (⊤ : MorphismProperty Scheme.{u}) S) :=
  instCategoryAffine S
local instance affineHomHasPullbacksAlong {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance affineHomIsStableUnderBaseChangeAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ isAffineHom_isStableUnderBaseChange.of_isPullback h hf⟩
local instance affineHomIsStableUnderComposition :
    MorphismProperty.IsStableUnderComposition
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  ⟨fun _ _ hf hg ↦ by
    let _ := hf
    let _ := hg
    infer_instance⟩
local instance affineHomHasAffineProperty :
    HasAffineProperty
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (fun X _ _ _ ↦ IsAffine X) :=
  AlgebraicGeometry.instHasAffinePropertyIsAffineHomIsAffine
local instance affineHomIsZariskiLocalAtTarget :
    IsZariskiLocalAtTarget
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  (HasAffineProperty.iff.mp affineHomHasAffineProperty).1
section AffineBase
variable [IsAffine S]
variable {J : Type t} [Category J] [UnivLE.{t, u}]
variable (T : Scheme.{u}) [IsAffine T] (f : T ⟶ S)
Lean source · statement
instance [Flat f] : PreservesFiniteLimits (Under.pushout (f.app ⊤))
instance

preservesColimitsOfShapePullback

L558 ↗
AlgebraicGeometry.Affine.preservesColimitsOfShapePullback
Source context 18 commands

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

@[expose] public section
universe w t u
noncomputable section
open CategoryTheory Limits Opposite TensorProduct
namespace AlgebraicGeometry
variable (S : Scheme.{u})
variable {S} in
namespace Affine
local instance affineHomOverCategory (S : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (⊤ : MorphismProperty Scheme.{u}) S) :=
  instCategoryAffine S
local instance affineHomHasPullbacksAlong {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance affineHomIsStableUnderBaseChangeAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ isAffineHom_isStableUnderBaseChange.of_isPullback h hf⟩
local instance affineHomIsStableUnderComposition :
    MorphismProperty.IsStableUnderComposition
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  ⟨fun _ _ hf hg ↦ by
    let _ := hf
    let _ := hg
    infer_instance⟩
local instance affineHomHasAffineProperty :
    HasAffineProperty
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (fun X _ _ _ ↦ IsAffine X) :=
  AlgebraicGeometry.instHasAffinePropertyIsAffineHomIsAffine
local instance affineHomIsZariskiLocalAtTarget :
    IsZariskiLocalAtTarget
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  (HasAffineProperty.iff.mp affineHomHasAffineProperty).1
section AffineBase
variable [IsAffine S]
variable {J : Type t} [Category J] [UnivLE.{t, u}]
variable (T : Scheme.{u}) [IsAffine T] (f : T ⟶ S)
Lean source · statement
instance preservesColimitsOfShapePullback
    [hpush : PreservesLimitsOfShape Jᵒᵖ (Under.pushout (f.app ⊤))] :
    PreservesColimitsOfShape J (Affine.pullback f)
instance

(anonymous instance)

L569 ↗
Source context 18 commands

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

@[expose] public section
universe w t u
noncomputable section
open CategoryTheory Limits Opposite TensorProduct
namespace AlgebraicGeometry
variable (S : Scheme.{u})
variable {S} in
namespace Affine
local instance affineHomOverCategory (S : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (⊤ : MorphismProperty Scheme.{u}) S) :=
  instCategoryAffine S
local instance affineHomHasPullbacksAlong {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance affineHomIsStableUnderBaseChangeAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ isAffineHom_isStableUnderBaseChange.of_isPullback h hf⟩
local instance affineHomIsStableUnderComposition :
    MorphismProperty.IsStableUnderComposition
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  ⟨fun _ _ hf hg ↦ by
    let _ := hf
    let _ := hg
    infer_instance⟩
local instance affineHomHasAffineProperty :
    HasAffineProperty
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (fun X _ _ _ ↦ IsAffine X) :=
  AlgebraicGeometry.instHasAffinePropertyIsAffineHomIsAffine
local instance affineHomIsZariskiLocalAtTarget :
    IsZariskiLocalAtTarget
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  (HasAffineProperty.iff.mp affineHomHasAffineProperty).1
section AffineBase
variable [IsAffine S]
variable {J : Type t} [Category J] [UnivLE.{t, u}]
variable (T : Scheme.{u}) [IsAffine T] (f : T ⟶ S)
Lean source · full declaration
instance [Flat f] : PreservesFiniteColimits (Affine.pullback f) where
  preservesFiniteColimits _ := inferInstance
instance

(anonymous instance)

L572 ↗
Source context 18 commands

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

@[expose] public section
universe w t u
noncomputable section
open CategoryTheory Limits Opposite TensorProduct
namespace AlgebraicGeometry
variable (S : Scheme.{u})
variable {S} in
namespace Affine
local instance affineHomOverCategory (S : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (⊤ : MorphismProperty Scheme.{u}) S) :=
  instCategoryAffine S
local instance affineHomHasPullbacksAlong {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance affineHomIsStableUnderBaseChangeAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ isAffineHom_isStableUnderBaseChange.of_isPullback h hf⟩
local instance affineHomIsStableUnderComposition :
    MorphismProperty.IsStableUnderComposition
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  ⟨fun _ _ hf hg ↦ by
    let _ := hf
    let _ := hg
    infer_instance⟩
local instance affineHomHasAffineProperty :
    HasAffineProperty
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (fun X _ _ _ ↦ IsAffine X) :=
  AlgebraicGeometry.instHasAffinePropertyIsAffineHomIsAffine
local instance affineHomIsZariskiLocalAtTarget :
    IsZariskiLocalAtTarget
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  (HasAffineProperty.iff.mp affineHomHasAffineProperty).1
section AffineBase
variable [IsAffine S]
variable {J : Type t} [Category J] [UnivLE.{t, u}]
variable (T : Scheme.{u}) [IsAffine T] (f : T ⟶ S)
Lean source · statement
instance [Flat f] :
    PreservesFiniteColimits (MorphismProperty.Over.pullback @IsAffineHom ⊤ f)
instance

(anonymous instance)

L582 ↗
Source context 16 commands

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

@[expose] public section
universe w t u
noncomputable section
open CategoryTheory Limits Opposite TensorProduct
namespace AlgebraicGeometry
variable (S : Scheme.{u})
variable {S} in
namespace Affine
local instance affineHomOverCategory (S : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (⊤ : MorphismProperty Scheme.{u}) S) :=
  instCategoryAffine S
local instance affineHomHasPullbacksAlong {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance affineHomIsStableUnderBaseChangeAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ isAffineHom_isStableUnderBaseChange.of_isPullback h hf⟩
local instance affineHomIsStableUnderComposition :
    MorphismProperty.IsStableUnderComposition
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  ⟨fun _ _ hf hg ↦ by
    let _ := hf
    let _ := hg
    infer_instance⟩
local instance affineHomHasAffineProperty :
    HasAffineProperty
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (fun X _ _ _ ↦ IsAffine X) :=
  AlgebraicGeometry.instHasAffinePropertyIsAffineHomIsAffine
local instance affineHomIsZariskiLocalAtTarget :
    IsZariskiLocalAtTarget
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  (HasAffineProperty.iff.mp affineHomHasAffineProperty).1
section
variable {J : Type t} [UnivLE.{t, u}] [SmallCategory J] [FinCategory J] (D : J ⥤ Affine S)
Lean source · statement
instance (i) : IsAffine (S.directedAffineCover.X i)
def

colimitGluingData

L588 ↗
AlgebraicGeometry.Affine.colimitGluingData
Documentation

The local colimit cocones for a finite diagram of affine morphisms on the directed affine cover.

Source context 17 commands

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

@[expose] public section
universe w t u
noncomputable section
open CategoryTheory Limits Opposite TensorProduct
namespace AlgebraicGeometry
variable (S : Scheme.{u})
variable {S} in
namespace Affine
local instance affineHomOverCategory (S : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (⊤ : MorphismProperty Scheme.{u}) S) :=
  instCategoryAffine S
local instance affineHomHasPullbacksAlong {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance affineHomIsStableUnderBaseChangeAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ isAffineHom_isStableUnderBaseChange.of_isPullback h hf⟩
local instance affineHomIsStableUnderComposition :
    MorphismProperty.IsStableUnderComposition
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  ⟨fun _ _ hf hg ↦ by
    let _ := hf
    let _ := hg
    infer_instance⟩
local instance affineHomHasAffineProperty :
    HasAffineProperty
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (fun X _ _ _ ↦ IsAffine X) :=
  AlgebraicGeometry.instHasAffinePropertyIsAffineHomIsAffine
local instance affineHomIsZariskiLocalAtTarget :
    IsZariskiLocalAtTarget
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  (HasAffineProperty.iff.mp affineHomHasAffineProperty).1
section
variable {J : Type t} [UnivLE.{t, u}] [SmallCategory J] [FinCategory J] (D : J ⥤ Affine S)
variable {S} in
Lean source · full declaration
def colimitGluingData : S.directedAffineCover.ColimitGluingData D where
  cocone _ := colimit.cocone _
  isColimit _ := colimit.isColimit _
  prop_trans := by
    intro i j hij
    have hhom : (homOfLE (leOfHom hij) : i ⟶ j) = hij :=
      homOfLE_leOfHom hij
    have h₁ :
        Scheme.Cover.trans S.directedAffineCover hij =
          Scheme.Cover.trans S.directedAffineCover
            (homOfLE (leOfHom hij) : i ⟶ j) :=
      congrArg
        (fun k : i ⟶ j ↦ Scheme.Cover.trans S.directedAffineCover k)
        hhom.symm
    have h₂ :
        Scheme.Cover.trans S.directedAffineCover
            (homOfLE (leOfHom hij) : i ⟶ j) =
          S.homOfLE (leOfHom hij) :=
      Scheme.directedAffineCover_trans (X := S) (leOfHom hij)
    have htrans :
        Scheme.Cover.trans S.directedAffineCover hij =
          S.homOfLE (leOfHom hij) :=
      Eq.trans h₁ h₂
    have hi : IsAffine (S.directedAffineCover.X i) := i.2
    have hj : IsAffine (S.directedAffineCover.X j) := j.2
    have hAffine : IsAffineHom (S.homOfLE (leOfHom hij)) :=
      @isAffineHom_of_isAffine
        (S.directedAffineCover.X i) (S.directedAffineCover.X j)
        (S.homOfLE (leOfHom hij)) hi hj
    exact htrans.symm ▸ hAffine
instance

(anonymous instance)

L619 ↗
Source context 17 commands

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

@[expose] public section
universe w t u
noncomputable section
open CategoryTheory Limits Opposite TensorProduct
namespace AlgebraicGeometry
variable (S : Scheme.{u})
variable {S} in
namespace Affine
local instance affineHomOverCategory (S : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (⊤ : MorphismProperty Scheme.{u}) S) :=
  instCategoryAffine S
local instance affineHomHasPullbacksAlong {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance affineHomIsStableUnderBaseChangeAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ isAffineHom_isStableUnderBaseChange.of_isPullback h hf⟩
local instance affineHomIsStableUnderComposition :
    MorphismProperty.IsStableUnderComposition
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  ⟨fun _ _ hf hg ↦ by
    let _ := hf
    let _ := hg
    infer_instance⟩
local instance affineHomHasAffineProperty :
    HasAffineProperty
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (fun X _ _ _ ↦ IsAffine X) :=
  AlgebraicGeometry.instHasAffinePropertyIsAffineHomIsAffine
local instance affineHomIsZariskiLocalAtTarget :
    IsZariskiLocalAtTarget
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  (HasAffineProperty.iff.mp affineHomHasAffineProperty).1
section
variable {J : Type t} [UnivLE.{t, u}] [SmallCategory J] [FinCategory J] (D : J ⥤ Affine S)
variable {S} in
Lean source · full declaration
instance : HasColimit D where
  exists_colimit := by
    have hmap {U V : S.affineOpens} (hUV : U.1 ≤ V.1) :
        PreservesColimitsOfShape J (map (S.homOfLE hUV)) :=
      inferInstance
    have hpb {U V : S.affineOpens} (hUV : U.1 ≤ V.1) :
        PreservesColimitsOfShape J (Affine.pullback (S.homOfLE hUV)) :=
      inferInstance
    let _ : ∀ {i j : S.directedAffineCover.I₀} (hij : i ⟶ j),
        PreservesColimitsOfShape J
          (MorphismProperty.Over.pullback
            (@IsAffineHom : MorphismProperty Scheme.{u}) ⊤
            (S.directedAffineCover.trans hij)) :=
      fun {i j} hij ↦ by
        have hhom : (homOfLE (leOfHom hij) : i ⟶ j) = hij :=
          homOfLE_leOfHom hij
        have h₁ :
            Scheme.Cover.trans S.directedAffineCover hij =
              Scheme.Cover.trans S.directedAffineCover
                (homOfLE (leOfHom hij) : i ⟶ j) :=
          congrArg
            (fun k : i ⟶ j ↦ Scheme.Cover.trans S.directedAffineCover k)
            hhom.symm
        have h₂ :
            Scheme.Cover.trans S.directedAffineCover
                (homOfLE (leOfHom hij) : i ⟶ j) =
              S.homOfLE (leOfHom hij) :=
          Scheme.directedAffineCover_trans (X := S) (leOfHom hij)
        have htrans :
            Scheme.Cover.trans S.directedAffineCover hij =
              S.homOfLE (leOfHom hij) :=
          Eq.trans h₁ h₂
        have hraw : PreservesColimitsOfShape J
            (MorphismProperty.Over.pullback
              (@IsAffineHom : MorphismProperty Scheme.{u}) ⊤
              (S.homOfLE (leOfHom hij))) :=
          hpb (leOfHom hij)
        exact htrans.symm ▸ hraw
    use (colimitGluingData D).gluedCocone
    exact (colimitGluingData D).isColimitGluedCocone
instance

(anonymous instance)

L662 ↗
Source context 14 commands

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

@[expose] public section
universe w t u
noncomputable section
open CategoryTheory Limits Opposite TensorProduct
namespace AlgebraicGeometry
variable (S : Scheme.{u})
variable {S} in
namespace Affine
local instance affineHomOverCategory (S : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (⊤ : MorphismProperty Scheme.{u}) S) :=
  instCategoryAffine S
local instance affineHomHasPullbacksAlong {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance affineHomIsStableUnderBaseChangeAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ isAffineHom_isStableUnderBaseChange.of_isPullback h hf⟩
local instance affineHomIsStableUnderComposition :
    MorphismProperty.IsStableUnderComposition
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  ⟨fun _ _ hf hg ↦ by
    let _ := hf
    let _ := hg
    infer_instance⟩
local instance affineHomHasAffineProperty :
    HasAffineProperty
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (fun X _ _ _ ↦ IsAffine X) :=
  AlgebraicGeometry.instHasAffinePropertyIsAffineHomIsAffine
local instance affineHomIsZariskiLocalAtTarget :
    IsZariskiLocalAtTarget
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  (HasAffineProperty.iff.mp affineHomHasAffineProperty).1
Lean source · full declaration
instance : HasFiniteColimits (Affine S) where
  out J _ _ := { }
instance

(anonymous instance)

L665 ↗
Source context 14 commands

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

@[expose] public section
universe w t u
noncomputable section
open CategoryTheory Limits Opposite TensorProduct
namespace AlgebraicGeometry
variable (S : Scheme.{u})
variable {S} in
namespace Affine
local instance affineHomOverCategory (S : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (⊤ : MorphismProperty Scheme.{u}) S) :=
  instCategoryAffine S
local instance affineHomHasPullbacksAlong {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance affineHomIsStableUnderBaseChangeAlong
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsAffineHom : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ isAffineHom_isStableUnderBaseChange.of_isPullback h hf⟩
local instance affineHomIsStableUnderComposition :
    MorphismProperty.IsStableUnderComposition
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  ⟨fun _ _ hf hg ↦ by
    let _ := hf
    let _ := hg
    infer_instance⟩
local instance affineHomHasAffineProperty :
    HasAffineProperty
      (@IsAffineHom : MorphismProperty Scheme.{u})
      (fun X _ _ _ ↦ IsAffine X) :=
  AlgebraicGeometry.instHasAffinePropertyIsAffineHomIsAffine
local instance affineHomIsZariskiLocalAtTarget :
    IsZariskiLocalAtTarget
      (@IsAffineHom : MorphismProperty Scheme.{u}) :=
  (HasAffineProperty.iff.mp affineHomHasAffineProperty).1
Lean source · statement
instance {U : Scheme.{u}} (f : U ⟶ S) [IsOpenImmersion f] [IsAffine U] :
    PreservesFiniteColimits (Affine.pullback f)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.