Opposites of morphism ideals

Taking opposites reverses every morphism in a two-sided ideal. This operation is involutive, and the quotient by the opposite ideal is canonically equivalent to the opposite of the quotient. The equivalence identifies the class of an opposite morphism with the opposite of its class.

This lets constructions expressed as additive ideal quotients pass between a category and its opposite. In particular, stable quotients defined using projective objects can be compared with the corresponding quotients defined using injective objects on the opposite category.

Main definitions

• TauCeti.MorphismIdeal.op: the opposite of a morphism ideal.
• TauCeti.MorphismIdeal.unop: the inverse operation on ideals of an opposite category.
• TauCeti.MorphismIdeal.opQuotientFunctor: the canonical functor from the quotient by the opposite ideal to the opposite quotient.
• TauCeti.MorphismIdeal.opQuotientEquivalence: the resulting equivalence of categories.

References

• D. Happel, Triangulated Categories in the Representation Theory of Finite Dimensional Algebras, LMS Lecture Note Series 119, CUP (1988), Section I.2.

def TauCeti.MorphismIdeal.op {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : MorphismIdeal C) : MorphismIdeal Cᵒᵖ

The opposite ideal: a morphism of Cᵒᵖ belongs to I.op when its unopposite belongs to I.

Equations

• I.op = { hom := fun (X Y : Cᵒᵖ) => AddSubgroup.comap (CategoryTheory.unopHom X Y) (I.hom (Opposite.unop Y) (Opposite.unop X)), comp_mem_left := ⋯, comp_mem_right := ⋯ }

@[simp]

theorem TauCeti.MorphismIdeal.mem_op_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : MorphismIdeal C) {X Y : Cᵒᵖ} (f : X ⟶ Y) : f ∈ I.op.hom X Y ↔ f.unop ∈ I.hom (Opposite.unop Y) (Opposite.unop X)

A morphism belongs to the opposite ideal exactly when its unopposite belongs to the original ideal.

def TauCeti.MorphismIdeal.unop {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : MorphismIdeal Cᵒᵖ) : MorphismIdeal C

Unopposite an ideal on an opposite category.

Equations

• I.unop = { hom := fun (X Y : C) => AddSubgroup.comap (CategoryTheory.opHom X Y) (I.hom (Opposite.op Y) (Opposite.op X)), comp_mem_left := ⋯, comp_mem_right := ⋯ }

@[simp]

theorem TauCeti.MorphismIdeal.mem_unop_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : MorphismIdeal Cᵒᵖ) {X Y : C} (f : X ⟶ Y) : f ∈ I.unop.hom X Y ↔ f.op ∈ I.hom (Opposite.op Y) (Opposite.op X)

A morphism belongs to the unopposite ideal exactly when its opposite belongs to the original ideal.

@[simp]

theorem TauCeti.MorphismIdeal.op_unop {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : MorphismIdeal Cᵒᵖ) : I.unop.op = I

Taking the opposite and then the unopposite of an ideal recovers the ideal.

@[simp]

theorem TauCeti.MorphismIdeal.unop_op {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : MorphismIdeal C) : I.op.unop = I

Taking the unopposite and then the opposite of an ideal recovers the ideal.

theorem TauCeti.MorphismIdeal.op_injective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] : Function.Injective op

Taking opposites is injective on morphism ideals.

theorem TauCeti.MorphismIdeal.unop_injective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] : Function.Injective unop

Taking unopposites is injective on morphism ideals.

theorem TauCeti.MorphismIdeal.op_monotone {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] : Monotone op

Taking opposites preserves inclusions of morphism ideals.

theorem TauCeti.MorphismIdeal.unop_monotone {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] : Monotone unop

Taking unopposites preserves inclusions of morphism ideals.

@[simp]

theorem TauCeti.MorphismIdeal.op_le_op_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {I J : MorphismIdeal C} : I.op ≤ J.op ↔ I ≤ J

Inclusion of opposite ideals is equivalent to inclusion of the original ideals.

@[simp]

theorem TauCeti.MorphismIdeal.unop_le_unop_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {I J : MorphismIdeal Cᵒᵖ} : I.unop ≤ J.unop ↔ I ≤ J

Inclusion of unopposite ideals is equivalent to inclusion of the original ideals.

@[simp]

theorem TauCeti.MorphismIdeal.op_rel_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : MorphismIdeal C) {X Y : Cᵒᵖ} {f g : X ⟶ Y} : I.op.rel f g ↔ I.rel f.unop g.unop

Congruence modulo the opposite ideal is congruence modulo the original ideal after taking unopposites.

@[simp]

theorem TauCeti.MorphismIdeal.unop_rel_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : MorphismIdeal Cᵒᵖ) {X Y : C} {f g : X ⟶ Y} : I.unop.rel f g ↔ I.rel f.op g.op

Congruence modulo an unopposite ideal is congruence modulo the original ideal after taking opposites.

noncomputable def TauCeti.MorphismIdeal.opQuotientFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : MorphismIdeal C) : CategoryTheory.Functor I.op.Quotient I.Quotientᵒᵖ

The canonical functor from the quotient by the opposite ideal to the opposite of the quotient. It sends the class of f to the opposite of the class of f.unop.

Equations

• I.opQuotientFunctor = I.op.lift I.quotientFunctor.op ⋯

theorem TauCeti.MorphismIdeal.opQuotientFunctor_eq_lift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : MorphismIdeal C) (h : I.op ≤ I.quotientFunctor.op.kerIdeal) : I.opQuotientFunctor = I.op.lift I.quotientFunctor.op h

The opposite-quotient comparison is the lift of the opposite quotient functor. Any proof that this functor kills the opposite ideal gives the same lift.

@[simp]

theorem TauCeti.MorphismIdeal.opQuotientFunctor_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : MorphismIdeal C) (X : Cᵒᵖ) : I.opQuotientFunctor.obj (I.op.quotientFunctor.obj X) = Opposite.op (I.quotientFunctor.obj (Opposite.unop X))

The canonical opposite-quotient functor sends the class of an object to the opposite of the class of its unopposite.

@[simp]

theorem TauCeti.MorphismIdeal.opQuotientFunctor_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : MorphismIdeal C) {X Y : Cᵒᵖ} (f : X ⟶ Y) : I.opQuotientFunctor.map (I.op.quotientFunctor.map f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (I.quotientFunctor.map f.unop).op (CategoryTheory.eqToHom ⋯))

The canonical opposite-quotient functor has the expected value on a representative.

instance TauCeti.MorphismIdeal.instFaithfulQuotientOppositeOpOpQuotientFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : MorphismIdeal C) : I.opQuotientFunctor.Faithful

instance TauCeti.MorphismIdeal.instFullQuotientOppositeOpOpQuotientFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : MorphismIdeal C) : I.opQuotientFunctor.Full

instance TauCeti.MorphismIdeal.instEssSurjQuotientOppositeOpOpQuotientFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : MorphismIdeal C) : I.opQuotientFunctor.EssSurj

instance TauCeti.MorphismIdeal.instAdditiveQuotientOppositeOpOpQuotientFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : MorphismIdeal C) : I.opQuotientFunctor.Additive

instance TauCeti.MorphismIdeal.instIsEquivalenceQuotientOppositeOpOpQuotientFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : MorphismIdeal C) : I.opQuotientFunctor.IsEquivalence

theorem TauCeti.MorphismIdeal.isEquivalence_op_lift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : MorphismIdeal C) (J : MorphismIdeal Cᵒᵖ) (hJ : J = I.op) (h : J ≤ I.quotientFunctor.op.kerIdeal) : (J.lift I.quotientFunctor.op h).IsEquivalence

Lifting the opposite quotient functor gives an equivalence whenever the source ideal is the opposite ideal. This formulation permits a different presentation of the source ideal.

noncomputable def TauCeti.MorphismIdeal.opQuotientEquivalence {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : MorphismIdeal C) : I.op.Quotient ≌ I.Quotientᵒᵖ

Quotienting the opposite category by the opposite ideal is canonically equivalent to taking the opposite of the quotient category.

Equations

• I.opQuotientEquivalence = I.opQuotientFunctor.asEquivalence

@[simp]

theorem TauCeti.MorphismIdeal.opQuotientEquivalence_functor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : MorphismIdeal C) : I.opQuotientEquivalence.functor = I.opQuotientFunctor

The functor of the canonical opposite-quotient equivalence is the opposite-quotient functor.

instance TauCeti.MorphismIdeal.instAdditiveQuotientOppositeOpFunctorOpQuotientEquivalence {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : MorphismIdeal C) : I.opQuotientEquivalence.functor.Additive