Tensor products of line bundles

The sheafified tensor product of 𝒪_X-modules sends two line bundles to a line bundle. This file packages that operation in the category InvertibleSheaf X, together with the unit computations for the trivial line bundle.

Main declarations

• InvertibleSheaf.tensorProduct packages the tensor product of two line bundles;
• InvertibleSheaf.trivialObjIsoUnit identifies the trivial line bundle with the monoidal unit;
• InvertibleSheaf.tensorProduct_obj identifies its underlying sheaf;
• InvertibleSheaf.tensorProductCongrLeft and InvertibleSheaf.tensorProductCongrRight transport isomorphisms through either tensor factor, so InvertibleSheaf.isIsomorphic_tensorProduct shows that tensor product respects isomorphism;
• InvertibleSheaf.tensorProductComm exchanges the two tensor factors;
• InvertibleSheaf.tensorProductAssoc is the associativity isomorphism;
• InvertibleSheaf.tensorTrivialLeftIso and InvertibleSheaf.tensorTrivialRightIso are the unit isomorphisms in the full category of invertible sheaves.

The underlying sheaf is exposed by tensorProduct_obj, while the congruence, symmetry, associativity, and unit isomorphisms provide the categorical API for manipulating tensor products of line bundles.

noncomputable def TauCeti.AlgebraicGeometry.InvertibleSheaf.trivialObjIsoUnit (X : AlgebraicGeometry.Scheme) : (trivial X).obj ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit X.Modules

The trivial line bundle is isomorphic to the monoidal unit of X.Modules. Here 𝟙_ X.Modules unfolds to SheafOfModules.unit X.ringCatSheaf.

Equations

• TauCeti.AlgebraicGeometry.InvertibleSheaf.trivialObjIsoUnit X = ⋯ ▸ TauCeti.SheafOfModules.freePUnitIsoUnit X.ringCatSheaf

noncomputable def TauCeti.AlgebraicGeometry.InvertibleSheaf.tensorProduct {X : AlgebraicGeometry.Scheme} (L K : InvertibleSheaf X) : InvertibleSheaf X

The tensor product of two line bundles on a scheme.

Equations

• L.tensorProduct K = { obj := TauCeti.SheafOfModules.tensorProduct X.sheaf L.obj K.obj, property := ⋯ }

@[simp]

theorem TauCeti.AlgebraicGeometry.InvertibleSheaf.tensorProduct_obj {X : AlgebraicGeometry.Scheme} (L K : InvertibleSheaf X) : (L.tensorProduct K).obj = SheafOfModules.tensorProduct X.sheaf L.obj K.obj

The underlying sheaf of tensorProduct L K is the sheafified tensor product of the underlying sheaves of L and K.

noncomputable def TauCeti.AlgebraicGeometry.InvertibleSheaf.tensorProductCongrLeftIso {X : AlgebraicGeometry.Scheme} {L L' K : InvertibleSheaf X} (e : L ≅ L') : (L.tensorProduct K).obj ≅ (L'.tensorProduct K).obj

The sheaf isomorphism underlying transport through the first tensor factor.

Equations

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

noncomputable def TauCeti.AlgebraicGeometry.InvertibleSheaf.tensorProductCongrLeft {X : AlgebraicGeometry.Scheme} {L L' K : InvertibleSheaf X} (e : L ≅ L') : L.tensorProduct K ≅ L'.tensorProduct K

An isomorphism of the first factor transports through the tensor product.

Equations

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

@[simp]

theorem TauCeti.AlgebraicGeometry.InvertibleSheaf.tensorProductCongrLeft_hom_val {X : AlgebraicGeometry.Scheme} {L L' K : InvertibleSheaf X} (e : L ≅ L') : (tensorProductCongrLeft e).hom.hom.val = (tensorProductCongrLeftIso e).hom.val

@[simp]

theorem TauCeti.AlgebraicGeometry.InvertibleSheaf.tensorProductCongrLeft_inv_val {X : AlgebraicGeometry.Scheme} {L L' K : InvertibleSheaf X} (e : L ≅ L') : (tensorProductCongrLeft e).inv.hom.val = (tensorProductCongrLeftIso e).inv.val

noncomputable def TauCeti.AlgebraicGeometry.InvertibleSheaf.tensorProductCongrRightIso {X : AlgebraicGeometry.Scheme} {L K K' : InvertibleSheaf X} (e : K ≅ K') : (L.tensorProduct K).obj ≅ (L.tensorProduct K').obj

The sheaf isomorphism underlying transport through the second tensor factor.

Equations

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

noncomputable def TauCeti.AlgebraicGeometry.InvertibleSheaf.tensorProductCongrRight {X : AlgebraicGeometry.Scheme} {L K K' : InvertibleSheaf X} (e : K ≅ K') : L.tensorProduct K ≅ L.tensorProduct K'

An isomorphism of the second factor transports through the tensor product.

Equations

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

@[simp]

theorem TauCeti.AlgebraicGeometry.InvertibleSheaf.tensorProductCongrRight_hom_val {X : AlgebraicGeometry.Scheme} {L K K' : InvertibleSheaf X} (e : K ≅ K') : (tensorProductCongrRight e).hom.hom.val = (tensorProductCongrRightIso e).hom.val

@[simp]

theorem TauCeti.AlgebraicGeometry.InvertibleSheaf.tensorProductCongrRight_inv_val {X : AlgebraicGeometry.Scheme} {L K K' : InvertibleSheaf X} (e : K ≅ K') : (tensorProductCongrRight e).inv.hom.val = (tensorProductCongrRightIso e).inv.val

theorem TauCeti.AlgebraicGeometry.InvertibleSheaf.isIsomorphic_tensorProduct {X : AlgebraicGeometry.Scheme} {L L' K K' : InvertibleSheaf X} (hL : CategoryTheory.IsIsomorphic L L') (hK : CategoryTheory.IsIsomorphic K K') : CategoryTheory.IsIsomorphic (L.tensorProduct K) (L'.tensorProduct K')

Tensor product preserves isomorphism of line bundles in both variables.

noncomputable def TauCeti.AlgebraicGeometry.InvertibleSheaf.tensorProductCommIso {X : AlgebraicGeometry.Scheme} (L K : InvertibleSheaf X) : (L.tensorProduct K).obj ≅ (K.tensorProduct L).obj

The sheaf isomorphism underlying symmetry of the tensor product of line bundles.

Equations

• L.tensorProductCommIso K = ⋯.mpr (TauCeti.SheafOfModules.tensorProductComm X.sheaf L.obj K.obj)

noncomputable def TauCeti.AlgebraicGeometry.InvertibleSheaf.tensorProductComm {X : AlgebraicGeometry.Scheme} (L K : InvertibleSheaf X) : L.tensorProduct K ≅ K.tensorProduct L

The tensor product of line bundles is symmetric.

Equations

• L.tensorProductComm K = (TauCeti.AlgebraicGeometry.SheafOfModules.isInvertible X).isoMk (AlgebraicGeometry.Scheme.Modules.isoOfSheafIso X (L.tensorProductCommIso K))

@[simp]

theorem TauCeti.AlgebraicGeometry.InvertibleSheaf.tensorProductComm_hom_val {X : AlgebraicGeometry.Scheme} (L K : InvertibleSheaf X) : (L.tensorProductComm K).hom.hom.val = (L.tensorProductCommIso K).hom.val

@[simp]

theorem TauCeti.AlgebraicGeometry.InvertibleSheaf.tensorProductComm_inv_val {X : AlgebraicGeometry.Scheme} (L K : InvertibleSheaf X) : (L.tensorProductComm K).inv.hom.val = (L.tensorProductCommIso K).inv.val

noncomputable def TauCeti.AlgebraicGeometry.InvertibleSheaf.tensorProductAssocIso {X : AlgebraicGeometry.Scheme} (L K M : InvertibleSheaf X) : ((L.tensorProduct K).tensorProduct M).obj ≅ (L.tensorProduct (K.tensorProduct M)).obj

The sheaf isomorphism underlying associativity of the tensor product of line bundles.

Equations

• L.tensorProductAssocIso K M = ⋯.mpr (TauCeti.SheafOfModules.tensorProductAssoc X.sheaf L.obj K.obj M.obj)

noncomputable def TauCeti.AlgebraicGeometry.InvertibleSheaf.tensorProductAssoc {X : AlgebraicGeometry.Scheme} (L K M : InvertibleSheaf X) : (L.tensorProduct K).tensorProduct M ≅ L.tensorProduct (K.tensorProduct M)

The tensor product of line bundles is associative.

Equations

• L.tensorProductAssoc K M = (TauCeti.AlgebraicGeometry.SheafOfModules.isInvertible X).isoMk (AlgebraicGeometry.Scheme.Modules.isoOfSheafIso X (L.tensorProductAssocIso K M))

@[simp]

theorem TauCeti.AlgebraicGeometry.InvertibleSheaf.tensorProductAssoc_hom_val {X : AlgebraicGeometry.Scheme} (L K M : InvertibleSheaf X) : (L.tensorProductAssoc K M).hom.hom.val = (L.tensorProductAssocIso K M).hom.val

@[simp]

theorem TauCeti.AlgebraicGeometry.InvertibleSheaf.tensorProductAssoc_inv_val {X : AlgebraicGeometry.Scheme} (L K M : InvertibleSheaf X) : (L.tensorProductAssoc K M).inv.hom.val = (L.tensorProductAssocIso K M).inv.val

noncomputable def TauCeti.AlgebraicGeometry.InvertibleSheaf.tensorTrivialLeftIsoSheaf {X : AlgebraicGeometry.Scheme} (L : InvertibleSheaf X) : ((trivial X).tensorProduct L).obj ≅ L.obj

The sheaf isomorphism underlying the left unit for the tensor product of line bundles.

Equations

• L.tensorTrivialLeftIsoSheaf = ⋯.mpr (TauCeti.SheafOfModules.tensorProductFreePUnitIsoLeft X.sheaf L.obj)

noncomputable def TauCeti.AlgebraicGeometry.InvertibleSheaf.tensorTrivialLeftIso {X : AlgebraicGeometry.Scheme} (L : InvertibleSheaf X) : (trivial X).tensorProduct L ≅ L

The trivial line bundle is a left unit for the sheafified tensor product of invertible sheaves.

Equations

• L.tensorTrivialLeftIso = (TauCeti.AlgebraicGeometry.SheafOfModules.isInvertible X).isoMk (AlgebraicGeometry.Scheme.Modules.isoOfSheafIso X L.tensorTrivialLeftIsoSheaf)

@[simp]

theorem TauCeti.AlgebraicGeometry.InvertibleSheaf.tensorTrivialLeftIso_hom_val {X : AlgebraicGeometry.Scheme} (L : InvertibleSheaf X) : L.tensorTrivialLeftIso.hom.hom.val = L.tensorTrivialLeftIsoSheaf.hom.val

@[simp]

theorem TauCeti.AlgebraicGeometry.InvertibleSheaf.tensorTrivialLeftIso_inv_val {X : AlgebraicGeometry.Scheme} (L : InvertibleSheaf X) : L.tensorTrivialLeftIso.inv.hom.val = L.tensorTrivialLeftIsoSheaf.inv.val

noncomputable def TauCeti.AlgebraicGeometry.InvertibleSheaf.tensorTrivialRightIsoSheaf {X : AlgebraicGeometry.Scheme} (L : InvertibleSheaf X) : (L.tensorProduct (trivial X)).obj ≅ L.obj

The sheaf isomorphism underlying the right unit for the tensor product of line bundles.

Equations

• L.tensorTrivialRightIsoSheaf = ⋯.mpr (TauCeti.SheafOfModules.tensorProductFreePUnitIsoRight X.sheaf L.obj)

noncomputable def TauCeti.AlgebraicGeometry.InvertibleSheaf.tensorTrivialRightIso {X : AlgebraicGeometry.Scheme} (L : InvertibleSheaf X) : L.tensorProduct (trivial X) ≅ L

The trivial line bundle is a right unit for the sheafified tensor product of invertible sheaves.

Equations

• L.tensorTrivialRightIso = (TauCeti.AlgebraicGeometry.SheafOfModules.isInvertible X).isoMk (AlgebraicGeometry.Scheme.Modules.isoOfSheafIso X L.tensorTrivialRightIsoSheaf)

@[simp]

theorem TauCeti.AlgebraicGeometry.InvertibleSheaf.tensorTrivialRightIso_hom_val {X : AlgebraicGeometry.Scheme} (L : InvertibleSheaf X) : L.tensorTrivialRightIso.hom.hom.val = L.tensorTrivialRightIsoSheaf.hom.val

@[simp]

theorem TauCeti.AlgebraicGeometry.InvertibleSheaf.tensorTrivialRightIso_inv_val {X : AlgebraicGeometry.Scheme} (L : InvertibleSheaf X) : L.tensorTrivialRightIso.inv.hom.val = L.tensorTrivialRightIsoSheaf.inv.val