Algebraic vector bundles

The declarations the status of Tau Ceti's roadmap names as Tau Ceti has them at commit ace60277.

DefinitionTauCeti.AlgebraicGeometry.relativeSpecEquiv#

Relative Spec and the algebra of regular functions give an anti-equivalence between quasi-coherent commutative algebras and affine schemes over an arbitrary base scheme. Its unit and counit are the canonical section and affine-chart comparisons.

TauCeti.AlgebraicGeometry.relativeSpecEquiv.{u} (X : AlgebraicGeometry.Scheme) :
  (TauCeti.AlgebraicGeometry.QuasicoherentAlgebra X)ᵒᵖ ≌
    TauCeti.AlgebraicGeometry.AffineSchemeOver X

Lean

Formalized in Tau Ceti as TauCeti.AlgebraicGeometry.relativeSpecEquiv.

Sources

• Tau Ceti documentation: TauCeti.AlgebraicGeometry.relativeSpecEquiv
• Source of TauCeti.AlgebraicGeometry.relativeSpecEquiv in TauCeti/AlgebraicGeometry/RelativeSpec/Equivalence.lean
• Tau Ceti roadmap status: Algebraic vector bundles

LeanTauCeti.AlgebraicGeometry.relativeSpecEquiv

Used by 1

Used byTauCeti.AlgebraicGeometry.gradedRelativeSpecEquiv

DefinitionRelative Spec commutes with base change, naturally in the algebra#

For f : Y ⟶ X, taking the relative spectrum of the pullback of a quasicoherent algebra is naturally isomorphic to base changing its relative spectrum along f.

TauCeti.AlgebraicGeometry.relativeSpecBaseChangeIso.{u} {X Y : AlgebraicGeometry.Scheme}
  (f : Y ⟶ X) :
  (TauCeti.AlgebraicGeometry.QuasicoherentAlgebra.pullback f).op.comp
      (TauCeti.AlgebraicGeometry.relativeSpec Y) ≅
    (TauCeti.AlgebraicGeometry.relativeSpec X).comp
      (TauCeti.AlgebraicGeometry.baseChangeAffineSchemeOver f)

Lean

Formalized in Tau Ceti as TauCeti.AlgebraicGeometry.relativeSpecBaseChangeIso.

Sources

• Tau Ceti documentation: TauCeti.AlgebraicGeometry.relativeSpecBaseChangeIso
• Source of TauCeti.AlgebraicGeometry.relativeSpecBaseChangeIso in TauCeti/AlgebraicGeometry/RelativeSpec/BaseChange.lean
• Tau Ceti roadmap status: Algebraic vector bundles

LeanTauCeti.AlgebraicGeometry.relativeSpecBaseChangeIso

TheoremRelative Spec commutes with base change, compatibly with composition#

For g : Z ⟶ Y and f : Y ⟶ X, the isomorphism Spec_Z ((g ≫ f)^* A) ≅ Z ×_X Spec_X A is the composite of the identification Spec_Z ((g ≫ f)^* A) ≅ Spec_Z (g^* f^* A), the isomorphisms for g and for f, and the canonical isomorphism Z ×_Y (Y ×_X Spec_X A) ≅ Z ×_X Spec_X A.

TauCeti.AlgebraicGeometry.relativeSpecPullbackIso_comp.{u} {X Y : AlgebraicGeometry.Scheme}
  (A : TauCeti.AlgebraicGeometry.QuasicoherentAlgebra X) (f : Y ⟶ X) {Z : AlgebraicGeometry.Scheme}
  (g : Z ⟶ Y) :
  (TauCeti.AlgebraicGeometry.relativeSpecPullbackIso A
        (CategoryTheory.CategoryStruct.comp g f)).hom =
    CategoryTheory.CategoryStruct.comp
      ((TauCeti.AlgebraicGeometry.relativeSpec Z).map
        ((TauCeti.AlgebraicGeometry.QuasicoherentAlgebra.pullbackComp g f).hom.app A).op)
      (CategoryTheory.CategoryStruct.comp
        (TauCeti.AlgebraicGeometry.relativeSpecPullbackIso
            ((TauCeti.AlgebraicGeometry.QuasicoherentAlgebra.pullback f).obj A) g).hom
        (CategoryTheory.CategoryStruct.comp
          ((TauCeti.AlgebraicGeometry.baseChangeAffineSchemeOver g).map
            (TauCeti.AlgebraicGeometry.relativeSpecPullbackIso A f).hom)
          ((CategoryTheory.MorphismProperty.Over.pullbackComp g f
                  (CategoryTheory.CategoryStruct.comp g f) ⋯).inv.app
            ((TauCeti.AlgebraicGeometry.relativeSpec X).obj (Opposite.op A)))))

Lean

Formalized in Tau Ceti as TauCeti.AlgebraicGeometry.relativeSpecPullbackIso_comp.

Sources

• Tau Ceti documentation: TauCeti.AlgebraicGeometry.relativeSpecPullbackIso_comp
• Source of TauCeti.AlgebraicGeometry.relativeSpecPullbackIso_comp in TauCeti/AlgebraicGeometry/RelativeSpec/BaseChange.lean
• Tau Ceti roadmap status: Algebraic vector bundles

LeanTauCeti.AlgebraicGeometry.relativeSpecPullbackIso_comp

DefinitionSpec_X (Sym F) represents linear functionals#

For a quasicoherent sheaf F on X and a scheme q : T ⟶ X over X, morphisms T ⟶ Spec_X (Sym F) over X correspond to morphisms of 𝒪_T-modules q^* F ⟶ 𝒪_T. It is relativeSpecSymmetricAlgebraHomEquiv followed by the adjunction between pullback and pushforward of modules.

TauCeti.AlgebraicGeometry.relativeSpecSymmetricAlgebraPullbackHomEquiv.{u}
  {X : AlgebraicGeometry.Scheme} (F : TauCeti.AlgebraicGeometry.QuasicoherentSheaf X)
  (T : CategoryTheory.Over X) :
  (T ⟶
      (CategoryTheory.MorphismProperty.Over.forget @AlgebraicGeometry.IsAffineHom ⊤ X).obj
        ((TauCeti.AlgebraicGeometry.relativeSpec X).obj
          (Opposite.op ((TauCeti.AlgebraicGeometry.symmetricAlgebra X).obj F)))) ≃
    ((AlgebraicGeometry.Scheme.Modules.pullback T.hom).obj F.obj ⟶
      CategoryTheory.MonoidalCategoryStruct.tensorUnit T.left.Modules)

Lean

Formalized in Tau Ceti as TauCeti.AlgebraicGeometry.relativeSpecSymmetricAlgebraPullbackHomEquiv.

Sources

• Tau Ceti documentation: TauCeti.AlgebraicGeometry.relativeSpecSymmetricAlgebraPullbackHomEquiv
• Source of TauCeti.AlgebraicGeometry.relativeSpecSymmetricAlgebraPullbackHomEquiv in TauCeti/AlgebraicGeometry/RelativeSpec/SymmetricAlgebra/Basic.lean
• Tau Ceti roadmap status: Algebraic vector bundles

LeanTauCeti.AlgebraicGeometry.relativeSpecSymmetricAlgebraPullbackHomEquiv

TheoremTauCeti.AlgebraicGeometry.QuasicoherentSheaf.nonempty_hasLeftDual_iff_isFiniteLocallyFree#

A quasicoherent sheaf on any scheme has a left dual in QuasicoherentSheaf X if and only if it is finite locally free.

TauCeti.AlgebraicGeometry.QuasicoherentSheaf.nonempty_hasLeftDual_iff_isFiniteLocallyFree.{u}
  {X : AlgebraicGeometry.Scheme} (E : TauCeti.AlgebraicGeometry.QuasicoherentSheaf X) :
  Nonempty (CategoryTheory.HasLeftDual E) ↔
    AlgebraicGeometry.Scheme.Modules.isFiniteLocallyFree X E.obj

Lean

Formalized in Tau Ceti as TauCeti.AlgebraicGeometry.QuasicoherentSheaf.nonempty_hasLeftDual_iff_isFiniteLocallyFree.

Sources

• Tau Ceti documentation: TauCeti.AlgebraicGeometry.QuasicoherentSheaf.nonempty_hasLeftDual_iff_isFiniteLocallyFree
• Source of TauCeti.AlgebraicGeometry.QuasicoherentSheaf.nonempty_hasLeftDual_iff_isFiniteLocallyFree in TauCeti/AlgebraicGeometry/VectorBundle/Dual/Dualizable.lean
• Tau Ceti roadmap status: Algebraic vector bundles

LeanTauCeti.AlgebraicGeometry.QuasicoherentSheaf.nonempty_hasLeftDual_iff_isFiniteLocallyFree

Uses 1

Proof usesTauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf

DefinitionTauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.evalNatIso#

The identity functor on finite locally free sheaves is naturally isomorphic to internal-Hom dualization applied twice.

TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.evalNatIso.{u} {X : AlgebraicGeometry.Scheme} :
  CategoryTheory.Functor.id (TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf X) ≅
    TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.dualFunctor.rightOp.comp
      TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.dualFunctor

Lean

Formalized in Tau Ceti as TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.evalNatIso.

Sources

• Tau Ceti documentation: TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.evalNatIso
• Source of TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.evalNatIso in TauCeti/AlgebraicGeometry/VectorBundle/Dual/Bidual.lean
• Tau Ceti roadmap status: Algebraic vector bundles

LeanTauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.evalNatIso

Uses 1

Statement usesTauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf

TheoremSymmetric powers commute with pullback of quasicoherent sheaves#

for every morphism of schemes f : X ⟶ Y and every quasicoherent 𝒪_Y-module M, the canonical comparison f^* (Symⁿ M) ⟶ Symⁿ (f^* M) is an isomorphism.

TauCeti.AlgebraicGeometry.isIso_pullbackSymmetricPowerComparison_app.{u}
  {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (n : ℕ) (M : Y.Modules)
  [SheafOfModules.IsQuasicoherent M] :
  CategoryTheory.IsIso
    ((AlgebraicGeometry.Scheme.Modules.pullbackSymmetricPowerComparison f n).app M)

Lean

Formalized in Tau Ceti as TauCeti.AlgebraicGeometry.isIso_pullbackSymmetricPowerComparison_app.

Sources

• Tau Ceti documentation: TauCeti.AlgebraicGeometry.isIso_pullbackSymmetricPowerComparison_app
• Source of TauCeti.AlgebraicGeometry.isIso_pullbackSymmetricPowerComparison_app in TauCeti/AlgebraicGeometry/Modules/SymmetricPower/Pullback/Quasicoherent.lean
• Tau Ceti roadmap status: Algebraic vector bundles

LeanTauCeti.AlgebraicGeometry.isIso_pullbackSymmetricPowerComparison_app

DefinitionTauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.pullbackDeterminantIso#

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.

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

Lean

Formalized in Tau Ceti as TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.pullbackDeterminantIso.

Sources

• Tau Ceti documentation: TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.pullbackDeterminantIso
• Source of TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.pullbackDeterminantIso in TauCeti/AlgebraicGeometry/VectorBundle/Determinant/Pullback.lean
• Tau Ceti roadmap status: Algebraic vector bundles

LeanTauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.pullbackDeterminantIso

Uses 1

Statement usesTauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf

DefinitionTauCeti.AlgebraicGeometry.gradedSymmetricAlgebraAdjunction#

The graded symmetric algebra functor is left adjoint to the degree-one functor: morphisms of graded quasicoherent algebras Sym F ⟶ A correspond to morphisms of quasicoherent sheaves F ⟶ A₁, by restriction to degree one along F ≅ Sym¹ F and by gradedSymmetricAlgebraLift.

TauCeti.AlgebraicGeometry.gradedSymmetricAlgebraAdjunction.{u} (X : AlgebraicGeometry.Scheme) :
  TauCeti.AlgebraicGeometry.gradedSymmetricAlgebra X ⊣
    TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.degreeOne

Lean

Formalized in Tau Ceti as TauCeti.AlgebraicGeometry.gradedSymmetricAlgebraAdjunction.

Sources

• Tau Ceti documentation: TauCeti.AlgebraicGeometry.gradedSymmetricAlgebraAdjunction
• Source of TauCeti.AlgebraicGeometry.gradedSymmetricAlgebraAdjunction in TauCeti/AlgebraicGeometry/Modules/Quasicoherent/GradedAlgebra/SymmetricAlgebra/Adjunction.lean
• Tau Ceti roadmap status: Algebraic vector bundles

LeanTauCeti.AlgebraicGeometry.gradedSymmetricAlgebraAdjunction

DefinitionTauCeti.AlgebraicGeometry.gradedSymmetricAlgebraEquiv#

The graded symmetric algebra functor is an equivalence between quasicoherent sheaves and graded quasicoherent algebras freely generated in degree one. Its inverse takes the degree-one component, and its unit is the identification F ≅ Sym¹ F.

TauCeti.AlgebraicGeometry.gradedSymmetricAlgebraEquiv.{u} (X : AlgebraicGeometry.Scheme) :
  TauCeti.AlgebraicGeometry.QuasicoherentSheaf X ≌
    TauCeti.AlgebraicGeometry.FreeGradedQuasicoherentAlgebra X

Lean

Formalized in Tau Ceti as TauCeti.AlgebraicGeometry.gradedSymmetricAlgebraEquiv.

Sources

• Tau Ceti documentation: TauCeti.AlgebraicGeometry.gradedSymmetricAlgebraEquiv
• Source of TauCeti.AlgebraicGeometry.gradedSymmetricAlgebraEquiv in TauCeti/AlgebraicGeometry/Modules/Quasicoherent/GradedAlgebra/Free.lean
• Tau Ceti roadmap status: Algebraic vector bundles

LeanTauCeti.AlgebraicGeometry.gradedSymmetricAlgebraEquiv

DefinitionTauCeti.AlgebraicGeometry.gradedRelativeSpecEquiv#

Graded relative Spec is an anti-equivalence between graded quasicoherent algebras and graded affine schemes over X. The functor sends A to the relative spectrum of ⨁ₙ Aₙ, graded through the relative-Spec unit p_* 𝒪 ≅ ⨁ₙ Aₙ, and the inverse reads off the grading. The unit is the identity, and the counit is, on underlying schemes, relative Spec of the grading isomorphism followed by the relative-Spec counit.

TauCeti.AlgebraicGeometry.gradedRelativeSpecEquiv.{u} (X : AlgebraicGeometry.Scheme) :
  (TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra X)ᵒᵖ ≌
    TauCeti.AlgebraicGeometry.GradedAffineSchemeOver X

Lean

Formalized in Tau Ceti as TauCeti.AlgebraicGeometry.gradedRelativeSpecEquiv.

Sources

• Tau Ceti documentation: TauCeti.AlgebraicGeometry.gradedRelativeSpecEquiv
• Source of TauCeti.AlgebraicGeometry.gradedRelativeSpecEquiv in TauCeti/AlgebraicGeometry/RelativeSpec/Graded.lean
• Tau Ceti roadmap status: Algebraic vector bundles

LeanTauCeti.AlgebraicGeometry.gradedRelativeSpecEquiv

Uses 1

Proof usesTauCeti.AlgebraicGeometry.relativeSpecEquiv

AbbreviationTauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf#

The full category of finite locally free sheaves on a scheme, that is, of locally free and finitely presented 𝒪_X-modules. Its morphisms are morphisms of 𝒪_X-modules.

TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.{u} (X : AlgebraicGeometry.Scheme) : Type (u + 1)

Lean

Formalized in Tau Ceti as TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.

Sources

• Tau Ceti documentation: TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf
• Source of TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf in TauCeti/AlgebraicGeometry/VectorBundle/FiniteLocallyFree.lean
• Tau Ceti roadmap status: Algebraic vector bundles

LeanTauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf

Used by 4

Used byTauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.evalNatIso · TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.pullbackDeterminantIso · TauCeti.AlgebraicGeometry.QuasicoherentSheaf.nonempty_hasLeftDual_iff_isFiniteLocallyFree · The Abel–Jacobi map into the degree-zero Picard fppf sheaf

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.