Adjoint quadruples

This file concerns adjoint quadruples L ⊣ F ⊣ G ⊣ R of functors L G : C ⥤ D, F R : D ⥤ C. We bundle the adjunctions in a structure Quadruple L F G R and make the two triples Triple L F G and Triple F G R accessible as Quadruple.leftTriple and Quadruple.rightTriple.

Currently the only two results are the following:

• When F and R are fully faithful, the components of the induced natural transformation G ⟶ L are epimorphisms iff the components of the natural transformation F ⟶ R are monomorphisms.
• When L and G are fully faithful, the components of the induced natural transformation L ⟶ G are epimorphisms iff the components of the natural transformation R ⟶ F are monomorphisms. This is in particular relevant for the adjoint quadruples π₀ ⊣ disc ⊣ Γ ⊣ codisc that appear in cohesive topoi, and can be found e.g. as proposition 2.7 here.

Note that by Triple.fullyFaithfulEquiv, in an adjoint quadruple L ⊣ F ⊣ G ⊣ R L is fully faithful iff G is and F is fully faithful iff R is; these lemmas thus cover all cases in which some of the functors are fully faithful. We opt to include only those typeclass assumptions that are needed for the theorem statements, so some lemmas require only e.g. F to be fully faithful when really this means F and R both must be.

structure CategoryTheory.Adjunction.Quadruple {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (L : Functor C D) (F : Functor D C) (G : Functor C D) (R : Functor D C) : Type (max (max (max u₁ u₂) v₁) v₂)

Structure containing the three adjunctions of an adjoint quadruple L ⊣ F ⊣ G ⊣ R.

• adj₁ : L ⊣ F

  Adjunction L ⊣ F of the adjoint quadruple L ⊣ F ⊣ G ⊣ R.

• adj₂ : F ⊣ G

  Adjunction F ⊣ G of the adjoint quadruple L ⊣ F ⊣ G ⊣ R.

• adj₃ : G ⊣ R

  Adjunction G ⊣ R of the adjoint quadruple L ⊣ F ⊣ G ⊣ R.

def CategoryTheory.Adjunction.Quadruple.leftTriple {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {L : Functor C D} {F : Functor D C} {G : Functor C D} {R : Functor D C} (q : Quadruple L F G R) : Triple L F G

The left part of an adjoint quadruple L ⊣ F ⊣ G ⊣ R.

Equations

• q.leftTriple = { adj₁ := q.adj₁, adj₂ := q.adj₂ }

@[simp]

theorem CategoryTheory.Adjunction.Quadruple.leftTriple_adj₁ {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {L : Functor C D} {F : Functor D C} {G : Functor C D} {R : Functor D C} (q : Quadruple L F G R) : q.leftTriple.adj₁ = q.adj₁

@[simp]

theorem CategoryTheory.Adjunction.Quadruple.leftTriple_adj₂ {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {L : Functor C D} {F : Functor D C} {G : Functor C D} {R : Functor D C} (q : Quadruple L F G R) : q.leftTriple.adj₂ = q.adj₂

def CategoryTheory.Adjunction.Quadruple.rightTriple {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {L : Functor C D} {F : Functor D C} {G : Functor C D} {R : Functor D C} (q : Quadruple L F G R) : Triple F G R

The right part of an adjoint quadruple L ⊣ F ⊣ G ⊣ R.

Equations

• q.rightTriple = { adj₁ := q.adj₂, adj₂ := q.adj₃ }

@[simp]

theorem CategoryTheory.Adjunction.Quadruple.rightTriple_adj₂ {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {L : Functor C D} {F : Functor D C} {G : Functor C D} {R : Functor D C} (q : Quadruple L F G R) : q.rightTriple.adj₂ = q.adj₃

@[simp]

theorem CategoryTheory.Adjunction.Quadruple.rightTriple_adj₁ {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {L : Functor C D} {F : Functor D C} {G : Functor C D} {R : Functor D C} (q : Quadruple L F G R) : q.rightTriple.adj₁ = q.adj₂

def CategoryTheory.Adjunction.Quadruple.op {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {L : Functor C D} {F : Functor D C} {G : Functor C D} {R : Functor D C} (q : Quadruple L F G R) : Quadruple R.op G.op F.op L.op

The adjoint quadruple R.op ⊣ G.op ⊣ F.op ⊣ L.op dual to an adjoint quadruple L ⊣ F ⊣ G ⊣ R.

Equations

• q.op = { adj₁ := q.adj₃.op, adj₂ := q.adj₂.op, adj₃ := q.adj₁.op }

@[simp]

theorem CategoryTheory.Adjunction.Quadruple.op_adj₃ {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {L : Functor C D} {F : Functor D C} {G : Functor C D} {R : Functor D C} (q : Quadruple L F G R) : q.op.adj₃ = q.adj₁.op

@[simp]

theorem CategoryTheory.Adjunction.Quadruple.op_adj₂ {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {L : Functor C D} {F : Functor D C} {G : Functor C D} {R : Functor D C} (q : Quadruple L F G R) : q.op.adj₂ = q.adj₂.op

@[simp]

theorem CategoryTheory.Adjunction.Quadruple.op_adj₁ {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {L : Functor C D} {F : Functor D C} {G : Functor C D} {R : Functor D C} (q : Quadruple L F G R) : q.op.adj₁ = q.adj₃.op

@[simp]

theorem CategoryTheory.Adjunction.Quadruple.op_leftTriple {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {L : Functor C D} {F : Functor D C} {G : Functor C D} {R : Functor D C} (q : Quadruple L F G R) : q.op.leftTriple = q.rightTriple.op

@[simp]

theorem CategoryTheory.Adjunction.Quadruple.op_rightTriple {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {L : Functor C D} {F : Functor D C} {G : Functor C D} {R : Functor D C} (q : Quadruple L F G R) : q.op.rightTriple = q.leftTriple.op

theorem CategoryTheory.Adjunction.Quadruple.epi_leftTriple_rightToLeft_app_iff_mono_rightTriple_leftToRight_app {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {L : Functor C D} {F : Functor D C} {G : Functor C D} {R : Functor D C} (q : Quadruple L F G R) [F.Full] [F.Faithful] : (∀ (X : C), Epi (q.leftTriple.rightToLeft.app X)) ↔ ∀ (X : D), Mono (q.rightTriple.leftToRight.app X)

For an adjoint quadruple L ⊣ F ⊣ G ⊣ R where F (and hence also R) is fully faithful, all components of the natural transformation G ⟶ L are epimorphisms iff all components of the natural transformation F ⟶ R are monomorphisms.

theorem CategoryTheory.Adjunction.Quadruple.epi_leftTriple_rightToLeft_iff_mono_rightTriple_leftToRight {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {L : Functor C D} {F : Functor D C} {G : Functor C D} {R : Functor D C} (q : Quadruple L F G R) [F.Full] [F.Faithful] [Limits.HasPullbacks C] [Limits.HasPushouts D] : Epi q.leftTriple.rightToLeft ↔ Mono q.rightTriple.leftToRight

For an adjoint quadruple L ⊣ F ⊣ G ⊣ R where F (and hence also R) is fully faithful and its domain / codomain has all pushouts resp. pullbacks, the natural transformation G ⟶ L is an epimorphism iff the natural transformation F ⟶ R is a monomorphism.

theorem CategoryTheory.Adjunction.Quadruple.epi_leftTriple_leftToRight_app_iff_mono_rightTriple_rightToLeft_app {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {L : Functor C D} {F : Functor D C} {G : Functor C D} {R : Functor D C} (q : Quadruple L F G R) [L.Full] [L.Faithful] [G.Full] [G.Faithful] : (∀ (X : C), Epi (q.leftTriple.leftToRight.app X)) ↔ ∀ (X : D), Mono (q.rightTriple.rightToLeft.app X)

For an adjoint quadruple L ⊣ F ⊣ G ⊣ R where L and G are fully faithful, all components of the natural transformation L ⟶ G are epimorphisms iff all components of the natural transformation R ⟶ F are monomorphisms.

theorem CategoryTheory.Adjunction.Quadruple.epi_leftTriple_leftToRight_iff_mono_rightTriple_rightToLeft {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {L : Functor C D} {F : Functor D C} {G : Functor C D} {R : Functor D C} (q : Quadruple L F G R) [L.Full] [L.Faithful] [G.Full] [G.Faithful] [Limits.HasPullbacks C] [Limits.HasPushouts D] : Epi q.leftTriple.leftToRight ↔ Mono q.rightTriple.rightToLeft

For an adjoint quadruple L ⊣ F ⊣ G ⊣ R where L and G are fully faithful and their domain and codomain have all pullbacks resp. pushouts, the natural transformation L ⟶ G is an epimorphism iff the natural transformation R ⟶ F is a monomorphism.