Sections through the dual: the reduction of 2.10

Deligne reduces local splitting of a general short exact sequence to sequences ending at the unit: a section of an epimorphism onto C is the same thing as a unit-side lifting through the left dual. This is the pure rigid-adjunction kernel of that reduction; the splitting-algebra argument then only ever meets maps out of the unit.

noncomputable def RS.dualUnitPoint {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RigidCategory A] (C : A) : CategoryTheory.MonoidalCategoryStruct.tensorUnit A ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (ᘁC) C

The dual-side comparison point: the image of the right unitor under the duality adjunction — the coevaluation-flavoured map the liftings are measured against.

Equations

• RS.dualUnitPoint C = (CategoryTheory.tensorLeftHomEquiv (CategoryTheory.MonoidalCategoryStruct.tensorUnit A) (ᘁC) C C) (CategoryTheory.MonoidalCategoryStruct.rightUnitor C).hom

theorem RS.exists_section_iff_unit_lift {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RigidCategory A] {B C : A} (b : B ⟶ C) : (∃ (t : C ⟶ B), CategoryTheory.CategoryStruct.comp t b = CategoryTheory.CategoryStruct.id C) ↔ ∃ (s : CategoryTheory.MonoidalCategoryStruct.tensorUnit A ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (ᘁC) B), CategoryTheory.CategoryStruct.comp s (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (ᘁC) b) = dualUnitPoint C

Sections through the dual: an epimorphism onto C admits a section exactly when the dual-side unit map lifts through it.

noncomputable def RS.unitEnd {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RigidCategory A] [CategoryTheory.Abelian A] {B C : A} (b : B ⟶ C) : A

The unit-ending object of the reduction: the preimage of the dual-side unit point inside the dual-twisted middle term.

Equations

• RS.unitEnd b = CategoryTheory.Limits.pullback (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (ᘁC) b) (RS.dualUnitPoint C)

noncomputable def RS.unitEndProj {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RigidCategory A] [CategoryTheory.Abelian A] {B C : A} (b : B ⟶ C) : unitEnd b ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit A

Its projection to the unit.

Equations

• RS.unitEndProj b = CategoryTheory.Limits.pullback.snd (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (ᘁC) b) (RS.dualUnitPoint C)

noncomputable def RS.kernelPullbackSndIso {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z) : CategoryTheory.Limits.kernel (CategoryTheory.Limits.pullback.snd f g) ≅ CategoryTheory.Limits.kernel f

The kernel of the second pullback projection is the kernel of the first leg.

Equations

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