structure SheafOfModules.VectorBundleData {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)] [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrp] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrp] (M : SheafOfModules R) : Type (max (u + 1) (v + 1))

A vector bundle is a sheaf of modules that is locally isomorphic to a free sheaf.

• OpensIndex : Type u

  The index type for the open cover on which the vector bundle is free.

• opens : self.OpensIndex → C

  The indexed family of opens on which the vector bundle is free.

• coversTop : J.CoversTop self.opens

  The indexed family of opens covers the base.

• BasisIndex : self.OpensIndex → Type v

  The indexed family of types that index local bases for the vector bundle.

• locallyFree (i : self.OpensIndex) : M.over (self.opens i) ≅ free (self.BasisIndex i)

  The restriction of the vector bundle to one of the opens is free.

structure SheafOfModules.FiniteRankVectorBundleData {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)] [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrp] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrp] (M : SheafOfModules R) extends M.VectorBundleData : Type (max (u + 1) (v + 1))

• OpensIndex : Type u
• opens : self.OpensIndex → C
• coversTop : J.CoversTop self.opens
• BasisIndex : self.OpensIndex → Type v
• locallyFree (i : self.OpensIndex) : M.over (self.opens i) ≅ free (self.BasisIndex i)
• finite (i : self.OpensIndex) : Finite (self.BasisIndex i)

  The predicate that every local basis in the defining data of the vector bundle is finite.

class SheafOfModules.IsVectorBundleWithRank {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)] [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrp] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrp] (M : SheafOfModules R) (n : ℕ) : Prop

A class for vector bundles of constant finite rank.

• exists_vector_bundle_data : ∃ (D : M.FiniteRankVectorBundleData), ∀ (i : D.OpensIndex), Nat.card (D.BasisIndex i) = n

  The predicate that a sheaf of modules is locally free.