Documentation

TauCeti.AlgebraicGeometry.VectorBundle.Determinant.Pullback

Pullback of the determinant of a vector bundle #

Let f : X ⟶ Y be a morphism of schemes and E a finite locally free sheaf of constant rank r on Y. Since E is quasicoherent, the canonical exterior-power comparison f^* (⋀ʳ E) ⟶ ⋀ʳ (f^* E) is an isomorphism (TauCeti.AlgebraicGeometry.isIso_pullbackExteriorPowerComparison_app). It therefore gives an isomorphism of invertible sheaves f^* (det E) ≅ det (f^* E), natural in E.

These comparisons are coherent: along the identity the comparison is induced by the identity isomorphism of pullback, and along a composite f ≫ g it is the composite of the comparisons along g and f, through the composition isomorphisms of pullback of invertible sheaves and of fixed-rank sheaves.

Without a constant rank, the determinant det E = ⋀^{rank E} E is the exterior power in the locally constant degree rank E. Its pullback is compared with det (f^* E) through the exterior-power comparison f^* (⋀^{rank E} E) ⟶ ⋀^{rank E ∘ f} (f^* E), again an isomorphism since E is quasicoherent (TauCeti.AlgebraicGeometry.isIso_pullbackLocallyConstantExteriorPowerComparison_app), and the identification rank (f^* E) = rank E ∘ f (FiniteLocallyFreeSheaf.rank_pullback).

Main declarations #

References #

source
noncomputable def TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.pullbackDeterminantIso {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (r : ℕ) :
(determinant Y r).comp (InvertibleSheaf.pullback f) ≅ (FixedRank.pullback f).comp (determinant X r)

Pulling back the determinant of a finite locally free sheaf of constant rank r is naturally isomorphic to taking the determinant of its pullback: f^* (det E) ≅ det (f^* E). The forward map is the canonical exterior-power comparison f^* (⋀ʳ E) ⟶ ⋀ʳ (f^* E), which is invertible because E is quasicoherent.

Instances For
    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.pullbackDeterminantIso_hom_app_hom {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {r : ℕ} (E : FixedRank Y r) :
    ((pullbackDeterminantIso f r).hom.app E).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullbackExteriorPowerComparison f r).app E.obj.obj) (CategoryTheory.eqToHom ⋯))

    On underlying sheaves, the forward map of pullbackDeterminantIso is the canonical exterior-power comparison f^* (⋀ʳ E) ⟶ ⋀ʳ (f^* E).

    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.pullbackDeterminantIso_inv_app_hom {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {r : ℕ} (E : FixedRank Y r) :
    ((pullbackDeterminantIso f r).inv.app E).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv ((AlgebraicGeometry.Scheme.Modules.pullbackExteriorPowerComparison f r).app E.obj.obj)) (CategoryTheory.eqToHom ⋯))

    On underlying sheaves, the inverse map of pullbackDeterminantIso is the inverse of the canonical exterior-power comparison f^* (⋀ʳ E) ⟶ ⋀ʳ (f^* E).

    source
    theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.pullbackDeterminantIso_hom_app_id {X : AlgebraicGeometry.Scheme} {r : ℕ} (E : FixedRank X r) :
    CategoryTheory.CategoryStruct.comp ((pullbackDeterminantIso (CategoryTheory.CategoryStruct.id X) r).hom.app E) ((determinant X r).map ((FixedRank.pullbackId X r).hom.app E)) = (InvertibleSheaf.pullbackId X).hom.app ((determinant X r).obj E)

    The determinant pullback comparison along the identity is induced by the identity isomorphisms of pullback of fixed-rank sheaves and of invertible sheaves.

    source
    theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.pullbackDeterminantIso_hom_app_id_assoc {X : AlgebraicGeometry.Scheme} {r : ℕ} (E : FixedRank X r) {Z : InvertibleSheaf X} (h : (determinant X r).obj E ⟶ Z) :
    CategoryTheory.CategoryStruct.comp ((pullbackDeterminantIso (CategoryTheory.CategoryStruct.id X) r).hom.app E) (CategoryTheory.CategoryStruct.comp ((determinant X r).map ((FixedRank.pullbackId X r).hom.app E)) h) = CategoryTheory.CategoryStruct.comp ((InvertibleSheaf.pullbackId X).hom.app ((determinant X r).obj E)) h

    The determinant pullback comparison along the identity is induced by the identity isomorphisms of pullback of fixed-rank sheaves and of invertible sheaves.

    source
    theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.pullbackDeterminantIso_hom_app_comp {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) {r : ℕ} (E : FixedRank Z r) :
    CategoryTheory.CategoryStruct.comp ((pullbackDeterminantIso (CategoryTheory.CategoryStruct.comp f g) r).hom.app E) ((determinant X r).map ((FixedRank.pullbackComp f g).inv.app E)) = CategoryTheory.CategoryStruct.comp ((InvertibleSheaf.pullbackComp f g).inv.app ((determinant Z r).obj E)) (CategoryTheory.CategoryStruct.comp ((InvertibleSheaf.pullback f).map ((pullbackDeterminantIso g r).hom.app E)) ((pullbackDeterminantIso f r).hom.app ((FixedRank.pullback g).obj E)))

    The determinant pullback comparison along a composite f ≫ g is the composite of the comparisons along g and along f, through the composition isomorphisms of pullback of fixed-rank sheaves and of invertible sheaves.

    source
    theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.pullbackDeterminantIso_hom_app_comp_assoc {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) {r : ℕ} (E : FixedRank Z r) {Z✝ : InvertibleSheaf X} (h : (determinant X r).obj ((FixedRank.pullback f).obj ((FixedRank.pullback g).obj E)) ⟶ Z✝) :
    CategoryTheory.CategoryStruct.comp ((pullbackDeterminantIso (CategoryTheory.CategoryStruct.comp f g) r).hom.app E) (CategoryTheory.CategoryStruct.comp ((determinant X r).map ((FixedRank.pullbackComp f g).inv.app E)) h) = CategoryTheory.CategoryStruct.comp ((InvertibleSheaf.pullbackComp f g).inv.app ((determinant Z r).obj E)) (CategoryTheory.CategoryStruct.comp ((InvertibleSheaf.pullback f).map ((pullbackDeterminantIso g r).hom.app E)) (CategoryTheory.CategoryStruct.comp ((pullbackDeterminantIso f r).hom.app ((FixedRank.pullback g).obj E)) h))

    The determinant pullback comparison along a composite f ≫ g is the composite of the comparisons along g and along f, through the composition isomorphisms of pullback of fixed-rank sheaves and of invertible sheaves.

    source
    noncomputable def TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.pullbackDetIso {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (E : FiniteLocallyFreeSheaf Y) :
    (InvertibleSheaf.pullback f).obj E.det ≅ ((pullback f).obj E).det

    Pullback of the determinant in locally constant rank. For a morphism of schemes f : X ⟶ Y and a finite locally free sheaf E on Y, the pullback of det E = ⋀^{rank E} E is the determinant of f^* E. The forward map is the exterior-power comparison f^* (⋀^{rank E} E) ⟶ ⋀^{rank E ∘ f} (f^* E), an isomorphism because E is quasicoherent, followed by the identification rank (f^* E) = rank E ∘ f.

    Instances For
      source
      @[simp]
      theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.pullbackDetIso_hom_hom {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (E : FiniteLocallyFreeSheaf Y) :
      (pullbackDetIso f E).hom.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((pullbackLocallyConstantExteriorPowerComparison f E.rank).app E.obj) (CategoryTheory.eqToHom ⋯))

      On underlying sheaves, the forward map of pullbackDetIso is the exterior-power comparison f^* (⋀^{rank E} E) ⟶ ⋀^{rank E ∘ f} (f^* E), followed by the identification rank (f^* E) = rank E ∘ f.

      source
      @[simp]
      theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.pullbackDetIso_inv_hom {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (E : FiniteLocallyFreeSheaf Y) :
      (pullbackDetIso f E).inv.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv ((pullbackLocallyConstantExteriorPowerComparison f E.rank).app E.obj)) (CategoryTheory.eqToHom ⋯))

      On underlying sheaves, the inverse map of pullbackDetIso is the inverse of the exterior-power comparison f^* (⋀^{rank E} E) ⟶ ⋀^{rank E ∘ f} (f^* E), preceded by the identification rank (f^* E) = rank E ∘ f.