Finite locally free sheaves of fixed rank

A finite locally free sheaf has a locally constant rank, which need not be constant on a disconnected scheme. This file packages the sheaves whose rank is constantly r as the full subcategory FiniteLocallyFreeSheaf.FixedRank X r. The package is stable under arbitrary pullback, and the free sheaf on a universe lift of Fin r gives its standard object.

In rank one, fixed-rank finite locally free sheaves are exactly invertible sheaves. The equivalence InvertibleSheaf.fixedRankOneEquiv is the identity on underlying sheaves and morphisms; it only changes which equivalent rank-one condition is bundled with the object.

Main declarations

• FiniteLocallyFreeSheaf.isConstantRank: the property that the rank is constantly r;
• FiniteLocallyFreeSheaf.FixedRank X r: finite locally free sheaves of fixed rank r;
• FiniteLocallyFreeSheaf.FixedRank.pullback: pullback of fixed-rank sheaves;
• InvertibleSheaf.fixedRankOneEquiv: the equivalence between invertible sheaves and finite locally free sheaves of fixed rank one.

def TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.isConstantRank (X : AlgebraicGeometry.Scheme) (r : ℕ) : CategoryTheory.ObjectProperty (FiniteLocallyFreeSheaf X)

The property that a finite locally free sheaf has rank r at every point.

Equations

• TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.isConstantRank X r E = ∀ (x : ↥X), E.rank x = r

@[simp]

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.isConstantRank_iff {X : AlgebraicGeometry.Scheme} (E : FiniteLocallyFreeSheaf X) (r : ℕ) : isConstantRank X r E ↔ ∀ (x : ↥X), E.rank x = r

A finite locally free sheaf has constant rank r exactly when its rank is r at every point.

instance TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.instIsClosedUnderIsomorphismsIsConstantRank (X : AlgebraicGeometry.Scheme) (r : ℕ) : (isConstantRank X r).IsClosedUnderIsomorphisms

Constant rank is preserved by isomorphisms of finite locally free sheaves.

@[reducible, inline]

abbrev TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.FixedRank (X : AlgebraicGeometry.Scheme) (r : ℕ) : Type (u + 1)

The full category of finite locally free sheaves of rank r at every point of X.

Equations

• TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.FixedRank X r = (TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.isConstantRank X r).FullSubcategory

@[reducible, inline]

abbrev TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.FixedRank.toFiniteLocallyFree (X : AlgebraicGeometry.Scheme) (r : ℕ) : CategoryTheory.Functor (FixedRank X r) (FiniteLocallyFreeSheaf X)

Forget that a finite locally free sheaf has fixed rank.

Equations

• TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.FixedRank.toFiniteLocallyFree X r = (TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.isConstantRank X r).ι

@[simp]

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.FixedRank.rank_apply {X : AlgebraicGeometry.Scheme} {r : ℕ} (E : FixedRank X r) (x : ↥X) : E.obj.rank x = r

The rank of a fixed-rank finite locally free sheaf is its bundled rank at every point.

noncomputable def TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.FixedRank.free (X : AlgebraicGeometry.Scheme) (r : ℕ) : FixedRank X r

The free sheaf on a universe lift of Fin r, as a finite locally free sheaf of fixed rank r.

Equations

• TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.FixedRank.free X r = { obj := TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.free X (ULift.{?u.1, 0} (Fin r)), property := ⋯ }

@[simp]

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.FixedRank.free_obj (X : AlgebraicGeometry.Scheme) (r : ℕ) : (free X r).obj = FiniteLocallyFreeSheaf.free X (ULift.{u, 0} (Fin r))

Forgetting the fixed rank of the standard free sheaf gives the free finite locally free sheaf on a universe lift of Fin r.

noncomputable def TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.FixedRank.pullback {X : AlgebraicGeometry.Scheme} {r : ℕ} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : CategoryTheory.Functor (FixedRank Y r) (FixedRank X r)

Pullback of finite locally free sheaves of fixed rank.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.FixedRank.pullback_obj_obj {X : AlgebraicGeometry.Scheme} {r : ℕ} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (E : FixedRank Y r) : ((pullback f).obj E).obj = (FiniteLocallyFreeSheaf.pullback f).obj E.obj

The underlying finite locally free sheaf of a fixed-rank pullback is the ordinary pullback.

@[simp]

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.FixedRank.pullback_map_hom {X : AlgebraicGeometry.Scheme} {r : ℕ} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {E F : FixedRank Y r} (g : E ⟶ F) : ((pullback f).map g).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((FiniteLocallyFreeSheaf.pullback f).map g.hom) (CategoryTheory.eqToHom ⋯))

Pullback acts on morphisms of fixed-rank sheaves by the ordinary pullback functor.

def TauCeti.AlgebraicGeometry.InvertibleSheaf.toFixedRankOne (X : AlgebraicGeometry.Scheme) : CategoryTheory.Functor (InvertibleSheaf X) (FiniteLocallyFreeSheaf.FixedRank X 1)

Regard an invertible sheaf as a finite locally free sheaf of fixed rank one.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.AlgebraicGeometry.InvertibleSheaf.toFixedRankOne_obj_obj (X : AlgebraicGeometry.Scheme) (L : InvertibleSheaf X) : ((toFixedRankOne X).obj L).obj = (toFiniteLocallyFree X).obj L

The underlying finite locally free sheaf of an invertible sheaf regarded as a fixed-rank object is the existing inclusion into finite locally free sheaves.

@[simp]

theorem TauCeti.AlgebraicGeometry.InvertibleSheaf.toFixedRankOne_map_hom (X : AlgebraicGeometry.Scheme) {L M : InvertibleSheaf X} (f : L ⟶ M) : ((toFixedRankOne X).map f).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((toFiniteLocallyFree X).map f) (CategoryTheory.eqToHom ⋯))

The fixed-rank-one functor acts on morphisms through the existing inclusion of invertible sheaves into finite locally free sheaves.

def TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.FixedRank.toInvertible (X : AlgebraicGeometry.Scheme) : CategoryTheory.Functor (FixedRank X 1) (InvertibleSheaf X)

Regard a finite locally free sheaf of fixed rank one as an invertible sheaf.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.FixedRank.toInvertible_obj_obj (X : AlgebraicGeometry.Scheme) (E : FixedRank X 1) : ((toInvertible X).obj E).obj = E.obj.obj

The underlying sheaf of a fixed-rank-one object regarded as invertible is unchanged.

@[simp]

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.FixedRank.toInvertible_map_hom (X : AlgebraicGeometry.Scheme) {E F : FixedRank X 1} (f : E ⟶ F) : ((toInvertible X).map f).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp f.hom.hom (CategoryTheory.eqToHom ⋯))

The inverse rank-one functor is the identity on underlying module morphisms.

def TauCeti.AlgebraicGeometry.InvertibleSheaf.fixedRankOneEquiv (X : AlgebraicGeometry.Scheme) : InvertibleSheaf X ≌ FiniteLocallyFreeSheaf.FixedRank X 1

Invertible sheaves on X are equivalent to finite locally free sheaves of fixed rank one. Both functors preserve the underlying sheaves and module morphisms.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.AlgebraicGeometry.InvertibleSheaf.fixedRankOneEquiv_functor (X : AlgebraicGeometry.Scheme) : (fixedRankOneEquiv X).functor = toFixedRankOne X

The forward functor of the rank-one equivalence is the canonical inclusion of invertible sheaves into fixed-rank finite locally free sheaves.

theorem TauCeti.AlgebraicGeometry.InvertibleSheaf.fixedRankOneEquiv_inverse (X : AlgebraicGeometry.Scheme) : (fixedRankOneEquiv X).inverse = FiniteLocallyFreeSheaf.FixedRank.toInvertible X

The inverse functor of the rank-one equivalence only changes the bundled rank-one witness.

@[simp]

theorem TauCeti.AlgebraicGeometry.InvertibleSheaf.fixedRankOneEquiv_functor_obj_obj (X : AlgebraicGeometry.Scheme) (L : InvertibleSheaf X) : ((fixedRankOneEquiv X).functor.obj L).obj.obj = L.obj

The forward rank-one equivalence leaves the underlying sheaf unchanged.

@[simp]

theorem TauCeti.AlgebraicGeometry.InvertibleSheaf.fixedRankOneEquiv_inverse_obj_obj (X : AlgebraicGeometry.Scheme) (E : FiniteLocallyFreeSheaf.FixedRank X 1) : ((fixedRankOneEquiv X).inverse.obj E).obj = E.obj.obj

The inverse rank-one equivalence leaves the underlying sheaf unchanged.

theorem TauCeti.AlgebraicGeometry.InvertibleSheaf.fixedRankOneEquiv_unit_obj (X : AlgebraicGeometry.Scheme) (L : InvertibleSheaf X) : (((fixedRankOneEquiv X).functor.comp (fixedRankOneEquiv X).inverse).obj L).obj = L.obj

The composite underlying sheaf appearing in the unit of the rank-one equivalence is the original sheaf. This equality supplies the transport in the unit's characteristic equation.

@[simp]

theorem TauCeti.AlgebraicGeometry.InvertibleSheaf.fixedRankOneEquiv_unitIso_hom_app_hom (X : AlgebraicGeometry.Scheme) (L : InvertibleSheaf X) : ((fixedRankOneEquiv X).unitIso.hom.app L).hom = CategoryTheory.eqToHom ⋯

The unit of the rank-one equivalence is the identity map after identifying its target with the original underlying sheaf.

theorem TauCeti.AlgebraicGeometry.InvertibleSheaf.fixedRankOneEquiv_counit_obj (X : AlgebraicGeometry.Scheme) (E : FiniteLocallyFreeSheaf.FixedRank X 1) : (((fixedRankOneEquiv X).inverse.comp (fixedRankOneEquiv X).functor).obj E).obj.obj = E.obj.obj

The composite underlying sheaf appearing in the counit of the rank-one equivalence is the original sheaf. This equality supplies the transport in the counit's characteristic equation.

@[simp]

theorem TauCeti.AlgebraicGeometry.InvertibleSheaf.fixedRankOneEquiv_counitIso_hom_app_hom_hom (X : AlgebraicGeometry.Scheme) (E : FiniteLocallyFreeSheaf.FixedRank X 1) : ((fixedRankOneEquiv X).counitIso.hom.app E).hom.hom = CategoryTheory.eqToHom ⋯

The counit of the rank-one equivalence is the identity map after identifying its source with the original underlying sheaf.