Documentation

TauCeti.AlgebraicGeometry.VectorBundle.Functoriality

Functorial pullback of finite locally free sheaves #

Pulling back a finite locally free sheaf along the identity is naturally isomorphic to the original sheaf. Pullback along a composite is naturally isomorphic to successive pullback. These comparisons are the restrictions of the corresponding comparisons for all modules on a scheme. They are comparison data needed for base-change naturality of the vector-bundle equivalence.

The construction follows the full-subcategory comparisons for invertible sheaves in TauCeti/AlgebraicGeometry/LineBundle/Functoriality.lean; finite local freeness replaces invertibility throughout.

source
noncomputable def TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.pullbackId (X : AlgebraicGeometry.Scheme) :
pullback (CategoryTheory.CategoryStruct.id X) ≅ CategoryTheory.Functor.id (FiniteLocallyFreeSheaf X)

Pullback along the identity is naturally isomorphic to the identity functor on finite locally free sheaves.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.pullbackId_app_hom_hom (X : AlgebraicGeometry.Scheme) (E : FiniteLocallyFreeSheaf X) :
    ((pullbackId X).hom.app E).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) ((AlgebraicGeometry.Scheme.Modules.pullbackId X).hom.app E.obj)

    On underlying modules, the identity comparison is Mathlib's pullback identity comparison.

    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.pullbackId_inv_app_hom (X : AlgebraicGeometry.Scheme) (E : FiniteLocallyFreeSheaf X) :
    ((pullbackId X).inv.app E).hom = CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullbackId X).inv.app E.obj) (CategoryTheory.eqToHom ⋯)

    The inverse identity comparison on underlying modules is Mathlib's inverse comparison.

    source
    noncomputable def TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.pullbackComp {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) :
    (pullback g).comp (pullback f) ≅ pullback (CategoryTheory.CategoryStruct.comp f g)

    Pullback along a composite is naturally isomorphic to successive pullback of finite locally free sheaves.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.pullbackComp_app_hom_hom {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (E : FiniteLocallyFreeSheaf Z) :
      ((pullbackComp f g).hom.app E).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullbackComp f g).hom.app E.obj) (CategoryTheory.eqToHom ⋯))

      On underlying modules, the composition comparison is Mathlib's pullback composition comparison.

      source
      @[simp]
      theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.pullbackComp_inv_app_hom {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (E : FiniteLocallyFreeSheaf Z) :
      ((pullbackComp f g).inv.app E).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullbackComp f g).inv.app E.obj) (CategoryTheory.eqToHom ⋯))

      The inverse composition comparison on underlying modules is Mathlib's inverse comparison.