Tensor compatibility of the affine vector-bundle equivalence

The equivalence between finite projective R-modules and finite locally free sheaves on Spec R is monoidal. Its tensor and unit comparisons are the restrictions of the comparisons of AlgebraicGeometry.tilde.functor, and the inverse functor of global sections carries the compatible monoidal structure. The existing unit and counit are monoidal transformations.

We use TauCeti.AlgebraicGeometry.tildeMonoidal and Mathlib's CategoryTheory.Equivalence.inverseMonoidal, so the tensor operations on both full subcategories remain those of modules and sheaves, respectively.

References

• R. Hartshorne, Algebraic Geometry, Proposition II.5.2 (b).

@[instance_reducible]

noncomputable instance TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.finiteProjectiveEquivFunctorMonoidal (R : CommRingCat) : (finiteProjectiveEquiv R).functor.Monoidal

The affine equivalence preserves tensor products and the tensor unit, using the canonical comparisons of the associated-sheaf functor.

Equations

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

@[simp]

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.finiteProjectiveEquiv_functor_ε_hom (R : CommRingCat) : (CategoryTheory.Functor.LaxMonoidal.ε (finiteProjectiveEquiv R).functor).hom = CategoryTheory.Functor.LaxMonoidal.ε (AlgebraicGeometry.tilde.functor R)

The underlying unit comparison is that of the associated-sheaf functor.

@[simp]

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.finiteProjectiveEquiv_functor_μ_hom (R : CommRingCat) (M N : (finiteProjectiveModules ↑R).FullSubcategory) : (CategoryTheory.Functor.LaxMonoidal.μ (finiteProjectiveEquiv R).functor M N).hom = CategoryTheory.Functor.LaxMonoidal.μ (AlgebraicGeometry.tilde.functor R) M.obj N.obj

The underlying tensor comparison is that of the associated-sheaf functor.

@[simp]

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.finiteProjectiveEquiv_functor_η_hom (R : CommRingCat) : (CategoryTheory.Functor.OplaxMonoidal.η (finiteProjectiveEquiv R).functor).hom = CategoryTheory.Functor.OplaxMonoidal.η (AlgebraicGeometry.tilde.functor R)

The underlying oplax unit comparison is that of the associated-sheaf functor.

@[simp]

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.finiteProjectiveEquiv_functor_δ_hom (R : CommRingCat) (M N : (finiteProjectiveModules ↑R).FullSubcategory) : (CategoryTheory.Functor.OplaxMonoidal.δ (finiteProjectiveEquiv R).functor M N).hom = CategoryTheory.Functor.OplaxMonoidal.δ (AlgebraicGeometry.tilde.functor R) M.obj N.obj

The underlying oplax tensor comparison is that of the associated-sheaf functor.

@[instance_reducible]

noncomputable instance TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.finiteProjectiveEquivInverseMonoidal (R : CommRingCat) : (finiteProjectiveEquiv R).inverse.Monoidal

Global sections on finite locally free sheaves carries the monoidal structure inverse to that of the associated-sheaf functor.

Equations

• TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.finiteProjectiveEquivInverseMonoidal R = (TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.finiteProjectiveEquiv R).inverseMonoidal

instance TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.finiteProjectiveEquiv_isMonoidal (R : CommRingCat) : (finiteProjectiveEquiv R).IsMonoidal

The affine equivalence, with its canonical unit and counit, is monoidal.