theorem
L46 ↗classify_tensor
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.classify_tensor
Source context 12 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ClassifyTensor
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open scoped CategoryTheory.MonObj
with_weak_namespace _root_.AlgebraicGeometry.RelPicard.RepresentsRelSubPicLean source · statement
theorem classify_tensor
{R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
{ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c}
{P : SubPicGroupCondition c ε} {D : RelativePic0Designation R c}
(h : RepresentsRelSubPic c ε P.toSubPicCondition D)
{T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (L M : RigidifiedLineBundle c ε t)
(hL : P.P t L) (hM : P.P t M) :
h.classify t (L.tensor M) (P.tensor_mem t L M hL hM) =
h.relativeGroupLaw.mul t (h.classify t L hL) (h.classify t M hM)