Exterior powers of finite locally free sheaves #
Let R be a sheaf of commutative rings on a small site. Since exterior powers commute with
restriction to a slice (SheafOfModules.overExteriorPowerIso) and the n-th exterior power of
the free sheaf on a finite linearly ordered type I is free on the n-element subsets of I
(SheafOfModules.exteriorPowerFreeIso), a basis of a sheaf of modules M over an object X
indexed by a finite type I yields a basis of ⋀ⁿ M over X indexed by the n-element subsets
of I. Consequently, exterior powers of finite locally free sheaves are finite locally free, and
a local basis with r elements gives a local basis of the n-th exterior power with
r.choose n elements. This is the input for the rank formula and the determinant of a vector
bundle.
Main declarations #
SheafOfModules.GeneratingSections.exteriorPower: the basis of⋀ⁿ MoverXinduced by a finite basis ofMoverX;SheafOfModules.isFiniteLocallyFree_exteriorPower: exterior powers of finite locally free sheaves are finite locally free.
References #
- [R. Hartshorne, Algebraic Geometry][hartshorne1977], Chapter II, Exercise 5.16
noncomputable def
SheafOfModules.GeneratingSections.exteriorPower
{C : Type u}
[CategoryTheory.SmallCategory C]
{J : CategoryTheory.GrothendieckTopology C}
[J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
[CategoryTheory.HasWeakSheafify J AddCommGrpCat]
[J.WEqualsLocallyBijective AddCommGrpCat]
{R : CategoryTheory.Sheaf J CommRingCat}
[∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
[∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat]
[∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat]
{M : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)}
{X : C}
(σ : (M.over X).GeneratingSections)
[CategoryTheory.IsIso σ.π]
[Finite σ.I]
[LinearOrder σ.I]
(n : ℕ)
:
(((SheafOfModules.exteriorPower R n).obj M).over X).GeneratingSections
A basis of M over X indexed by a finite linearly ordered type σ.I induces a basis of the
n-th exterior power of M over X, indexed by the n-element subsets of σ.I.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
SheafOfModules.GeneratingSections.exteriorPower_I
{C : Type u}
[CategoryTheory.SmallCategory C]
{J : CategoryTheory.GrothendieckTopology C}
[J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
[CategoryTheory.HasWeakSheafify J AddCommGrpCat]
[J.WEqualsLocallyBijective AddCommGrpCat]
{R : CategoryTheory.Sheaf J CommRingCat}
[∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
[∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat]
[∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat]
{M : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)}
{X : C}
(σ : (M.over X).GeneratingSections)
[CategoryTheory.IsIso σ.π]
[Finite σ.I]
[LinearOrder σ.I]
(n : ℕ)
:
The basis σ.exteriorPower n is indexed by the n-element subsets of σ.I.
theorem
SheafOfModules.GeneratingSections.exteriorPower_def
{C : Type u}
[CategoryTheory.SmallCategory C]
{J : CategoryTheory.GrothendieckTopology C}
[J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
[CategoryTheory.HasWeakSheafify J AddCommGrpCat]
[J.WEqualsLocallyBijective AddCommGrpCat]
{R : CategoryTheory.Sheaf J CommRingCat}
[∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
[∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat]
[∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat]
{M : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)}
{X : C}
(σ : (M.over X).GeneratingSections)
[CategoryTheory.IsIso σ.π]
[Finite σ.I]
[LinearOrder σ.I]
(n : ℕ)
:
σ.exteriorPower n = (equivOfIso
(overExteriorPowerIso n M X ≪≫ (SheafOfModules.exteriorPower (R.over X) n).mapIso (CategoryTheory.asIso σ.π).symm ≪≫ exteriorPowerFreeIso σ.I n).symm)
(free.generatingSections ↑(Set.powersetCard σ.I n))
The characteristic equation of σ.exteriorPower n: it is the basis of the free sheaf on the
n-element subsets of σ.I, transported along the composite of overExteriorPowerIso, the
exterior power of the inverse of σ.π, and exteriorPowerFreeIso.
instance
SheafOfModules.GeneratingSections.isIso_exteriorPower_π
{C : Type u}
[CategoryTheory.SmallCategory C]
{J : CategoryTheory.GrothendieckTopology C}
[J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
[CategoryTheory.HasWeakSheafify J AddCommGrpCat]
[J.WEqualsLocallyBijective AddCommGrpCat]
{R : CategoryTheory.Sheaf J CommRingCat}
[∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
[∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat]
[∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat]
{M : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)}
{X : C}
(σ : (M.over X).GeneratingSections)
[CategoryTheory.IsIso σ.π]
[Finite σ.I]
[LinearOrder σ.I]
(n : ℕ)
:
instance
SheafOfModules.GeneratingSections.finite_exteriorPower_I
{C : Type u}
[CategoryTheory.SmallCategory C]
{J : CategoryTheory.GrothendieckTopology C}
[J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
[CategoryTheory.HasWeakSheafify J AddCommGrpCat]
[J.WEqualsLocallyBijective AddCommGrpCat]
{R : CategoryTheory.Sheaf J CommRingCat}
[∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
[∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat]
[∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat]
{M : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)}
{X : C}
(σ : (M.over X).GeneratingSections)
[CategoryTheory.IsIso σ.π]
[Finite σ.I]
[LinearOrder σ.I]
(n : ℕ)
:
Finite (σ.exteriorPower n).I
theorem
SheafOfModules.isFiniteLocallyFree_exteriorPower
{C : Type u}
[CategoryTheory.SmallCategory C]
{J : CategoryTheory.GrothendieckTopology C}
[J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
[CategoryTheory.HasWeakSheafify J AddCommGrpCat]
[J.WEqualsLocallyBijective AddCommGrpCat]
{R : CategoryTheory.Sheaf J CommRingCat}
[∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
[∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat]
[∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat]
(M : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R))
(n : ℕ)
[CategoryTheory.Limits.HasPullbacks C]
[∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat]
(hM : isFiniteLocallyFree (TauCeti.SheafOfModules.ringCatSheaf R) M)
:
The exterior powers of a finite locally free sheaf of modules are finite locally free.