Atlas.TensorCategories.code.TensorExact

source

instance CategoryTheory.tensorLeft_preservesLimitsOfSize {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [RigidCategory C] (X : C) :

Limits.PreservesLimitsOfSize.{v, v, v, v, u, u} (MonoidalCategory.tensorLeft X)

In a rigid category, the left-tensor functor X ⊗ - preserves all limits, as it is the right adjoint of Xᘁ ⊗ -.

source

instance CategoryTheory.tensorLeft_preservesColimitsOfSize {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [RigidCategory C] (X : C) :

Limits.PreservesColimitsOfSize.{v, v, v, v, u, u} (MonoidalCategory.tensorLeft X)

In a rigid category, the left-tensor functor X ⊗ - preserves all colimits, as it is the left adjoint of ᘁX ⊗ -.

source

instance CategoryTheory.tensorLeft_preservesFiniteLimits {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [RigidCategory C] (X : C) :

Limits.PreservesFiniteLimits (MonoidalCategory.tensorLeft X)

The left-tensor functor X ⊗ - in a rigid category preserves finite limits.

source

instance CategoryTheory.tensorLeft_preservesFiniteColimits {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [RigidCategory C] (X : C) :

Limits.PreservesFiniteColimits (MonoidalCategory.tensorLeft X)

The left-tensor functor X ⊗ - in a rigid category preserves finite colimits.

source

instance CategoryTheory.tensorRight_preservesLimitsOfSize {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [RigidCategory C] (X : C) :

Limits.PreservesLimitsOfSize.{v, v, v, v, u, u} (MonoidalCategory.tensorRight X)

In a rigid category, the right-tensor functor - ⊗ X preserves all limits, as it is the right adjoint of - ⊗ ᘁX.

source

instance CategoryTheory.tensorRight_preservesColimitsOfSize {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [RigidCategory C] (X : C) :

Limits.PreservesColimitsOfSize.{v, v, v, v, u, u} (MonoidalCategory.tensorRight X)

In a rigid category, the right-tensor functor - ⊗ X preserves all colimits, as it is the left adjoint of - ⊗ Xᘁ.

source

instance CategoryTheory.tensorRight_preservesFiniteLimits {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [RigidCategory C] (X : C) :

Limits.PreservesFiniteLimits (MonoidalCategory.tensorRight X)

The right-tensor functor - ⊗ X in a rigid category preserves finite limits.

source

instance CategoryTheory.tensorRight_preservesFiniteColimits {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [RigidCategory C] (X : C) :

Limits.PreservesFiniteColimits (MonoidalCategory.tensorRight X)

The right-tensor functor - ⊗ X in a rigid category preserves finite colimits.

source

noncomputable def CategoryTheory.tensorLeft_exact {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [RigidCategory C] (X : C) :

exactFunctor C C (MonoidalCategory.tensorLeft X)

The left-tensor functor X ⊗ - in a rigid category is exact, packaged as an exactFunctor.

Instances For

source

noncomputable def CategoryTheory.tensorRight_exact {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [RigidCategory C] (X : C) :

exactFunctor C C (MonoidalCategory.tensorRight X)

The right-tensor functor - ⊗ X in a rigid category is exact, packaged as an exactFunctor.

Instances For

source

theorem CategoryTheory.tensor_biexact {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [RigidCategory C] (X : C) :

exactFunctor C C (MonoidalCategory.tensorLeft X) ∧ exactFunctor C C (MonoidalCategory.tensorRight X)

In a rigid category, both X ⊗ - and - ⊗ X are exact functors.

source

theorem CategoryTheory.proposition_1_13_1 {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [RigidCategory C] (X : C) :

exactFunctor C C (MonoidalCategory.tensorLeft X) ∧ exactFunctor C C (MonoidalCategory.tensorRight X)

Proposition 1.13.1: in a rigid monoidal category, both left and right tensoring with any object are exact functors.

source

noncomputable def CategoryTheory.rightDualizationFunctor {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [RigidCategory C] :

Functor Cᵒᵖ C

The right dualization functor Cᵒᵖ ⥤ C sending X ↦ Xᘁ and a morphism to its right adjoint mate.

Instances For

source

noncomputable def CategoryTheory.leftDualizationFunctor {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [RigidCategory C] :

Functor Cᵒᵖ C

The left dualization functor Cᵒᵖ ⥤ C sending X ↦ ᘁX and a morphism to its left adjoint mate.

Instances For

source

noncomputable def CategoryTheory.rightAdjointMateEquiv {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [RigidCategory C] (X Y : C) :

(X ⟶ Y) ≃ (Yᘁ ⟶ Xᘁ)

The right adjoint mate is a bijection Hom(X, Y) ≃ Hom(Yᘁ, Xᘁ) induced by the rigid structure.

Instances For

source

theorem CategoryTheory.rightAdjointMateEquiv_apply {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [RigidCategory C] (X Y : C) (f : X ⟶ Y) :

(rightAdjointMateEquiv X Y) f = fᘁ

Computation: rightAdjointMateEquiv applied to f agrees with the underlying right adjoint mate.

source

noncomputable def CategoryTheory.leftAdjointMateEquiv {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [RigidCategory C] (X Y : C) :

(X ⟶ Y) ≃ (ᘁY ⟶ ᘁX)

The left adjoint mate is a bijection Hom(X, Y) ≃ Hom(ᘁY, ᘁX) induced by the rigid structure.

Instances For

source

theorem CategoryTheory.leftAdjointMateEquiv_apply {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [RigidCategory C] (X Y : C) (f : X ⟶ Y) :

(leftAdjointMateEquiv X Y) f = ᘁf

Computation: leftAdjointMateEquiv applied to f agrees with the underlying left adjoint mate.

source

instance CategoryTheory.rightDualizationFunctor_faithful {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [RigidCategory C] :

rightDualizationFunctor.Faithful

The right dualization functor Cᵒᵖ ⥤ C is faithful, as the right adjoint mate is injective.

source

instance CategoryTheory.rightDualizationFunctor_full {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [RigidCategory C] :

rightDualizationFunctor.Full

The right dualization functor Cᵒᵖ ⥤ C is full, as the right adjoint mate is surjective.

source

instance CategoryTheory.rightDualizationFunctor_essSurj {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [RigidCategory C] :

rightDualizationFunctor.EssSurj

The right dualization functor Cᵒᵖ ⥤ C is essentially surjective: every Z is (ᘁZ)ᘁ.

source

instance CategoryTheory.rightDualizationFunctor_isEquivalence {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [RigidCategory C] :

rightDualizationFunctor.IsEquivalence

The right dualization functor Cᵒᵖ ⥤ C is an equivalence of categories.

source

instance CategoryTheory.rightDualizationFunctor_preservesLimits {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [RigidCategory C] :

Limits.PreservesLimitsOfSize.{v, v, v, v, u, u} rightDualizationFunctor

The right dualization functor preserves all limits, since it is an equivalence.

source

instance CategoryTheory.rightDualizationFunctor_preservesColimits {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [RigidCategory C] :

Limits.PreservesColimitsOfSize.{v, v, v, v, u, u} rightDualizationFunctor

The right dualization functor preserves all colimits, since it is an equivalence.

source

instance CategoryTheory.rightDualizationFunctor_preservesFiniteLimits {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [RigidCategory C] :

Limits.PreservesFiniteLimits rightDualizationFunctor

The right dualization functor preserves finite limits.

source

instance CategoryTheory.rightDualizationFunctor_preservesFiniteColimits {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [RigidCategory C] :

Limits.PreservesFiniteColimits rightDualizationFunctor

The right dualization functor preserves finite colimits.

source

instance CategoryTheory.leftDualizationFunctor_faithful {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [RigidCategory C] :

leftDualizationFunctor.Faithful

The left dualization functor Cᵒᵖ ⥤ C is faithful, as the left adjoint mate is injective.

source

instance CategoryTheory.leftDualizationFunctor_full {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [RigidCategory C] :

leftDualizationFunctor.Full

The left dualization functor Cᵒᵖ ⥤ C is full, as the left adjoint mate is surjective.

source

instance CategoryTheory.leftDualizationFunctor_essSurj {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [RigidCategory C] :

leftDualizationFunctor.EssSurj

The left dualization functor Cᵒᵖ ⥤ C is essentially surjective: every Z is ᘁ(Zᘁ).

source

instance CategoryTheory.leftDualizationFunctor_isEquivalence {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [RigidCategory C] :

leftDualizationFunctor.IsEquivalence

The left dualization functor Cᵒᵖ ⥤ C is an equivalence of categories.

source

instance CategoryTheory.leftDualizationFunctor_preservesLimits {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [RigidCategory C] :

Limits.PreservesLimitsOfSize.{v, v, v, v, u, u} leftDualizationFunctor

The left dualization functor preserves all limits, since it is an equivalence.

source

instance CategoryTheory.leftDualizationFunctor_preservesColimits {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [RigidCategory C] :

Limits.PreservesColimitsOfSize.{v, v, v, v, u, u} leftDualizationFunctor

The left dualization functor preserves all colimits, since it is an equivalence.

source

instance CategoryTheory.leftDualizationFunctor_preservesFiniteLimits {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [RigidCategory C] :

Limits.PreservesFiniteLimits leftDualizationFunctor

The left dualization functor preserves finite limits.

source

instance CategoryTheory.leftDualizationFunctor_preservesFiniteColimits {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [RigidCategory C] :

Limits.PreservesFiniteColimits leftDualizationFunctor

The left dualization functor preserves finite colimits.

source

noncomputable def CategoryTheory.rightDualizationFunctor_exact {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [RigidCategory C] :

exactFunctor Cᵒᵖ C rightDualizationFunctor

The right dualization functor Cᵒᵖ ⥤ C is exact, packaged as an exactFunctor.

Instances For

source

noncomputable def CategoryTheory.leftDualizationFunctor_exact {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [RigidCategory C] :

exactFunctor Cᵒᵖ C leftDualizationFunctor

The left dualization functor Cᵒᵖ ⥤ C is exact, packaged as an exactFunctor.

Instances For

source

theorem CategoryTheory.dualization_exact {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [RigidCategory C] :

exactFunctor Cᵒᵖ C rightDualizationFunctor ∧ exactFunctor Cᵒᵖ C leftDualizationFunctor

Both dualization functors Cᵒᵖ ⥤ C are exact in a rigid category.

source

theorem CategoryTheory.prop_1_13_5 {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [RigidCategory C] :

exactFunctor Cᵒᵖ C rightDualizationFunctor ∧ exactFunctor Cᵒᵖ C leftDualizationFunctor

Proposition 1.13.5: in a rigid monoidal category, both dualization functors Cᵒᵖ ⥤ C are exact.