The base-change section for embedded short exact sequences

RS.Classical.Deligne.Rappel210Ind proves the local splitting statement (Deligne 2.10) over Ind C for every short exact sequence S whose quotient S.X₃, whose dual S.X₃ᘁ and whose unit-form middle RS.unitFormMid S carry the duals used in the reduction. This file discharges all four of those side conditions for the sequences that the fibre-functor assembly actually consumes: the images T.map RS.indOf of short exact sequences of C.

• RS.exactPairingOfIso — an exact pairing transports along an isomorphism of its left leg (Mathlib has the analogous CategoryTheory.rightDualIso/leftDualIso comparisons, but no transport of the pairing itself);
• RS.hasRightDualIndOf — embedded objects carry right duals, from RS.exactPairingIndOf; the dual of RS.indOf.obj X is RS.indOf.obj (Xᘁ) by construction, so the duals of S.X₃ᘁ are instances of the same lemma and HasLeftDual (S.X₃ᘁ) is Mathlib's CategoryTheory.hasLeftDualRightDual;
• RS.unitName_indOf — the name of the identity transports along the embedding, from the strong braided monoidal structure RS.indOfBraided;
• RS.unitFormMidIndOfIso — the unit-form middle of an embedded sequence is embedded: RS.unitFormMid is a pullback of maps between embedded objects, and RS.indOf preserves limits, so the comparison isomorphisms of the tensor and unit comparisons turn the cospan upstairs into the image of the cospan downstairs;
• RS.rappel210_indOf — Deligne 2.10 for embedded sequences.

The fourth side condition is the only one with content: C is rigid, so the pullback taken in C has a right dual there, and RS.exactPairingOfIso carries the embedded pairing across the comparison isomorphism.

@[implicit_reducible]

def RS.exactPairingOfIso {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {X X' Y : D} [CategoryTheory.ExactPairing X Y] (e : X ≅ X') : CategoryTheory.ExactPairing X' Y

Exact pairings transport along an isomorphism of the left leg.

Equations

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

@[instance_reducible]

noncomputable instance RS.hasRightDualIndOf {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] (X : C) : CategoryTheory.HasRightDual (indOf.obj X)

Embedded objects inherit right duals.

Equations

• RS.hasRightDualIndOf X = { rightDual := RS.indOf.obj Xᘁ, exact := RS.exactPairingIndOf X Xᘁ }

theorem RS.coevaluation_indOf {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] (X : C) : η_ (indOf.obj X) (indOf.obj Xᘁ) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε indOf) (CategoryTheory.CategoryStruct.comp (indOf.map (η_ X Xᘁ)) (CategoryTheory.Functor.OplaxMonoidal.δ indOf X Xᘁ))

The coevaluation of an embedded pairing: the unit comparison, the image of the coevaluation, and the cotensorator.

theorem RS.delta_braiding_indOf {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] (X Y : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ indOf X Y) (β_ (indOf.obj X) (indOf.obj Y)).hom = CategoryTheory.CategoryStruct.comp (indOf.map (β_ X Y).hom) (CategoryTheory.Functor.OplaxMonoidal.δ indOf Y X)

The cotensorator intertwines the braidings: the embedding is braided, so the braiding upstairs is the image of the braiding downstairs, conjugated by the tensor comparisons.

theorem RS.unitName_indOf {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.RigidCategory C] (X : C) : unitName (indOf.obj X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε indOf) (CategoryTheory.CategoryStruct.comp (indOf.map (unitName X)) (CategoryTheory.Functor.OplaxMonoidal.δ indOf Xᘁ X))

The name of the identity transports along the embedding.

noncomputable def RS.unitFormMidIndOfIso {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RigidCategory C] (T : CategoryTheory.ShortComplex C) : indOf.obj (unitFormMid T) ≅ CategoryTheory.Limits.pullback (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (indOf.obj T.X₃ᘁ) (indOf.map T.g)) (unitName (indOf.obj T.X₃))

The unit-form middle of an embedded sequence is embedded: the pullback displayed here is RS.unitFormMid (T.map RS.indOf) with the dual instance of RS.hasRightDualIndOf, written out so that the statement needs no local instance. The embedding preserves the pullback, and the tensor and unit comparisons carry the cospan downstairs to the cospan upstairs.

Equations

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

theorem RS.rappel210_indOf {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RigidCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Linear ℂ (CategoryTheory.Ind C)] [CategoryTheory.MonoidalLinear ℂ (CategoryTheory.Ind C)] (T : CategoryTheory.ShortComplex C) (hT : T.ShortExact) (h1 : ¬CategoryTheory.Limits.IsZero (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Ind C))) : ∃ (A : CategoryTheory.Ind C) (x : CategoryTheory.MonObj A) (_ : CategoryTheory.IsCommMonObj A), CategoryTheory.MonObj.one ≠ 0 ∧ ∃ (s : freeMod A (T.map indOf).X₃ ⟶ freeMod A (T.map indOf).X₂), CategoryTheory.CategoryStruct.comp s (freeModMap A (T.map indOf).g) = CategoryTheory.CategoryStruct.id (freeMod A (T.map indOf).X₃)

The local splitting statement for embedded short exact sequences (Deligne 2.10): the image in Ind C of a short exact sequence of C splits after base change to a nonzero commutative algebra. The four duality side conditions of RS.rappel210_ind are supplied here: the quotient and its dual are embedded, and so — up to isomorphism — is the unit-form middle.