Documentation

TauCeti.AlgebraicGeometry.BaseChangeSection

Base change of a section of a scheme morphism #

A section of f : X ⟶ S induces a section on each base change T ×_S X. The projection formulas and naturality in T follow from pullback of split epimorphisms and symmetry of pullbacks.

source
noncomputable def TauCeti.AlgebraicGeometry.baseChangeSection {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) (x₀ : S ⟶ X) (hx₀ : CategoryTheory.CategoryStruct.comp x₀ f = CategoryTheory.CategoryStruct.id S) (T : CategoryTheory.Over S) :
T.left ⟶ CategoryTheory.Limits.pullback T.hom f

The base change x₀_T : T ⟶ T ×_S X of a section x₀ of f : X ⟶ S to a scheme T over S.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.baseChangeSection_fst {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) (x₀ : S ⟶ X) (hx₀ : CategoryTheory.CategoryStruct.comp x₀ f = CategoryTheory.CategoryStruct.id S) (T : CategoryTheory.Over S) :
    CategoryTheory.CategoryStruct.comp (baseChangeSection f x₀ hx₀ T) (CategoryTheory.Limits.pullback.fst T.hom f) = CategoryTheory.CategoryStruct.id T.left

    The base-changed section is a section of the projection T ×_S X ⟶ T.

    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.baseChangeSection_fst_assoc {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) (x₀ : S ⟶ X) (hx₀ : CategoryTheory.CategoryStruct.comp x₀ f = CategoryTheory.CategoryStruct.id S) (T : CategoryTheory.Over S) {Z : AlgebraicGeometry.Scheme} (h : T.left ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (baseChangeSection f x₀ hx₀ T) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst T.hom f) h) = h

    The base-changed section is a section of the projection T ×_S X ⟶ T.

    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.baseChangeSection_snd {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) (x₀ : S ⟶ X) (hx₀ : CategoryTheory.CategoryStruct.comp x₀ f = CategoryTheory.CategoryStruct.id S) (T : CategoryTheory.Over S) :
    CategoryTheory.CategoryStruct.comp (baseChangeSection f x₀ hx₀ T) (CategoryTheory.Limits.pullback.snd T.hom f) = CategoryTheory.CategoryStruct.comp T.hom x₀

    The base-changed section followed by the projection to X is T ⟶ S ⟶ X.

    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.baseChangeSection_snd_assoc {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) (x₀ : S ⟶ X) (hx₀ : CategoryTheory.CategoryStruct.comp x₀ f = CategoryTheory.CategoryStruct.id S) (T : CategoryTheory.Over S) {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (baseChangeSection f x₀ hx₀ T) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd T.hom f) h) = CategoryTheory.CategoryStruct.comp T.hom (CategoryTheory.CategoryStruct.comp x₀ h)

    The base-changed section followed by the projection to X is T ⟶ S ⟶ X.

    source
    theorem TauCeti.AlgebraicGeometry.baseChangeSection_comp_pullback_map {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) (x₀ : S ⟶ X) (hx₀ : CategoryTheory.CategoryStruct.comp x₀ f = CategoryTheory.CategoryStruct.id S) {T' T : CategoryTheory.Over S} (φ : T' ⟶ T) :
    CategoryTheory.CategoryStruct.comp (baseChangeSection f x₀ hx₀ T') (CategoryTheory.Over.Hom.left ((CategoryTheory.Over.pullback f).map φ)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left φ) (baseChangeSection f x₀ hx₀ T)

    The base-changed sections are compatible with the morphisms T' ×_S X ⟶ T ×_S X induced by morphisms T' ⟶ T over S.

    source
    theorem TauCeti.AlgebraicGeometry.baseChangeSection_comp_pullback_map_assoc {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) (x₀ : S ⟶ X) (hx₀ : CategoryTheory.CategoryStruct.comp x₀ f = CategoryTheory.CategoryStruct.id S) {T' T : CategoryTheory.Over S} (φ : T' ⟶ T) {Z : AlgebraicGeometry.Scheme} (h : ((CategoryTheory.Over.pullback f).obj T).left ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (baseChangeSection f x₀ hx₀ T') (CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left ((CategoryTheory.Over.pullback f).map φ)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left φ) (CategoryTheory.CategoryStruct.comp (baseChangeSection f x₀ hx₀ T) h)

    The base-changed sections are compatible with the morphisms T' ×_S X ⟶ T ×_S X induced by morphisms T' ⟶ T over S.