Adjunctions with a parameter #
Given bifunctors F : C₁ ⥤ C₂ ⥤ C₃ and G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂,
this file introduces the notation F ⊣₂ G for the adjunctions
with a parameter (in C₁) between F and G.
(See MonoidalClosed.internalHomAdjunction₂ in the file
CategoryTheory.Closed.Monoidal for an example of such an adjunction.)
Note: this notion is weaker than the notion of
"adjunction of two variables" which appears in the mathematical literature.
In order to have an adjunction of two variables, we need
a third functor H : C₂ᵒᵖ ⥤ C₃ ⥤ C₁ and two adjunctions with
a parameter F ⊣₂ G and F.flip ⊣₂ H.
TODO #
Show that given F : C₁ ⥤ C₂ ⥤ C₃, if F.obj X₁ has a right adjoint
G X₁ : C₃ ⥤ C₂ for any X₁ : C₁, then G extends as a
bifunctor G' : C₁ᵒᵖ ⥤ C₃ ⥤ C₂ with F ⊣₂ G' (and similarly for
left adjoints).
References #
- https://ncatlab.org/nlab/show/two-variable+adjunction
structure
CategoryTheory.ParametrizedAdjunction
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
(F : Functor C₁ (Functor C₂ C₃))
(G : Functor C₁ᵒᵖ (Functor C₃ C₂))
:
Type (max (max (max (max u₁ u₂) u₃) v₂) v₃)
Given bifunctors F : C₁ ⥤ C₂ ⥤ C₃ and G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂,
an adjunction with parameter F ⊣₂ G consists of the data of
adjunctions F.obj X₁ ⊣ G.obj (op X₁) for all X₁ : C₁ which
satisfy a naturality condition with respect to X₁.
a family of adjunctions
- unit_whiskerRight_map {X₁ Y₁ : C₁} (f : X₁ ⟶ Y₁) : CategoryStruct.comp (self.adj X₁).unit (whiskerRight (F.map f) (G.obj (Opposite.op X₁))) = CategoryStruct.comp (self.adj Y₁).unit (whiskerLeft (F.obj Y₁) (G.map f.op))
Instances For
The notation F ⊣₂ G stands for ParametrizedAdjunction F G
representing that the bifunctor F is the left adjoint to G
in an adjunction with a parameter.
Equations
- CategoryTheory.«term_⊣₂_» = Lean.ParserDescr.trailingNode `CategoryTheory.«term_⊣₂_» 15 15 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊣₂ ") (Lean.ParserDescr.cat `term 16))
Instances For
theorem
CategoryTheory.ParametrizedAdjunction.unit_whiskerRight_map_assoc
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
{F : Functor C₁ (Functor C₂ C₃)}
{G : Functor C₁ᵒᵖ (Functor C₃ C₂)}
(self : F ⊣₂ G)
{X₁ Y₁ : C₁}
(f : X₁ ⟶ Y₁)
{Z : Functor C₂ C₂}
(h : (F.obj Y₁).comp (G.obj (Opposite.op X₁)) ⟶ Z)
:
CategoryStruct.comp (self.adj X₁).unit (CategoryStruct.comp (whiskerRight (F.map f) (G.obj (Opposite.op X₁))) h) = CategoryStruct.comp (self.adj Y₁).unit (CategoryStruct.comp (whiskerLeft (F.obj Y₁) (G.map f.op)) h)
def
CategoryTheory.ParametrizedAdjunction.mk'
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
{F : Functor C₁ (Functor C₂ C₃)}
{G : Functor C₁ᵒᵖ (Functor C₃ C₂)}
(adj : (X₁ : C₁) → F.obj X₁ ⊣ G.obj (Opposite.op X₁))
(h :
∀ {X₁ Y₁ : C₁} (f : X₁ ⟶ Y₁) {X₂ : C₂} {X₃ : C₃} (g : (F.obj Y₁).obj X₂ ⟶ X₃),
((adj X₁).homEquiv X₂ X₃) (CategoryStruct.comp ((F.map f).app X₂) g) = CategoryStruct.comp (((adj Y₁).homEquiv X₂ X₃) g) ((G.map f.op).app X₃) := by
aesop_cat)
:
Alternative constructor for parametrized adjunctions, for which
the compatibility is stated in terms of Adjunction.homEquiv.
Equations
- CategoryTheory.ParametrizedAdjunction.mk' adj h = { adj := adj, unit_whiskerRight_map := ⋯ }
Instances For
@[simp]
theorem
CategoryTheory.ParametrizedAdjunction.mk'_adj
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
{F : Functor C₁ (Functor C₂ C₃)}
{G : Functor C₁ᵒᵖ (Functor C₃ C₂)}
(adj : (X₁ : C₁) → F.obj X₁ ⊣ G.obj (Opposite.op X₁))
(h :
∀ {X₁ Y₁ : C₁} (f : X₁ ⟶ Y₁) {X₂ : C₂} {X₃ : C₃} (g : (F.obj Y₁).obj X₂ ⟶ X₃),
((adj X₁).homEquiv X₂ X₃) (CategoryStruct.comp ((F.map f).app X₂) g) = CategoryStruct.comp (((adj Y₁).homEquiv X₂ X₃) g) ((G.map f.op).app X₃) := by
aesop_cat)
(X₁ : C₁)
:
def
CategoryTheory.ParametrizedAdjunction.homEquiv
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
{F : Functor C₁ (Functor C₂ C₃)}
{G : Functor C₁ᵒᵖ (Functor C₃ C₂)}
(adj₂ : F ⊣₂ G)
{X₁ : C₁}
{X₂ : C₂}
{X₃ : C₃}
:
The bijection ((F.obj X₁).obj X₂ ⟶ X₃) ≃ (X₂ ⟶ (G.obj (op X₁)).obj X₃)
given by an adjunction with a parameter adj₂ : F ⊣₂ G.
Instances For
theorem
CategoryTheory.ParametrizedAdjunction.homEquiv_eq
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
{F : Functor C₁ (Functor C₂ C₃)}
{G : Functor C₁ᵒᵖ (Functor C₃ C₂)}
(adj₂ : F ⊣₂ G)
{X₁ : C₁}
{X₂ : C₂}
{X₃ : C₃}
:
theorem
CategoryTheory.ParametrizedAdjunction.homEquiv_naturality_one
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
{F : Functor C₁ (Functor C₂ C₃)}
{G : Functor C₁ᵒᵖ (Functor C₃ C₂)}
(adj₂ : F ⊣₂ G)
{X₁ Y₁ : C₁}
{X₂ : C₂}
{X₃ : C₃}
(f₁ : X₁ ⟶ Y₁)
(g : (F.obj Y₁).obj X₂ ⟶ X₃)
:
adj₂.homEquiv (CategoryStruct.comp ((F.map f₁).app X₂) g) = CategoryStruct.comp (adj₂.homEquiv g) ((G.map f₁.op).app X₃)
theorem
CategoryTheory.ParametrizedAdjunction.homEquiv_naturality_one_assoc
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
{F : Functor C₁ (Functor C₂ C₃)}
{G : Functor C₁ᵒᵖ (Functor C₃ C₂)}
(adj₂ : F ⊣₂ G)
{X₁ Y₁ : C₁}
{X₂ : C₂}
{X₃ : C₃}
(f₁ : X₁ ⟶ Y₁)
(g : (F.obj Y₁).obj X₂ ⟶ X₃)
{Z : C₂}
(h : (G.obj (Opposite.op X₁)).obj X₃ ⟶ Z)
:
CategoryStruct.comp (adj₂.homEquiv (CategoryStruct.comp ((F.map f₁).app X₂) g)) h = CategoryStruct.comp (adj₂.homEquiv g) (CategoryStruct.comp ((G.map f₁.op).app X₃) h)
theorem
CategoryTheory.ParametrizedAdjunction.homEquiv_naturality_two
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
{F : Functor C₁ (Functor C₂ C₃)}
{G : Functor C₁ᵒᵖ (Functor C₃ C₂)}
(adj₂ : F ⊣₂ G)
{X₁ : C₁}
{X₂ Y₂ : C₂}
{X₃ : C₃}
(f₂ : X₂ ⟶ Y₂)
(g : (F.obj X₁).obj Y₂ ⟶ X₃)
:
adj₂.homEquiv (CategoryStruct.comp ((F.obj X₁).map f₂) g) = CategoryStruct.comp f₂ (adj₂.homEquiv g)
theorem
CategoryTheory.ParametrizedAdjunction.homEquiv_naturality_two_assoc
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
{F : Functor C₁ (Functor C₂ C₃)}
{G : Functor C₁ᵒᵖ (Functor C₃ C₂)}
(adj₂ : F ⊣₂ G)
{X₁ : C₁}
{X₂ Y₂ : C₂}
{X₃ : C₃}
(f₂ : X₂ ⟶ Y₂)
(g : (F.obj X₁).obj Y₂ ⟶ X₃)
{Z : C₂}
(h : (G.obj (Opposite.op X₁)).obj X₃ ⟶ Z)
:
CategoryStruct.comp (adj₂.homEquiv (CategoryStruct.comp ((F.obj X₁).map f₂) g)) h = CategoryStruct.comp f₂ (CategoryStruct.comp (adj₂.homEquiv g) h)
theorem
CategoryTheory.ParametrizedAdjunction.homEquiv_naturality_three
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
{F : Functor C₁ (Functor C₂ C₃)}
{G : Functor C₁ᵒᵖ (Functor C₃ C₂)}
(adj₂ : F ⊣₂ G)
{X₁ : C₁}
{X₂ : C₂}
{X₃ Y₃ : C₃}
(f₃ : X₃ ⟶ Y₃)
(g : (F.obj X₁).obj X₂ ⟶ X₃)
:
adj₂.homEquiv (CategoryStruct.comp g f₃) = CategoryStruct.comp (adj₂.homEquiv g) ((G.obj (Opposite.op X₁)).map f₃)
theorem
CategoryTheory.ParametrizedAdjunction.homEquiv_naturality_three_assoc
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
{F : Functor C₁ (Functor C₂ C₃)}
{G : Functor C₁ᵒᵖ (Functor C₃ C₂)}
(adj₂ : F ⊣₂ G)
{X₁ : C₁}
{X₂ : C₂}
{X₃ Y₃ : C₃}
(f₃ : X₃ ⟶ Y₃)
(g : (F.obj X₁).obj X₂ ⟶ X₃)
{Z : C₂}
(h : (G.obj (Opposite.op X₁)).obj Y₃ ⟶ Z)
:
CategoryStruct.comp (adj₂.homEquiv (CategoryStruct.comp g f₃)) h = CategoryStruct.comp (adj₂.homEquiv g) (CategoryStruct.comp ((G.obj (Opposite.op X₁)).map f₃) h)
theorem
CategoryTheory.ParametrizedAdjunction.homEquiv_symm_naturality_one
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
{F : Functor C₁ (Functor C₂ C₃)}
{G : Functor C₁ᵒᵖ (Functor C₃ C₂)}
(adj₂ : F ⊣₂ G)
{X₁ Y₁ : C₁}
{X₂ : C₂}
{X₃ : C₃}
(f₁ : X₁ ⟶ Y₁)
(g : X₂ ⟶ (G.obj (Opposite.op Y₁)).obj X₃)
:
theorem
CategoryTheory.ParametrizedAdjunction.homEquiv_symm_naturality_one_assoc
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
{F : Functor C₁ (Functor C₂ C₃)}
{G : Functor C₁ᵒᵖ (Functor C₃ C₂)}
(adj₂ : F ⊣₂ G)
{X₁ Y₁ : C₁}
{X₂ : C₂}
{X₃ : C₃}
(f₁ : X₁ ⟶ Y₁)
(g : X₂ ⟶ (G.obj (Opposite.op Y₁)).obj X₃)
{Z : C₃}
(h : X₃ ⟶ Z)
:
CategoryStruct.comp (adj₂.homEquiv.symm (CategoryStruct.comp g ((G.map f₁.op).app X₃))) h = CategoryStruct.comp ((F.map f₁).app X₂) (CategoryStruct.comp (adj₂.homEquiv.symm g) h)
theorem
CategoryTheory.ParametrizedAdjunction.homEquiv_symm_naturality_two
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
{F : Functor C₁ (Functor C₂ C₃)}
{G : Functor C₁ᵒᵖ (Functor C₃ C₂)}
(adj₂ : F ⊣₂ G)
{X₁ : C₁}
{X₂ Y₂ : C₂}
{X₃ : C₃}
(f₂ : X₂ ⟶ Y₂)
(g : Y₂ ⟶ (G.obj (Opposite.op X₁)).obj X₃)
:
adj₂.homEquiv.symm (CategoryStruct.comp f₂ g) = CategoryStruct.comp ((F.obj X₁).map f₂) (adj₂.homEquiv.symm g)
theorem
CategoryTheory.ParametrizedAdjunction.homEquiv_symm_naturality_two_assoc
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
{F : Functor C₁ (Functor C₂ C₃)}
{G : Functor C₁ᵒᵖ (Functor C₃ C₂)}
(adj₂ : F ⊣₂ G)
{X₁ : C₁}
{X₂ Y₂ : C₂}
{X₃ : C₃}
(f₂ : X₂ ⟶ Y₂)
(g : Y₂ ⟶ (G.obj (Opposite.op X₁)).obj X₃)
{Z : C₃}
(h : X₃ ⟶ Z)
:
CategoryStruct.comp (adj₂.homEquiv.symm (CategoryStruct.comp f₂ g)) h = CategoryStruct.comp ((F.obj X₁).map f₂) (CategoryStruct.comp (adj₂.homEquiv.symm g) h)
theorem
CategoryTheory.ParametrizedAdjunction.homEquiv_symm_naturality_three
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
{F : Functor C₁ (Functor C₂ C₃)}
{G : Functor C₁ᵒᵖ (Functor C₃ C₂)}
(adj₂ : F ⊣₂ G)
{X₁ : C₁}
{X₂ : C₂}
{X₃ Y₃ : C₃}
(f₃ : X₃ ⟶ Y₃)
(g : X₂ ⟶ (G.obj (Opposite.op X₁)).obj X₃)
:
adj₂.homEquiv.symm (CategoryStruct.comp g ((G.obj (Opposite.op X₁)).map f₃)) = CategoryStruct.comp (adj₂.homEquiv.symm g) f₃
theorem
CategoryTheory.ParametrizedAdjunction.homEquiv_symm_naturality_three_assoc
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
{F : Functor C₁ (Functor C₂ C₃)}
{G : Functor C₁ᵒᵖ (Functor C₃ C₂)}
(adj₂ : F ⊣₂ G)
{X₁ : C₁}
{X₂ : C₂}
{X₃ Y₃ : C₃}
(f₃ : X₃ ⟶ Y₃)
(g : X₂ ⟶ (G.obj (Opposite.op X₁)).obj X₃)
{Z : C₃}
(h : Y₃ ⟶ Z)
:
CategoryStruct.comp (adj₂.homEquiv.symm (CategoryStruct.comp g ((G.obj (Opposite.op X₁)).map f₃))) h = CategoryStruct.comp (adj₂.homEquiv.symm g) (CategoryStruct.comp f₃ h)
theorem
CategoryTheory.ParametrizedAdjunction.whiskerLeft_map_counit
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
{F : Functor C₁ (Functor C₂ C₃)}
{G : Functor C₁ᵒᵖ (Functor C₃ C₂)}
(adj₂ : F ⊣₂ G)
{X₁ Y₁ : C₁}
(f : X₁ ⟶ Y₁)
:
CategoryStruct.comp (whiskerLeft (G.obj (Opposite.op Y₁)) (F.map f)) (adj₂.adj Y₁).counit = CategoryStruct.comp (whiskerRight (G.map f.op) (F.obj X₁)) (adj₂.adj X₁).counit
theorem
CategoryTheory.ParametrizedAdjunction.whiskerLeft_map_counit_assoc
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
{F : Functor C₁ (Functor C₂ C₃)}
{G : Functor C₁ᵒᵖ (Functor C₃ C₂)}
(adj₂ : F ⊣₂ G)
{X₁ Y₁ : C₁}
(f : X₁ ⟶ Y₁)
{Z : Functor C₃ C₃}
(h : Functor.id C₃ ⟶ Z)
:
CategoryStruct.comp (whiskerLeft (G.obj (Opposite.op Y₁)) (F.map f)) (CategoryStruct.comp (adj₂.adj Y₁).counit h) = CategoryStruct.comp (whiskerRight (G.map f.op) (F.obj X₁)) (CategoryStruct.comp (adj₂.adj X₁).counit h)