NYLL
Module

InternalHom.lean

Nyll.SchemeTheory.Affine.WeilRestriction.InternalHom
39 declarations indexed from sourceView source ↗

Module documentation

Affine internal Homs over an affine base

This file promotes the algebraic affine Weil restriction from SchemeTheory.Affine.WeilRestriction.Basic to the corresponding geometric representability statement for affine schemes over Spec R.

For finite free A/R and finitely presented B/R, the functor sending an affine T over Spec R to morphisms over Spec R T x_{Spec R} Spec A -> Spec B is representable by the affine scheme associated to CommAlgCat.affineWeilRestriction.

Imports4
Imported by2

Declarations

def

allRingHom

L42 ↗
SchemeTheory.Affine.allRingHom
Documentation

The ring-homomorphism property satisfied by every homomorphism.

Source context 8 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
open CategoryTheory.MorphismProperty
open AlgebraicGeometry
open scoped TensorProduct
noncomputable section
universe u u₁ u₂ v₁ v₂ w
namespace SchemeTheory.Affine
Lean source · statement
def allRingHom
    {R S : Type u} [CommRing R] [CommRing S] (_ : R →+* S) : Prop
lemma

allRingHom_respectsIso

L45 ↗
SchemeTheory.Affine.allRingHom_respectsIso
Source context 8 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
open CategoryTheory.MorphismProperty
open AlgebraicGeometry
open scoped TensorProduct
noncomputable section
universe u u₁ u₂ v₁ v₂ w
namespace SchemeTheory.Affine
Lean source · statement
lemma allRingHom_respectsIso : RingHom.RespectsIso (@allRingHom.{u})
lemma

allRingHom_localizationAwayPreserves

L48 ↗
SchemeTheory.Affine.allRingHom_localizationAwayPreserves
Source context 8 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
open CategoryTheory.MorphismProperty
open AlgebraicGeometry
open scoped TensorProduct
noncomputable section
universe u u₁ u₂ v₁ v₂ w
namespace SchemeTheory.Affine
Lean source · statement
lemma allRingHom_localizationAwayPreserves :
    RingHom.LocalizationAwayPreserves (@allRingHom.{u})
lemma

allRingHom_ofLocalizationSpan

L52 ↗
SchemeTheory.Affine.allRingHom_ofLocalizationSpan
Source context 8 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
open CategoryTheory.MorphismProperty
open AlgebraicGeometry
open scoped TensorProduct
noncomputable section
universe u u₁ u₂ v₁ v₂ w
namespace SchemeTheory.Affine
Lean source · statement
lemma allRingHom_ofLocalizationSpan :
    RingHom.OfLocalizationSpan (@allRingHom.{u})
abbrev

affineHomProperty

L57 ↗
SchemeTheory.Affine.affineHomProperty
Documentation

The morphism property selecting affine morphisms of schemes.

Source context 8 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
open CategoryTheory.MorphismProperty
open AlgebraicGeometry
open scoped TensorProduct
noncomputable section
universe u u₁ u₂ v₁ v₂ w
namespace SchemeTheory.Affine
Lean source · statement
abbrev affineHomProperty : MorphismProperty Scheme.{u}
instance

(anonymous instance)

L59 ↗
Source context 8 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
open CategoryTheory.MorphismProperty
open AlgebraicGeometry
open scoped TensorProduct
noncomputable section
universe u u₁ u₂ v₁ v₂ w
namespace SchemeTheory.Affine
Lean source · statement
instance : HasAffineProperty (affineHomProperty : MorphismProperty Scheme.{u})
    (affineAnd (@allRingHom.{u}))
def

allUnderInverse

L68 ↗
SchemeTheory.Affine.allUnderInverse
Documentation

View a ring under R in the under-category restricted by the universal ring-homomorphism property.

Source context 9 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
open CategoryTheory.MorphismProperty
open AlgebraicGeometry
open scoped TensorProduct
noncomputable section
universe u u₁ u₂ v₁ v₂ w
namespace SchemeTheory.Affine
local instance : HasAffineProperty (affineHomProperty : MorphismProperty Scheme.{u})
    (affineAnd (@allRingHom.{u})) :=
  (HasAffineProperty.affineAnd_iff _ allRingHom_respectsIso
    allRingHom_localizationAwayPreserves allRingHom_ofLocalizationSpan).2 (by
      intro X Y f
      simp [affineHomProperty, allRingHom])
Lean source · statement
def allUnderInverse (R : CommRingCat.{u}) :
    Under R ⥤ (RingHom.toMorphismProperty (@allRingHom.{u})).Under ⊤ R
def

allUnderEquiv

L75 ↗
SchemeTheory.Affine.allUnderEquiv
Documentation

The restricted under-category for the universal ring-homomorphism property is equivalent to the category of rings under R.

Source context 9 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
open CategoryTheory.MorphismProperty
open AlgebraicGeometry
open scoped TensorProduct
noncomputable section
universe u u₁ u₂ v₁ v₂ w
namespace SchemeTheory.Affine
local instance : HasAffineProperty (affineHomProperty : MorphismProperty Scheme.{u})
    (affineAnd (@allRingHom.{u})) :=
  (HasAffineProperty.affineAnd_iff _ allRingHom_respectsIso
    allRingHom_localizationAwayPreserves allRingHom_ofLocalizationSpan).2 (by
      intro X Y f
      simp [affineHomProperty, allRingHom])
Lean source · statement
def allUnderEquiv (R : CommRingCat.{u}) :
    (RingHom.toMorphismProperty (@allRingHom.{u})).Under ⊤ R ≌ Under R
def

affineAlgebraEquiv

L86 ↗
SchemeTheory.Affine.affineAlgebraEquiv
Documentation

Affine schemes over Spec R, with arrows reversed, are equivalent to commutative R-algebras.

Source context 9 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
open CategoryTheory.MorphismProperty
open AlgebraicGeometry
open scoped TensorProduct
noncomputable section
universe u u₁ u₂ v₁ v₂ w
namespace SchemeTheory.Affine
local instance : HasAffineProperty (affineHomProperty : MorphismProperty Scheme.{u})
    (affineAnd (@allRingHom.{u})) :=
  (HasAffineProperty.affineAnd_iff _ allRingHom_respectsIso
    allRingHom_localizationAwayPreserves allRingHom_ofLocalizationSpan).2 (by
      intro X Y f
      simp [affineHomProperty, allRingHom])
Lean source · statement
def affineAlgebraEquiv (R : CommRingCat.{u}) :
    (affineHomProperty.Over ⊤ (Spec R))ᵒᵖ ≌
      CommAlgCat.{u} R
def

specOverFunctor

L95 ↗
SchemeTheory.Affine.specOverFunctor
Documentation

The spectrum functor from commutative R-algebras, with arrows reversed, to schemes over Spec R.

Source context 9 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
open CategoryTheory.MorphismProperty
open AlgebraicGeometry
open scoped TensorProduct
noncomputable section
universe u u₁ u₂ v₁ v₂ w
namespace SchemeTheory.Affine
local instance : HasAffineProperty (affineHomProperty : MorphismProperty Scheme.{u})
    (affineAnd (@allRingHom.{u})) :=
  (HasAffineProperty.affineAnd_iff _ allRingHom_respectsIso
    allRingHom_localizationAwayPreserves allRingHom_ofLocalizationSpan).2 (by
      intro X Y f
      simp [affineHomProperty, allRingHom])
Lean source · statement
def specOverFunctor (R : CommRingCat.{u}) :
    (CommAlgCat.{u} R)ᵒᵖ ⥤ Over (Spec R)
def

specOverFunctorFullyFaithful

L102 ↗
SchemeTheory.Affine.specOverFunctorFullyFaithful
Documentation

The spectrum functor on commutative R-algebras is fully faithful over Spec R.

Source context 9 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
open CategoryTheory.MorphismProperty
open AlgebraicGeometry
open scoped TensorProduct
noncomputable section
universe u u₁ u₂ v₁ v₂ w
namespace SchemeTheory.Affine
local instance : HasAffineProperty (affineHomProperty : MorphismProperty Scheme.{u})
    (affineAnd (@allRingHom.{u})) :=
  (HasAffineProperty.affineAnd_iff _ allRingHom_respectsIso
    allRingHom_localizationAwayPreserves allRingHom_ofLocalizationSpan).2 (by
      intro X Y f
      simp [affineHomProperty, allRingHom])
Lean source · statement
def specOverFunctorFullyFaithful (R : CommRingCat.{u}) :
    (specOverFunctor R).FullyFaithful
abbrev

affineForget

L109 ↗
SchemeTheory.Affine.affineForget
Documentation

Forget that the source of a scheme over Spec R is affine.

Source context 9 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
open CategoryTheory.MorphismProperty
open AlgebraicGeometry
open scoped TensorProduct
noncomputable section
universe u u₁ u₂ v₁ v₂ w
namespace SchemeTheory.Affine
local instance : HasAffineProperty (affineHomProperty : MorphismProperty Scheme.{u})
    (affineAnd (@allRingHom.{u})) :=
  (HasAffineProperty.affineAnd_iff _ allRingHom_respectsIso
    allRingHom_localizationAwayPreserves allRingHom_ofLocalizationSpan).2 (by
      intro X Y f
      simp [affineHomProperty, allRingHom])
Lean source · statement
abbrev affineForget (R : CommRingCat.{u}) :
    affineHomProperty.Over ⊤ (Spec R) ⥤ Over (Spec R)
abbrev

affineSpecGamma

L114 ↗
SchemeTheory.Affine.affineSpecGamma
Documentation

Send an affine scheme over Spec R to the spectrum of its global-sections R-algebra.

Source context 9 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
open CategoryTheory.MorphismProperty
open AlgebraicGeometry
open scoped TensorProduct
noncomputable section
universe u u₁ u₂ v₁ v₂ w
namespace SchemeTheory.Affine
local instance : HasAffineProperty (affineHomProperty : MorphismProperty Scheme.{u})
    (affineAnd (@allRingHom.{u})) :=
  (HasAffineProperty.affineAnd_iff _ allRingHom_respectsIso
    allRingHom_localizationAwayPreserves allRingHom_ofLocalizationSpan).2 (by
      intro X Y f
      simp [affineHomProperty, allRingHom])
Lean source · statement
abbrev affineSpecGamma (R : CommRingCat.{u}) :
    affineHomProperty.Over ⊤ (Spec R) ⥤ Over (Spec R)
def

affineToSpecGammaIso

L120 ↗
SchemeTheory.Affine.affineToSpecGammaIso
Documentation

Every affine scheme over Spec R is naturally isomorphic, over Spec R, to the spectrum of its global sections.

Source context 9 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
open CategoryTheory.MorphismProperty
open AlgebraicGeometry
open scoped TensorProduct
noncomputable section
universe u u₁ u₂ v₁ v₂ w
namespace SchemeTheory.Affine
local instance : HasAffineProperty (affineHomProperty : MorphismProperty Scheme.{u})
    (affineAnd (@allRingHom.{u})) :=
  (HasAffineProperty.affineAnd_iff _ allRingHom_respectsIso
    allRingHom_localizationAwayPreserves allRingHom_ofLocalizationSpan).2 (by
      intro X Y f
      simp [affineHomProperty, allRingHom])
Lean source · statement
def affineToSpecGammaIso (R : CommRingCat.{u}) :
    affineForget R ≅ affineSpecGamma R
def

specTensorIso

L151 ↗
SchemeTheory.Affine.specTensorIso
Documentation

Taking spectra identifies tensoring R-algebras with A with fibre products by Spec A over Spec R.

Source context 9 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
open CategoryTheory.MorphismProperty
open AlgebraicGeometry
open scoped TensorProduct
noncomputable section
universe u u₁ u₂ v₁ v₂ w
namespace SchemeTheory.Affine
local instance : HasAffineProperty (affineHomProperty : MorphismProperty Scheme.{u})
    (affineAnd (@allRingHom.{u})) :=
  (HasAffineProperty.affineAnd_iff _ allRingHom_respectsIso
    allRingHom_localizationAwayPreserves allRingHom_ofLocalizationSpan).2 (by
      intro X Y f
      simp [affineHomProperty, allRingHom])
Lean source · statement
def specTensorIso
    (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A] :
    (MonoidalCategory.tensorRight (CommAlgCat.of R A)).op ⋙
        specOverFunctor (CommRingCat.of R) ≅
      specOverFunctor (CommRingCat.of R) ⋙
        MonoidalCategory.tensorRight
          ((specOverFunctor (CommRingCat.of R)).obj
            (Opposite.op (CommAlgCat.of R A)))
def

corepresentableByCompEquivalence

L205 ↗
SchemeTheory.Affine.corepresentableByCompEquivalence
Documentation

Transport a corepresentation of a functor through an equivalence of its source category.

Source context 9 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
open CategoryTheory.MorphismProperty
open AlgebraicGeometry
open scoped TensorProduct
noncomputable section
universe u u₁ u₂ v₁ v₂ w
namespace SchemeTheory.Affine
local instance : HasAffineProperty (affineHomProperty : MorphismProperty Scheme.{u})
    (affineAnd (@allRingHom.{u})) :=
  (HasAffineProperty.affineAnd_iff _ allRingHom_respectsIso
    allRingHom_localizationAwayPreserves allRingHom_ofLocalizationSpan).2 (by
      intro X Y f
      simp [affineHomProperty, allRingHom])
Lean source · full declaration
def corepresentableByCompEquivalence
    {C : Type u₁} {D : Type u₂} [Category.{v₁} C] [Category.{v₂} D]
    (E : C ≌ D) {F : D ⥤ Type w} {H : D} (r : F.CorepresentableBy H) :
    (E.functor ⋙ F).CorepresentableBy (E.inverse.obj H) where
  homEquiv {Y} :=
    (E.symm.toAdjunction.homEquiv H Y).trans r.homEquiv
  homEquiv_comp {Y Y'} g f := by
    change r.homEquiv (E.symm.toAdjunction.homEquiv H Y' (f ≫ g)) = _
    rw [E.symm.toAdjunction.homEquiv_naturality_right]
    exact r.homEquiv_comp _ _
def

representableByOfCorepresentableOp

L218 ↗
SchemeTheory.Affine.representableByOfCorepresentableOp
Documentation

A corepresentation on the opposite category gives a representation of the corresponding presheaf.

Source context 9 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
open CategoryTheory.MorphismProperty
open AlgebraicGeometry
open scoped TensorProduct
noncomputable section
universe u u₁ u₂ v₁ v₂ w
namespace SchemeTheory.Affine
local instance : HasAffineProperty (affineHomProperty : MorphismProperty Scheme.{u})
    (affineAnd (@allRingHom.{u})) :=
  (HasAffineProperty.affineAnd_iff _ allRingHom_respectsIso
    allRingHom_localizationAwayPreserves allRingHom_ofLocalizationSpan).2 (by
      intro X Y f
      simp [affineHomProperty, allRingHom])
Lean source · full declaration
def representableByOfCorepresentableOp
    {C : Type u₁} [Category.{v₁} C] {F : Cᵒᵖ ⥤ Type w} {W : Cᵒᵖ}
    (r : F.CorepresentableBy W) : F.RepresentableBy W.unop where
  homEquiv {X} := (opEquiv W (Opposite.op X)).symm.trans r.homEquiv
  homEquiv_comp {X X'} f g := by
    change r.homEquiv ((f ≫ g).op) = F.map f.op (r.homEquiv g.op)
    exact r.homEquiv_comp f.op g.op
lemma

map_op_comp

L226 ↗
SchemeTheory.Affine.map_op_comp
Source context 9 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
open CategoryTheory.MorphismProperty
open AlgebraicGeometry
open scoped TensorProduct
noncomputable section
universe u u₁ u₂ v₁ v₂ w
namespace SchemeTheory.Affine
local instance : HasAffineProperty (affineHomProperty : MorphismProperty Scheme.{u})
    (affineAnd (@allRingHom.{u})) :=
  (HasAffineProperty.affineAnd_iff _ allRingHom_respectsIso
    allRingHom_localizationAwayPreserves allRingHom_ofLocalizationSpan).2 (by
      intro X Y f
      simp [affineHomProperty, allRingHom])
Lean source · statement
lemma map_op_comp
    {C : Type u₁} {D : Type u₂} [Category.{v₁} C] [Category.{v₂} D]
    (F : Cᵒᵖ ⥤ D) {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
    F.map (f ≫ g).op = F.map g.op ≫ F.map f.op
abbrev

tensorRightAlg

L240 ↗
SchemeTheory.Affine.tensorRightAlg
Documentation

The functor tensoring commutative R-algebras on the right with A.

Source context 11 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
open CategoryTheory.MorphismProperty
open AlgebraicGeometry
open scoped TensorProduct
noncomputable section
universe u u₁ u₂ v₁ v₂ w
namespace SchemeTheory.Affine
local instance : HasAffineProperty (affineHomProperty : MorphismProperty Scheme.{u})
    (affineAnd (@allRingHom.{u})) :=
  (HasAffineProperty.affineAnd_iff _ allRingHom_respectsIso
    allRingHom_localizationAwayPreserves allRingHom_ofLocalizationSpan).2 (by
      intro X Y f
      simp [affineHomProperty, allRingHom])
section Weil
variable {R A B : Type u} [CommRing R] [CommRing A] [CommRing B]
  [Algebra R A] [Algebra R B] [Module.Free R A] [Module.Finite R A]
  [Algebra.FinitePresentation R B]
Lean source · statement
abbrev tensorRightAlg : CommAlgCat.{u} R ⥤ CommAlgCat.{u} R
abbrev

algebraHomFunctor

L244 ↗
SchemeTheory.Affine.algebraHomFunctor
Documentation

The functor sending an R-algebra C to R-algebra homomorphisms from B to C tensor A.

Source context 11 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
open CategoryTheory.MorphismProperty
open AlgebraicGeometry
open scoped TensorProduct
noncomputable section
universe u u₁ u₂ v₁ v₂ w
namespace SchemeTheory.Affine
local instance : HasAffineProperty (affineHomProperty : MorphismProperty Scheme.{u})
    (affineAnd (@allRingHom.{u})) :=
  (HasAffineProperty.affineAnd_iff _ allRingHom_respectsIso
    allRingHom_localizationAwayPreserves allRingHom_ofLocalizationSpan).2 (by
      intro X Y f
      simp [affineHomProperty, allRingHom])
section Weil
variable {R A B : Type u} [CommRing R] [CommRing A] [CommRing B]
  [Algebra R A] [Algebra R B] [Module.Free R A] [Module.Finite R A]
  [Algebra.FinitePresentation R B]
Lean source · statement
abbrev algebraHomFunctor : CommAlgCat.{u} R ⥤ Type u
def

algebraTargetSource

L250 ↗
SchemeTheory.Affine.algebraTargetSource
Documentation

The finitely presented algebra B as an object where the partial left adjoint to tensoring with A is defined.

Source context 11 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
open CategoryTheory.MorphismProperty
open AlgebraicGeometry
open scoped TensorProduct
noncomputable section
universe u u₁ u₂ v₁ v₂ w
namespace SchemeTheory.Affine
local instance : HasAffineProperty (affineHomProperty : MorphismProperty Scheme.{u})
    (affineAnd (@allRingHom.{u})) :=
  (HasAffineProperty.affineAnd_iff _ allRingHom_respectsIso
    allRingHom_localizationAwayPreserves allRingHom_ofLocalizationSpan).2 (by
      intro X Y f
      simp [affineHomProperty, allRingHom])
section Weil
variable {R A B : Type u} [CommRing R] [CommRing A] [CommRing B]
  [Algebra R A] [Algebra R B] [Module.Free R A] [Module.Finite R A]
  [Algebra.FinitePresentation R B]
Lean source · statement
def algebraTargetSource :
    (tensorRightAlg (R := R) (A := A)).PartialLeftAdjointSource
abbrev

algebraRepresenter

L255 ↗
SchemeTheory.Affine.algebraRepresenter
Documentation

The R-algebra corepresenting homomorphisms from B to tensor products with A.

Source context 11 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
open CategoryTheory.MorphismProperty
open AlgebraicGeometry
open scoped TensorProduct
noncomputable section
universe u u₁ u₂ v₁ v₂ w
namespace SchemeTheory.Affine
local instance : HasAffineProperty (affineHomProperty : MorphismProperty Scheme.{u})
    (affineAnd (@allRingHom.{u})) :=
  (HasAffineProperty.affineAnd_iff _ allRingHom_respectsIso
    allRingHom_localizationAwayPreserves allRingHom_ofLocalizationSpan).2 (by
      intro X Y f
      simp [affineHomProperty, allRingHom])
section Weil
variable {R A B : Type u} [CommRing R] [CommRing A] [CommRing B]
  [Algebra R A] [Algebra R B] [Module.Free R A] [Module.Finite R A]
  [Algebra.FinitePresentation R B]
Lean source · statement
abbrev algebraRepresenter : CommAlgCat.{u} R
def

algebraCorepresentableBy

L261 ↗
SchemeTheory.Affine.algebraCorepresentableBy
Documentation

The partial left adjoint to tensoring with A corepresents the algebra-homomorphism functor for B.

Source context 11 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
open CategoryTheory.MorphismProperty
open AlgebraicGeometry
open scoped TensorProduct
noncomputable section
universe u u₁ u₂ v₁ v₂ w
namespace SchemeTheory.Affine
local instance : HasAffineProperty (affineHomProperty : MorphismProperty Scheme.{u})
    (affineAnd (@allRingHom.{u})) :=
  (HasAffineProperty.affineAnd_iff _ allRingHom_respectsIso
    allRingHom_localizationAwayPreserves allRingHom_ofLocalizationSpan).2 (by
      intro X Y f
      simp [affineHomProperty, allRingHom])
section Weil
variable {R A B : Type u} [CommRing R] [CommRing A] [CommRing B]
  [Algebra R A] [Algebra R B] [Module.Free R A] [Module.Finite R A]
  [Algebra.FinitePresentation R B]
Lean source · statement
def algebraCorepresentableBy :
    (algebraHomFunctor (R := R) (A := A) (B := B)).CorepresentableBy
      (algebraRepresenter (R := R) (A := A) (B := B))
abbrev

affineTransportedFunctor

L271 ↗
SchemeTheory.Affine.affineTransportedFunctor
Documentation

The algebra-homomorphism functor for B and tensoring with A, viewed on affine test schemes over Spec R.

Source context 11 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
open CategoryTheory.MorphismProperty
open AlgebraicGeometry
open scoped TensorProduct
noncomputable section
universe u u₁ u₂ v₁ v₂ w
namespace SchemeTheory.Affine
local instance : HasAffineProperty (affineHomProperty : MorphismProperty Scheme.{u})
    (affineAnd (@allRingHom.{u})) :=
  (HasAffineProperty.affineAnd_iff _ allRingHom_respectsIso
    allRingHom_localizationAwayPreserves allRingHom_ofLocalizationSpan).2 (by
      intro X Y f
      simp [affineHomProperty, allRingHom])
section Weil
variable {R A B : Type u} [CommRing R] [CommRing A] [CommRing B]
  [Algebra R A] [Algebra R B] [Module.Free R A] [Module.Finite R A]
  [Algebra.FinitePresentation R B]
Lean source · statement
abbrev affineTransportedFunctor :
    (affineHomProperty.Over ⊤ (Spec (CommRingCat.of R)))ᵒᵖ ⥤ Type u
abbrev

affineTransportedRepresenter

L277 ↗
SchemeTheory.Affine.affineTransportedRepresenter
Documentation

The affine scheme over Spec R corresponding to the algebraic corepresenter.

Source context 11 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
open CategoryTheory.MorphismProperty
open AlgebraicGeometry
open scoped TensorProduct
noncomputable section
universe u u₁ u₂ v₁ v₂ w
namespace SchemeTheory.Affine
local instance : HasAffineProperty (affineHomProperty : MorphismProperty Scheme.{u})
    (affineAnd (@allRingHom.{u})) :=
  (HasAffineProperty.affineAnd_iff _ allRingHom_respectsIso
    allRingHom_localizationAwayPreserves allRingHom_ofLocalizationSpan).2 (by
      intro X Y f
      simp [affineHomProperty, allRingHom])
section Weil
variable {R A B : Type u} [CommRing R] [CommRing A] [CommRing B]
  [Algebra R A] [Algebra R B] [Module.Free R A] [Module.Finite R A]
  [Algebra.FinitePresentation R B]
Lean source · statement
abbrev affineTransportedRepresenter :
    affineHomProperty.Over ⊤ (Spec (CommRingCat.of R))
def

affineTransportedRepresentable

L284 ↗
SchemeTheory.Affine.affineTransportedRepresentable
Documentation

The affine scheme obtained from the algebraic corepresenter represents the transported affine functor.

Source context 11 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
open CategoryTheory.MorphismProperty
open AlgebraicGeometry
open scoped TensorProduct
noncomputable section
universe u u₁ u₂ v₁ v₂ w
namespace SchemeTheory.Affine
local instance : HasAffineProperty (affineHomProperty : MorphismProperty Scheme.{u})
    (affineAnd (@allRingHom.{u})) :=
  (HasAffineProperty.affineAnd_iff _ allRingHom_respectsIso
    allRingHom_localizationAwayPreserves allRingHom_ofLocalizationSpan).2 (by
      intro X Y f
      simp [affineHomProperty, allRingHom])
section Weil
variable {R A B : Type u} [CommRing R] [CommRing A] [CommRing B]
  [Algebra R A] [Algebra R B] [Module.Free R A] [Module.Finite R A]
  [Algebra.FinitePresentation R B]
Lean source · statement
def affineTransportedRepresentable :
    (affineTransportedFunctor (R := R) (A := A) (B := B)).RepresentableBy
      (affineTransportedRepresenter (R := R) (A := A) (B := B))
abbrev

specAOver

L292 ↗
SchemeTheory.Affine.specAOver
Documentation

Spec A with its structural morphism to Spec R.

Source context 11 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
open CategoryTheory.MorphismProperty
open AlgebraicGeometry
open scoped TensorProduct
noncomputable section
universe u u₁ u₂ v₁ v₂ w
namespace SchemeTheory.Affine
local instance : HasAffineProperty (affineHomProperty : MorphismProperty Scheme.{u})
    (affineAnd (@allRingHom.{u})) :=
  (HasAffineProperty.affineAnd_iff _ allRingHom_respectsIso
    allRingHom_localizationAwayPreserves allRingHom_ofLocalizationSpan).2 (by
      intro X Y f
      simp [affineHomProperty, allRingHom])
section Weil
variable {R A B : Type u} [CommRing R] [CommRing A] [CommRing B]
  [Algebra R A] [Algebra R B] [Module.Free R A] [Module.Finite R A]
  [Algebra.FinitePresentation R B]
Lean source · statement
abbrev specAOver :
    Over (Spec (CommRingCat.of R))
abbrev

specBOver

L298 ↗
SchemeTheory.Affine.specBOver
Documentation

Spec B with its structural morphism to Spec R.

Source context 11 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
open CategoryTheory.MorphismProperty
open AlgebraicGeometry
open scoped TensorProduct
noncomputable section
universe u u₁ u₂ v₁ v₂ w
namespace SchemeTheory.Affine
local instance : HasAffineProperty (affineHomProperty : MorphismProperty Scheme.{u})
    (affineAnd (@allRingHom.{u})) :=
  (HasAffineProperty.affineAnd_iff _ allRingHom_respectsIso
    allRingHom_localizationAwayPreserves allRingHom_ofLocalizationSpan).2 (by
      intro X Y f
      simp [affineHomProperty, allRingHom])
section Weil
variable {R A B : Type u} [CommRing R] [CommRing A] [CommRing B]
  [Algebra R A] [Algebra R B] [Module.Free R A] [Module.Finite R A]
  [Algebra.FinitePresentation R B]
Lean source · statement
abbrev specBOver :
    Over (Spec (CommRingCat.of R))
abbrev

affineActualProductFunctor

L304 ↗
SchemeTheory.Affine.affineActualProductFunctor
Documentation

The functor taking the fibre product of an affine test scheme with Spec A over Spec R.

Source context 11 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
open CategoryTheory.MorphismProperty
open AlgebraicGeometry
open scoped TensorProduct
noncomputable section
universe u u₁ u₂ v₁ v₂ w
namespace SchemeTheory.Affine
local instance : HasAffineProperty (affineHomProperty : MorphismProperty Scheme.{u})
    (affineAnd (@allRingHom.{u})) :=
  (HasAffineProperty.affineAnd_iff _ allRingHom_respectsIso
    allRingHom_localizationAwayPreserves allRingHom_ofLocalizationSpan).2 (by
      intro X Y f
      simp [affineHomProperty, allRingHom])
section Weil
variable {R A B : Type u} [CommRing R] [CommRing A] [CommRing B]
  [Algebra R A] [Algebra R B] [Module.Free R A] [Module.Finite R A]
  [Algebra.FinitePresentation R B]
Lean source · statement
abbrev affineActualProductFunctor :
    affineHomProperty.Over ⊤ (Spec (CommRingCat.of R)) ⥤
      Over (Spec (CommRingCat.of R))
abbrev

affineTensorSpecFunctor

L312 ↗
SchemeTheory.Affine.affineTensorSpecFunctor
Documentation

The functor taking the spectrum of the global-sections R-algebra of an affine test scheme tensored with A.

Source context 11 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
open CategoryTheory.MorphismProperty
open AlgebraicGeometry
open scoped TensorProduct
noncomputable section
universe u u₁ u₂ v₁ v₂ w
namespace SchemeTheory.Affine
local instance : HasAffineProperty (affineHomProperty : MorphismProperty Scheme.{u})
    (affineAnd (@allRingHom.{u})) :=
  (HasAffineProperty.affineAnd_iff _ allRingHom_respectsIso
    allRingHom_localizationAwayPreserves allRingHom_ofLocalizationSpan).2 (by
      intro X Y f
      simp [affineHomProperty, allRingHom])
section Weil
variable {R A B : Type u} [CommRing R] [CommRing A] [CommRing B]
  [Algebra R A] [Algebra R B] [Module.Free R A] [Module.Finite R A]
  [Algebra.FinitePresentation R B]
Lean source · statement
abbrev affineTensorSpecFunctor :
    affineHomProperty.Over ⊤ (Spec (CommRingCat.of R)) ⥤
      Over (Spec (CommRingCat.of R))
def

affineProductSpecIso

L321 ↗
SchemeTheory.Affine.affineProductSpecIso
Documentation

The fibre product of an affine test scheme with Spec A is naturally isomorphic to the spectrum of its global sections tensored with A.

Source context 11 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
open CategoryTheory.MorphismProperty
open AlgebraicGeometry
open scoped TensorProduct
noncomputable section
universe u u₁ u₂ v₁ v₂ w
namespace SchemeTheory.Affine
local instance : HasAffineProperty (affineHomProperty : MorphismProperty Scheme.{u})
    (affineAnd (@allRingHom.{u})) :=
  (HasAffineProperty.affineAnd_iff _ allRingHom_respectsIso
    allRingHom_localizationAwayPreserves allRingHom_ofLocalizationSpan).2 (by
      intro X Y f
      simp [affineHomProperty, allRingHom])
section Weil
variable {R A B : Type u} [CommRing R] [CommRing A] [CommRing B]
  [Algebra R A] [Algebra R B] [Module.Free R A] [Module.Finite R A]
  [Algebra.FinitePresentation R B]
Lean source · statement
def affineProductSpecIso :
    affineActualProductFunctor (R := R) (A := A) ≅
      affineTensorSpecFunctor (R := R) (A := A)
abbrev

affineInternalHomFunctor

L344 ↗
SchemeTheory.Affine.affineInternalHomFunctor
Documentation

The geometric affine internal Hom functor over Spec R.

On an affine T over Spec R, this is the set of morphisms over Spec R from T x_{Spec R} Spec A to Spec B.

Source context 11 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
open CategoryTheory.MorphismProperty
open AlgebraicGeometry
open scoped TensorProduct
noncomputable section
universe u u₁ u₂ v₁ v₂ w
namespace SchemeTheory.Affine
local instance : HasAffineProperty (affineHomProperty : MorphismProperty Scheme.{u})
    (affineAnd (@allRingHom.{u})) :=
  (HasAffineProperty.affineAnd_iff _ allRingHom_respectsIso
    allRingHom_localizationAwayPreserves allRingHom_ofLocalizationSpan).2 (by
      intro X Y f
      simp [affineHomProperty, allRingHom])
section Weil
variable {R A B : Type u} [CommRing R] [CommRing A] [CommRing B]
  [Algebra R A] [Algebra R B] [Module.Free R A] [Module.Finite R A]
  [Algebra.FinitePresentation R B]
Lean source · statement
abbrev affineInternalHomFunctor :
    (affineHomProperty.Over ⊤ (Spec (CommRingCat.of R)))ᵒᵖ ⥤ Type u
abbrev

affineInternalHomRepresenter

L350 ↗
SchemeTheory.Affine.affineInternalHomRepresenter
Documentation

The affine scheme over Spec R representing affineInternalHomFunctor.

Source context 11 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
open CategoryTheory.MorphismProperty
open AlgebraicGeometry
open scoped TensorProduct
noncomputable section
universe u u₁ u₂ v₁ v₂ w
namespace SchemeTheory.Affine
local instance : HasAffineProperty (affineHomProperty : MorphismProperty Scheme.{u})
    (affineAnd (@allRingHom.{u})) :=
  (HasAffineProperty.affineAnd_iff _ allRingHom_respectsIso
    allRingHom_localizationAwayPreserves allRingHom_ofLocalizationSpan).2 (by
      intro X Y f
      simp [affineHomProperty, allRingHom])
section Weil
variable {R A B : Type u} [CommRing R] [CommRing A] [CommRing B]
  [Algebra R A] [Algebra R B] [Module.Free R A] [Module.Finite R A]
  [Algebra.FinitePresentation R B]
Lean source · statement
abbrev affineInternalHomRepresenter :
    affineHomProperty.Over ⊤ (Spec (CommRingCat.of R))
def

transportedGeometricEquiv

L356 ↗
SchemeTheory.Affine.transportedGeometricEquiv
Documentation

For an affine test scheme T, algebra homomorphisms from B to its global sections tensored with A correspond to morphisms from T fibre-product Spec A to Spec B over Spec R.

Source context 11 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
open CategoryTheory.MorphismProperty
open AlgebraicGeometry
open scoped TensorProduct
noncomputable section
universe u u₁ u₂ v₁ v₂ w
namespace SchemeTheory.Affine
local instance : HasAffineProperty (affineHomProperty : MorphismProperty Scheme.{u})
    (affineAnd (@allRingHom.{u})) :=
  (HasAffineProperty.affineAnd_iff _ allRingHom_respectsIso
    allRingHom_localizationAwayPreserves allRingHom_ofLocalizationSpan).2 (by
      intro X Y f
      simp [affineHomProperty, allRingHom])
section Weil
variable {R A B : Type u} [CommRing R] [CommRing A] [CommRing B]
  [Algebra R A] [Algebra R B] [Module.Free R A] [Module.Finite R A]
  [Algebra.FinitePresentation R B]
Lean source · statement
def transportedGeometricEquiv
    (T : (affineHomProperty.Over ⊤ (Spec (CommRingCat.of R)))ᵒᵖ) :
    (affineTransportedFunctor (R := R) (A := A) (B := B)).obj T ≃
      (affineInternalHomFunctor (R := R) (A := A) (B := B)).obj T
lemma

transportedGeometricEquiv_apply

L384 ↗
SchemeTheory.Affine.transportedGeometricEquiv_apply
Source context 12 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
open CategoryTheory.MorphismProperty
open AlgebraicGeometry
open scoped TensorProduct
noncomputable section
universe u u₁ u₂ v₁ v₂ w
namespace SchemeTheory.Affine
local instance : HasAffineProperty (affineHomProperty : MorphismProperty Scheme.{u})
    (affineAnd (@allRingHom.{u})) :=
  (HasAffineProperty.affineAnd_iff _ allRingHom_respectsIso
    allRingHom_localizationAwayPreserves allRingHom_ofLocalizationSpan).2 (by
      intro X Y f
      simp [affineHomProperty, allRingHom])
section Weil
variable {R A B : Type u} [CommRing R] [CommRing A] [CommRing B]
  [Algebra R A] [Algebra R B] [Module.Free R A] [Module.Finite R A]
  [Algebra.FinitePresentation R B]
omit [Module.Free R A] [Module.Finite R A] [Algebra.FinitePresentation R B] in
Lean source · statement
lemma transportedGeometricEquiv_apply
    (T : (affineHomProperty.Over ⊤ (Spec (CommRingCat.of R)))ᵒᵖ)
    (g : (affineTransportedFunctor (R := R) (A := A) (B := B)).obj T) :
    transportedGeometricEquiv (R := R) (A := A) (B := B) T g =
      (affineProductSpecIso (R := R) (A := A)).hom.app T.unop ≫
        (specOverFunctor (CommRingCat.of R)).map g.op
lemma

affineTransportedFunctor_map_apply

L392 ↗
SchemeTheory.Affine.affineTransportedFunctor_map_apply
Source context 12 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
open CategoryTheory.MorphismProperty
open AlgebraicGeometry
open scoped TensorProduct
noncomputable section
universe u u₁ u₂ v₁ v₂ w
namespace SchemeTheory.Affine
local instance : HasAffineProperty (affineHomProperty : MorphismProperty Scheme.{u})
    (affineAnd (@allRingHom.{u})) :=
  (HasAffineProperty.affineAnd_iff _ allRingHom_respectsIso
    allRingHom_localizationAwayPreserves allRingHom_ofLocalizationSpan).2 (by
      intro X Y f
      simp [affineHomProperty, allRingHom])
section Weil
variable {R A B : Type u} [CommRing R] [CommRing A] [CommRing B]
  [Algebra R A] [Algebra R B] [Module.Free R A] [Module.Finite R A]
  [Algebra.FinitePresentation R B]
omit [Module.Free R A] [Module.Finite R A] [Algebra.FinitePresentation R B] in
Lean source · statement
lemma affineTransportedFunctor_map_apply
    {T U : (affineHomProperty.Over ⊤ (Spec (CommRingCat.of R)))ᵒᵖ}
    (f : T ⟶ U)
    (g : (affineTransportedFunctor (R := R) (A := A) (B := B)).obj T) :
    (affineTransportedFunctor (R := R) (A := A) (B := B)).map f g =
      g ≫ (tensorRightAlg (R := R) (A := A)).map
        ((affineAlgebraEquiv (CommRingCat.of R)).functor.map f)
lemma

affineInternalHomFunctor_map_apply

L401 ↗
SchemeTheory.Affine.affineInternalHomFunctor_map_apply
Source context 12 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
open CategoryTheory.MorphismProperty
open AlgebraicGeometry
open scoped TensorProduct
noncomputable section
universe u u₁ u₂ v₁ v₂ w
namespace SchemeTheory.Affine
local instance : HasAffineProperty (affineHomProperty : MorphismProperty Scheme.{u})
    (affineAnd (@allRingHom.{u})) :=
  (HasAffineProperty.affineAnd_iff _ allRingHom_respectsIso
    allRingHom_localizationAwayPreserves allRingHom_ofLocalizationSpan).2 (by
      intro X Y f
      simp [affineHomProperty, allRingHom])
section Weil
variable {R A B : Type u} [CommRing R] [CommRing A] [CommRing B]
  [Algebra R A] [Algebra R B] [Module.Free R A] [Module.Finite R A]
  [Algebra.FinitePresentation R B]
omit [Module.Free R A] [Module.Finite R A] [Algebra.FinitePresentation R B] in
Lean source · statement
lemma affineInternalHomFunctor_map_apply
    {T U : (affineHomProperty.Over ⊤ (Spec (CommRingCat.of R)))ᵒᵖ}
    (f : T ⟶ U)
    (g : (affineInternalHomFunctor (R := R) (A := A) (B := B)).obj T) :
    (affineInternalHomFunctor (R := R) (A := A) (B := B)).map f g =
      (affineActualProductFunctor (R := R) (A := A)).map f.unop ≫ g
def

affineTransportedGeometricIso

L409 ↗
SchemeTheory.Affine.affineTransportedGeometricIso
Documentation

The algebraic and geometric affine internal-Hom functors are naturally isomorphic.

Source context 11 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
open CategoryTheory.MorphismProperty
open AlgebraicGeometry
open scoped TensorProduct
noncomputable section
universe u u₁ u₂ v₁ v₂ w
namespace SchemeTheory.Affine
local instance : HasAffineProperty (affineHomProperty : MorphismProperty Scheme.{u})
    (affineAnd (@allRingHom.{u})) :=
  (HasAffineProperty.affineAnd_iff _ allRingHom_respectsIso
    allRingHom_localizationAwayPreserves allRingHom_ofLocalizationSpan).2 (by
      intro X Y f
      simp [affineHomProperty, allRingHom])
section Weil
variable {R A B : Type u} [CommRing R] [CommRing A] [CommRing B]
  [Algebra R A] [Algebra R B] [Module.Free R A] [Module.Finite R A]
  [Algebra.FinitePresentation R B]
Lean source · statement
def affineTransportedGeometricIso :
    affineTransportedFunctor (R := R) (A := A) (B := B) ≅
      affineInternalHomFunctor (R := R) (A := A) (B := B)
def

affineInternalHomRepresentable

L443 ↗
SchemeTheory.Affine.affineInternalHomRepresentable
Documentation

The affine internal Hom functor is represented by the affine scheme associated to CommAlgCat.affineWeilRestriction.

Source context 11 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
open CategoryTheory.MorphismProperty
open AlgebraicGeometry
open scoped TensorProduct
noncomputable section
universe u u₁ u₂ v₁ v₂ w
namespace SchemeTheory.Affine
local instance : HasAffineProperty (affineHomProperty : MorphismProperty Scheme.{u})
    (affineAnd (@allRingHom.{u})) :=
  (HasAffineProperty.affineAnd_iff _ allRingHom_respectsIso
    allRingHom_localizationAwayPreserves allRingHom_ofLocalizationSpan).2 (by
      intro X Y f
      simp [affineHomProperty, allRingHom])
section Weil
variable {R A B : Type u} [CommRing R] [CommRing A] [CommRing B]
  [Algebra R A] [Algebra R B] [Module.Free R A] [Module.Finite R A]
  [Algebra.FinitePresentation R B]
Lean source · statement
def affineInternalHomRepresentable :
    (affineInternalHomFunctor (R := R) (A := A) (B := B)).RepresentableBy
      (affineInternalHomRepresenter (R := R) (A := A) (B := B))

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