Exactness of tensoring with a dualizable object

The first stage of the reduction of the local splitting statement: tensoring with a two-sided dualizable object is exact, because the exact pairings make the tensor functor a left and a right adjoint at once. A short exact sequence therefore stays short exact after tensoring, which produces the internal-hom extension that the pullback stage consumes.

theorem RS.tensorLeftPreservesColimits {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (X : D) [CategoryTheory.HasLeftDual X] : CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (CategoryTheory.MonoidalCategory.tensorLeft X)

Tensoring on the left with an object with a left dual preserves colimits: the exact pairing makes it a left adjoint.

theorem RS.tensorLeftPreservesLimits {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (X : D) [CategoryTheory.HasRightDual X] : CategoryTheory.Limits.PreservesLimitsOfSize.{0, 0, v, v, u, u} (CategoryTheory.MonoidalCategory.tensorLeft X)

Tensoring on the left with an object with a right dual preserves limits: the exact pairing makes it a right adjoint.

theorem RS.ShortExact_tensorLeft {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Abelian D] [CategoryTheory.MonoidalPreadditive D] {S : CategoryTheory.ShortComplex D} (hS : S.ShortExact) (X : D) [CategoryTheory.HasLeftDual X] [CategoryTheory.HasRightDual X] : (S.map (CategoryTheory.MonoidalCategory.tensorLeft X)).ShortExact

Tensoring with a two-sided dualizable object is exact: a short exact sequence stays short exact after tensoring on the left.

noncomputable def RS.unitName {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (X : D) [CategoryTheory.HasRightDual X] : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj Xᘁ X

The name of the identity: the coevaluation, braided into the evaluation source.

Equations

• RS.unitName X = CategoryTheory.CategoryStruct.comp (η_ X Xᘁ) (β_ X Xᘁ).hom

noncomputable def RS.unitFormMid {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Abelian D] (S : CategoryTheory.ShortComplex D) [CategoryTheory.HasRightDual S.X₃] : D

The middle object of the unit-form extension: the pullback of the internal-hom epimorphism along the name of the identity.

Equations

• RS.unitFormMid S = CategoryTheory.Limits.pullback (CategoryTheory.MonoidalCategoryStruct.whiskerLeft S.X₃ᘁ S.g) (RS.unitName S.X₃)

noncomputable def RS.unitFormIn {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Abelian D] [CategoryTheory.MonoidalPreadditive D] (S : CategoryTheory.ShortComplex D) [CategoryTheory.HasRightDual S.X₃] : CategoryTheory.MonoidalCategoryStruct.tensorObj S.X₃ᘁ S.X₁ ⟶ unitFormMid S

The inclusion of the unit-form extension.

Equations

• RS.unitFormIn S = CategoryTheory.Limits.pullback.lift (CategoryTheory.MonoidalCategoryStruct.whiskerLeft S.X₃ᘁ S.f) 0 ⋯

noncomputable def RS.unitForm {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Abelian D] [CategoryTheory.MonoidalPreadditive D] (S : CategoryTheory.ShortComplex D) [CategoryTheory.HasRightDual S.X₃] : CategoryTheory.ShortComplex D

The unit-form extension: the given sequence, internally hommed and pulled back along the name of the identity, now with unit quotient.

Equations

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

theorem RS.unitFormIn_fst {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Abelian D] [CategoryTheory.MonoidalPreadditive D] (S : CategoryTheory.ShortComplex D) [CategoryTheory.HasRightDual S.X₃] : CategoryTheory.CategoryStruct.comp (unitFormIn S) (CategoryTheory.Limits.pullback.fst (CategoryTheory.MonoidalCategoryStruct.whiskerLeft S.X₃ᘁ S.g) (unitName S.X₃)) = CategoryTheory.MonoidalCategoryStruct.whiskerLeft S.X₃ᘁ S.f

Defining square of the inclusion.

theorem RS.unitForm_shortExact {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Abelian D] [CategoryTheory.MonoidalPreadditive D] (S : CategoryTheory.ShortComplex D) [CategoryTheory.HasRightDual S.X₃] [CategoryTheory.HasLeftDual S.X₃ᘁ] [CategoryTheory.HasRightDual S.X₃ᘁ] (hS : S.ShortExact) : (unitForm S).ShortExact

The unit-form extension is short exact: the pullback of a short exact sequence along a point of its quotient.

theorem RS.mono_rightAdjointMate {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {X Y : D} [CategoryTheory.HasRightDual X] [CategoryTheory.HasRightDual Y] [∀ (W : D), (CategoryTheory.MonoidalCategory.tensorLeft W).PreservesEpimorphisms] (f : X ⟶ Y) (hf : CategoryTheory.Epi f) : CategoryTheory.Mono (fᘁ)

Epimorphisms dualise to monomorphisms: the right adjoint mate of an epimorphism is monic.

noncomputable def RS.unitDualIso {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ≅ (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)ᘁ

The dual of the unit, canonically.

Equations

• RS.unitDualIso = CategoryTheory.rightDualIso CategoryTheory.exactPairingUnit inferInstance

noncomputable def RS.unitFormPoint {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Abelian D] [CategoryTheory.MonoidalPreadditive D] (S : CategoryTheory.ShortComplex D) [CategoryTheory.HasRightDual S.X₃] [CategoryTheory.HasRightDual (unitFormMid S)] : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ (unitFormMid S)ᘁ

The monic point of the dual: the unit-form quotient, dualised into a point of the dual of the middle object.

Equations

• RS.unitFormPoint S = CategoryTheory.CategoryStruct.comp RS.unitDualIso.hom ((RS.unitForm S).gᘁ)

theorem RS.mono_unitFormPoint {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Abelian D] [CategoryTheory.MonoidalPreadditive D] (S : CategoryTheory.ShortComplex D) [CategoryTheory.HasRightDual S.X₃] [CategoryTheory.HasRightDual (unitFormMid S)] [CategoryTheory.HasLeftDual S.X₃ᘁ] [CategoryTheory.HasRightDual S.X₃ᘁ] [∀ (W : D), (CategoryTheory.MonoidalCategory.tensorLeft W).PreservesEpimorphisms] (hS : S.ShortExact) : CategoryTheory.Mono (unitFormPoint S)

The point is monic when the sequence is short exact.

theorem RS.coevaluation_unitDualIso_inv {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] : CategoryTheory.CategoryStruct.comp (η_ (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)ᘁ) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) unitDualIso.inv) = (CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).inv

The coevaluation meets the canonical unit-dual inverse as the unit pairing's coevaluation.

noncomputable def RS.pointSection {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Abelian D] (S : CategoryTheory.ShortComplex D) [CategoryTheory.HasRightDual S.X₃] [CategoryTheory.HasRightDual (unitFormMid S)] (B : D) (cls : (unitFormMid S)ᘁ ⟶ B) : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (unitFormMid S) B

The point section: the coevaluation, carried through a class of the dual of the middle object.

Equations

• RS.pointSection S B cls = CategoryTheory.CategoryStruct.comp (η_ (RS.unitFormMid S) (RS.unitFormMid S)ᘁ) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (RS.unitFormMid S) cls)

theorem RS.coevaluation_unitFormPoint {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Abelian D] [CategoryTheory.MonoidalPreadditive D] (S : CategoryTheory.ShortComplex D) [CategoryTheory.HasRightDual S.X₃] [CategoryTheory.HasRightDual (unitFormMid S)] : CategoryTheory.CategoryStruct.comp (η_ (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)ᘁ) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) (CategoryTheory.CategoryStruct.comp unitDualIso.inv (unitFormPoint S))) = CategoryTheory.CategoryStruct.comp (η_ (unitFormMid S) (unitFormMid S)ᘁ) (CategoryTheory.MonoidalCategoryStruct.whiskerRight (unitForm S).g (unitFormMid S)ᘁ)

The coevaluation carries the quotient onto the point, through the canonical unit-dual identification.

theorem RS.pointSection_section {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Abelian D] [CategoryTheory.MonoidalPreadditive D] (S : CategoryTheory.ShortComplex D) [CategoryTheory.HasRightDual S.X₃] [CategoryTheory.HasRightDual (unitFormMid S)] (B : D) [CategoryTheory.MonObj B] (cls : (unitFormMid S)ᘁ ⟶ B) (hcls : CategoryTheory.CategoryStruct.comp (unitFormPoint S) cls = CategoryTheory.MonObj.one) : CategoryTheory.CategoryStruct.comp (pointSection S B cls) (CategoryTheory.MonoidalCategoryStruct.whiskerRight (unitForm S).g B) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).inv (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) CategoryTheory.MonObj.one)

The section property of the point section: against the unit-form quotient, a class restricting on the point to the unit of the algebra yields the unit itself.

noncomputable def RS.freeSectionHom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Abelian D] (S : CategoryTheory.ShortComplex D) [CategoryTheory.HasRightDual S.X₃] [CategoryTheory.HasRightDual (unitFormMid S)] (B : D) [CategoryTheory.MonObj B] (cls : (unitFormMid S)ᘁ ⟶ B) : CategoryTheory.MonoidalCategoryStruct.tensorObj B (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj B (unitFormMid S)

The free section carrier: the point section, folded into the free module through the multiplication.

Equations

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

theorem RS.freeSectionHom_section {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Abelian D] [CategoryTheory.MonoidalPreadditive D] (S : CategoryTheory.ShortComplex D) [CategoryTheory.HasRightDual S.X₃] [CategoryTheory.HasRightDual (unitFormMid S)] (B : D) [CategoryTheory.MonObj B] (cls : (unitFormMid S)ᘁ ⟶ B) (hcls : CategoryTheory.CategoryStruct.comp (unitFormPoint S) cls = CategoryTheory.MonObj.one) : CategoryTheory.CategoryStruct.comp (freeSectionHom S B cls) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (unitForm S).g) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj B (CategoryTheory.MonoidalCategoryStruct.tensorUnit D))

The free section splits the quotient: when the class restricts on the point to the unit, the free section carrier is a section of the whiskered quotient.

noncomputable def RS.freeModExtend {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (B : D) [CategoryTheory.MonObj B] {V : D} (M : CategoryTheory.Mod D B) (q : V ⟶ M.X) : freeMod B V ⟶ M

Extend a point to the free module: any morphism into the carrier of a module extends to a linear map from the free module, through the action.

Equations

• RS.freeModExtend B M q = CategoryTheory.Mod.Hom.mk' (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B q) (RS.actLeft B M.X)) ⋯

noncomputable def RS.freeSection {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Abelian D] (S : CategoryTheory.ShortComplex D) [CategoryTheory.HasRightDual S.X₃] [CategoryTheory.HasRightDual (unitFormMid S)] (B : D) [CategoryTheory.MonObj B] (cls : (unitFormMid S)ᘁ ⟶ B) : freeMod B (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) ⟶ freeMod B (unitFormMid S)

The free section: the point section, braided and extended to the free module.

Equations

• RS.freeSection S B cls = RS.freeModExtend B (RS.freeMod B (RS.unitFormMid S)) (CategoryTheory.CategoryStruct.comp (RS.pointSection S B cls) (β_ (RS.unitFormMid S) B).hom)

theorem RS.freeSection_hom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Abelian D] (S : CategoryTheory.ShortComplex D) [CategoryTheory.HasRightDual S.X₃] [CategoryTheory.HasRightDual (unitFormMid S)] (B : D) [CategoryTheory.MonObj B] (cls : (unitFormMid S)ᘁ ⟶ B) : (freeSection S B cls).hom = freeSectionHom S B cls

The free section's carrier is the folded point section.

noncomputable def RS.evalContract {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (X W : D) [CategoryTheory.HasRightDual X] : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj Xᘁ W) X ⟶ W

Contract the dual against the argument: braid the payload out and evaluate.

Equations

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

theorem RS.evalContract_natural {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (X : D) [CategoryTheory.HasRightDual X] {W W' : D} (h : W ⟶ W') : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Xᘁ h) X) (evalContract X W') = CategoryTheory.CategoryStruct.comp (evalContract X W) h

The contraction is natural in the payload.

theorem RS.unitName_evalContract {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (X : D) [CategoryTheory.HasRightDual X] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (unitName X) X) (evalContract X X) = (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom

The zigzag of the name: the name of the identity, contracted against the argument, is the unitor.

noncomputable def RS.freeSectionPoint {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Abelian D] (S : CategoryTheory.ShortComplex D) [CategoryTheory.HasRightDual S.X₃] [CategoryTheory.HasRightDual (unitFormMid S)] (B : D) [CategoryTheory.MonObj B] (cls : (unitFormMid S)ᘁ ⟶ B) : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj B (CategoryTheory.MonoidalCategoryStruct.tensorObj S.X₃ᘁ S.X₂)

The element of the free section: the unit, pushed through the free section and out of the pullback.

Equations

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

theorem RS.freeSectionPoint_g {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Abelian D] [CategoryTheory.MonoidalPreadditive D] (S : CategoryTheory.ShortComplex D) [CategoryTheory.HasRightDual S.X₃] [CategoryTheory.HasRightDual (unitFormMid S)] (B : D) [CategoryTheory.MonObj B] (cls : (unitFormMid S)ᘁ ⟶ B) (hcls : CategoryTheory.CategoryStruct.comp (unitFormPoint S) cls = CategoryTheory.MonObj.one) : CategoryTheory.CategoryStruct.comp (freeSectionPoint S B cls) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (CategoryTheory.MonoidalCategoryStruct.whiskerLeft S.X₃ᘁ S.g)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (unitName S.X₃)))

The element carries the internal quotient onto the name.

noncomputable def RS.sectionPoint {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Abelian D] (S : CategoryTheory.ShortComplex D) [CategoryTheory.HasRightDual S.X₃] [CategoryTheory.HasRightDual (unitFormMid S)] (B : D) [CategoryTheory.MonObj B] (cls : (unitFormMid S)ᘁ ⟶ B) : S.X₃ ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj B S.X₂

The transferred point: the free-section element, contracted against the argument.

Equations

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

theorem RS.sectionPoint_g {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Abelian D] [CategoryTheory.MonoidalPreadditive D] (S : CategoryTheory.ShortComplex D) [CategoryTheory.HasRightDual S.X₃] [CategoryTheory.HasRightDual (unitFormMid S)] (B : D) [CategoryTheory.MonObj B] (cls : (unitFormMid S)ᘁ ⟶ B) (hcls : CategoryTheory.CategoryStruct.comp (unitFormPoint S) cls = CategoryTheory.MonObj.one) : CategoryTheory.CategoryStruct.comp (sectionPoint S B cls) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B S.g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor S.X₃).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one S.X₃)

The transferred point splits the quotient: against the quotient it is the unit against the argument.

noncomputable def RS.rappel210Section {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Abelian D] (S : CategoryTheory.ShortComplex D) [CategoryTheory.HasRightDual S.X₃] [CategoryTheory.HasRightDual (unitFormMid S)] (B : D) [CategoryTheory.MonObj B] (cls : (unitFormMid S)ᘁ ⟶ B) : freeMod B S.X₃ ⟶ freeMod B S.X₂

The section of the statement of record: the transferred point, extended to the free module.

Equations

• RS.rappel210Section S B cls = RS.freeModExtend B (RS.freeMod B S.X₂) (RS.sectionPoint S B cls)

theorem RS.rappel210Section_splits {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Abelian D] [CategoryTheory.MonoidalPreadditive D] (S : CategoryTheory.ShortComplex D) [CategoryTheory.HasRightDual S.X₃] [CategoryTheory.HasRightDual (unitFormMid S)] (B : D) [CategoryTheory.MonObj B] (cls : (unitFormMid S)ᘁ ⟶ B) (hcls : CategoryTheory.CategoryStruct.comp (unitFormPoint S) cls = CategoryTheory.MonObj.one) : CategoryTheory.CategoryStruct.comp (rappel210Section S B cls) (freeModMap B S.g) = CategoryTheory.CategoryStruct.id (freeMod B S.X₃)

The section splits the base-changed epimorphism.

theorem RS.rappel210_of_class {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Abelian D] [CategoryTheory.MonoidalPreadditive D] (S : CategoryTheory.ShortComplex D) [CategoryTheory.HasRightDual S.X₃] [CategoryTheory.HasRightDual (unitFormMid S)] (hS : S.ShortExact) (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (hnz : CategoryTheory.MonObj.one ≠ 0) (cls : (unitFormMid S)ᘁ ⟶ B) (hcls : CategoryTheory.CategoryStruct.comp (unitFormPoint S) cls = CategoryTheory.MonObj.one) : Rappel210Statement S hS

The local splitting statement holds given a unital class on the dual of the unit-form middle object: the full reduction.