Composition, natural transformations and equivalences of left-linear functors #
Let a monoidal category C act on the left on categories D, D', D''. Mathlib's
Functor.LaxLeftLinear, Functor.OplaxLeftLinear and Functor.LeftLinear equip a functor with
lineators μₗ F c d : c ⊙ₗ F.obj d ⟶ F.obj (c ⊙ₗ d) and δₗ F c d in the other direction. For a
group G, a left-linear functor between categories with an action of Discrete G is a
G-equivariant functor, with commutation isomorphisms satisfying the unit and product
diagrams. This file develops the structure these functors form:
- the identity functor is (lax, oplax) left-linear with identity lineators, and composites of
(lax, oplax) left-linear functors are (lax, oplax) left-linear (
Functor.LaxLeftLinear.comp,Functor.OplaxLeftLinear.comp,Functor.LeftLinear.comp); Functor.LeftLinear.ofLaxLeftLinear: a lax left-linear functor with invertible lineators is left-linear;NatTrans.IsLeftLinear: a natural transformation between lax left-linear functors is left-linear (equivariant) when it commutes with the lineators. These are closed under identities, vertical and horizontal composition, whiskering and inverses, and the unitors and associators of functor composition are left-linear. Between left-linear functors, it is equivalent to commute with the oplax lineators (app_comp_δₗ,of_app_comp_δₗ);Adjunction.rightAdjointLaxLeftLinear: the right adjoint of an oplax left-linear functor is lax left-linear; when the left adjoint is left-linear, the unit and counit are left-linear;Equivalence.inverseLeftLinear: the inverse of a left-linear equivalence is left-linear, and the unit and counit of the equivalence are then left-linear, so that an equivalence whose functor is equivariant is an equivalence of categories with an action.
The constructions follow their monoidal counterparts in Mathlib: Functor.LaxMonoidal.comp,
NatTrans.IsMonoidal, Adjunction.rightAdjointLaxMonoidal and Equivalence.inverseMonoidal.
@[instance_reducible]
instance
CategoryTheory.Functor.LaxLeftLinear.id
(C : Type u_1)
[Category.{v_1, u_1} C]
[MonoidalCategory C]
(D : Type u_2)
[Category.{v_2, u_2} D]
[MonoidalCategory.MonoidalLeftAction C D]
:
(Functor.id D).LaxLeftLinear C
The identity functor is lax left-linear, with identity lineators.
@[simp]
theorem
CategoryTheory.Functor.LaxLeftLinear.id_μₗ
(C : Type u_1)
[Category.{v_1, u_1} C]
[MonoidalCategory C]
(D : Type u_2)
[Category.{v_2, u_2} D]
[MonoidalCategory.MonoidalLeftAction C D]
(x✝ : C)
(x✝¹ : D)
:
μₗ (Functor.id D) x✝ x✝¹ = CategoryStruct.id (MonoidalCategory.MonoidalLeftActionStruct.actionObj x✝ ((Functor.id D).obj x✝¹))
@[instance_reducible]
instance
CategoryTheory.Functor.LaxLeftLinear.comp
{C : Type u_1}
[Category.{v_1, u_1} C]
[MonoidalCategory C]
{D : Type u_2}
[Category.{v_2, u_2} D]
[MonoidalCategory.MonoidalLeftAction C D]
{D' : Type u_3}
[Category.{v_3, u_3} D']
[MonoidalCategory.MonoidalLeftAction C D']
{D'' : Type u_4}
[Category.{v_4, u_4} D'']
[MonoidalCategory.MonoidalLeftAction C D'']
(F : Functor D D')
(G : Functor D' D'')
[F.LaxLeftLinear C]
[G.LaxLeftLinear C]
:
(F.comp G).LaxLeftLinear C
The composite of lax left-linear functors is lax left-linear: the lineator of F ⋙ G at
c and d is μₗ G c (F.obj d) ≫ G.map (μₗ F c d).
@[simp]
theorem
CategoryTheory.Functor.LaxLeftLinear.comp_μₗ
{C : Type u_1}
[Category.{v_1, u_1} C]
[MonoidalCategory C]
{D : Type u_2}
[Category.{v_2, u_2} D]
[MonoidalCategory.MonoidalLeftAction C D]
{D' : Type u_3}
[Category.{v_3, u_3} D']
[MonoidalCategory.MonoidalLeftAction C D']
{D'' : Type u_4}
[Category.{v_4, u_4} D'']
[MonoidalCategory.MonoidalLeftAction C D'']
(F : Functor D D')
(G : Functor D' D'')
[F.LaxLeftLinear C]
[G.LaxLeftLinear C]
(c : C)
(d : D)
:
@[instance_reducible]
instance
CategoryTheory.Functor.OplaxLeftLinear.id
(C : Type u_1)
[Category.{v_1, u_1} C]
[MonoidalCategory C]
(D : Type u_2)
[Category.{v_2, u_2} D]
[MonoidalCategory.MonoidalLeftAction C D]
:
(Functor.id D).OplaxLeftLinear C
The identity functor is oplax left-linear, with identity lineators.
@[simp]
theorem
CategoryTheory.Functor.OplaxLeftLinear.id_δₗ
(C : Type u_1)
[Category.{v_1, u_1} C]
[MonoidalCategory C]
(D : Type u_2)
[Category.{v_2, u_2} D]
[MonoidalCategory.MonoidalLeftAction C D]
(x✝ : C)
(x✝¹ : D)
:
δₗ (Functor.id D) x✝ x✝¹ = CategoryStruct.id ((Functor.id D).obj (MonoidalCategory.MonoidalLeftActionStruct.actionObj x✝ x✝¹))
@[instance_reducible]
instance
CategoryTheory.Functor.OplaxLeftLinear.comp
{C : Type u_1}
[Category.{v_1, u_1} C]
[MonoidalCategory C]
{D : Type u_2}
[Category.{v_2, u_2} D]
[MonoidalCategory.MonoidalLeftAction C D]
{D' : Type u_3}
[Category.{v_3, u_3} D']
[MonoidalCategory.MonoidalLeftAction C D']
{D'' : Type u_4}
[Category.{v_4, u_4} D'']
[MonoidalCategory.MonoidalLeftAction C D'']
(F : Functor D D')
(G : Functor D' D'')
[F.OplaxLeftLinear C]
[G.OplaxLeftLinear C]
:
(F.comp G).OplaxLeftLinear C
The composite of oplax left-linear functors is oplax left-linear: the lineator of F ⋙ G
at c and d is G.map (δₗ F c d) ≫ δₗ G c (F.obj d).
@[simp]
theorem
CategoryTheory.Functor.OplaxLeftLinear.comp_δₗ
{C : Type u_1}
[Category.{v_1, u_1} C]
[MonoidalCategory C]
{D : Type u_2}
[Category.{v_2, u_2} D]
[MonoidalCategory.MonoidalLeftAction C D]
{D' : Type u_3}
[Category.{v_3, u_3} D']
[MonoidalCategory.MonoidalLeftAction C D']
{D'' : Type u_4}
[Category.{v_4, u_4} D'']
[MonoidalCategory.MonoidalLeftAction C D'']
(F : Functor D D')
(G : Functor D' D'')
[F.OplaxLeftLinear C]
[G.OplaxLeftLinear C]
(c : C)
(d : D)
:
@[instance_reducible]
instance
CategoryTheory.Functor.LeftLinear.id
(C : Type u_1)
[Category.{v_1, u_1} C]
[MonoidalCategory C]
(D : Type u_2)
[Category.{v_2, u_2} D]
[MonoidalCategory.MonoidalLeftAction C D]
:
(Functor.id D).LeftLinear C
The identity functor is left-linear, with identity lineators.
@[instance_reducible]
noncomputable def
CategoryTheory.Functor.LeftLinear.ofLaxLeftLinear
{C : Type u_1}
[Category.{v_1, u_1} C]
[MonoidalCategory C]
{D : Type u_2}
[Category.{v_2, u_2} D]
[MonoidalCategory.MonoidalLeftAction C D]
{D' : Type u_3}
[Category.{v_3, u_3} D']
[MonoidalCategory.MonoidalLeftAction C D']
(F : Functor D D')
[F.LaxLeftLinear C]
[∀ (c : C) (d : D), IsIso (LaxLeftLinear.μₗ F c d)]
:
F.LeftLinear C
A lax left-linear functor whose lineators μₗ F c d are isomorphisms is left-linear, with
oplax lineators their inverses.
Instances For
theorem
CategoryTheory.Functor.LeftLinear.ofLaxLeftLinear_δₗ
{C : Type u_1}
[Category.{v_1, u_1} C]
[MonoidalCategory C]
{D : Type u_2}
[Category.{v_2, u_2} D]
[MonoidalCategory.MonoidalLeftAction C D]
{D' : Type u_3}
[Category.{v_3, u_3} D']
[MonoidalCategory.MonoidalLeftAction C D']
(F : Functor D D')
[F.LaxLeftLinear C]
[∀ (c : C) (d : D), IsIso (LaxLeftLinear.μₗ F c d)]
(c : C)
(d : D)
:
The oplax lineators of LeftLinear.ofLaxLeftLinear F are the inverses of the lax ones.
@[instance_reducible]
instance
CategoryTheory.Functor.LeftLinear.comp
{C : Type u_1}
[Category.{v_1, u_1} C]
[MonoidalCategory C]
{D : Type u_2}
[Category.{v_2, u_2} D]
[MonoidalCategory.MonoidalLeftAction C D]
{D' : Type u_3}
[Category.{v_3, u_3} D']
[MonoidalCategory.MonoidalLeftAction C D']
{D'' : Type u_4}
[Category.{v_4, u_4} D'']
[MonoidalCategory.MonoidalLeftAction C D'']
(F : Functor D D')
(G : Functor D' D'')
[F.LeftLinear C]
[G.LeftLinear C]
:
(F.comp G).LeftLinear C
The composite of left-linear functors is left-linear, with the lineators of
LaxLeftLinear.comp and OplaxLeftLinear.comp.
class
CategoryTheory.NatTrans.IsLeftLinear
{D : Type u_1}
[Category.{v_1, u_1} D]
{D' : Type u_2}
[Category.{v_2, u_2} D']
{F₁ F₂ : Functor D D'}
(τ : F₁ ⟶ F₂)
(C : Type u_3)
[Category.{v_3, u_3} C]
[MonoidalCategory C]
[MonoidalCategory.MonoidalLeftAction C D]
[MonoidalCategory.MonoidalLeftAction C D']
[F₁.LaxLeftLinear C]
[F₂.LaxLeftLinear C]
:
A natural transformation τ : F₁ ⟶ F₂ between lax left-linear functors is left-linear
(equivariant) if it commutes with the lineators:
μₗ F₁ c d ≫ τ.app (c ⊙ₗ d) = c ⊴ₗ τ.app d ≫ μₗ F₂ c d.
- μₗ_comp_app (c : C) (d : D) : CategoryStruct.comp (Functor.LaxLeftLinear.μₗ F₁ c d) (τ.app (MonoidalCategory.MonoidalLeftActionStruct.actionObj c d)) = CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c (τ.app d)) (Functor.LaxLeftLinear.μₗ F₂ c d)
Instances
@[simp]
theorem
CategoryTheory.NatTrans.IsLeftLinear.μₗ_comp_app_assoc
{D : Type u_1}
{inst✝ : Category.{v_1, u_1} D}
{D' : Type u_2}
{inst✝¹ : Category.{v_2, u_2} D'}
{F₁ F₂ : Functor D D'}
(τ : F₁ ⟶ F₂)
{C : Type u_3}
{inst✝² : Category.{v_3, u_3} C}
{inst✝³ : MonoidalCategory C}
{inst✝⁴ : MonoidalCategory.MonoidalLeftAction C D}
{inst✝⁵ : MonoidalCategory.MonoidalLeftAction C D'}
{inst✝⁶ : F₁.LaxLeftLinear C}
{inst✝⁷ : F₂.LaxLeftLinear C}
[self : IsLeftLinear τ C]
(c : C)
(d : D)
{Z : D'}
(h : F₂.obj (MonoidalCategory.MonoidalLeftActionStruct.actionObj c d) ⟶ Z)
:
instance
CategoryTheory.NatTrans.IsLeftLinear.id
{D : Type u_1}
[Category.{v_1, u_1} D]
{D' : Type u_2}
[Category.{v_2, u_2} D']
{C : Type u_3}
[Category.{v_3, u_3} C]
[MonoidalCategory C]
[MonoidalCategory.MonoidalLeftAction C D]
[MonoidalCategory.MonoidalLeftAction C D']
{F₁ : Functor D D'}
[F₁.LaxLeftLinear C]
:
IsLeftLinear (CategoryStruct.id F₁) C
The identity natural transformation is left-linear.
instance
CategoryTheory.NatTrans.IsLeftLinear.comp
{D : Type u_1}
[Category.{v_1, u_1} D]
{D' : Type u_2}
[Category.{v_2, u_2} D']
{C : Type u_3}
[Category.{v_3, u_3} C]
[MonoidalCategory C]
[MonoidalCategory.MonoidalLeftAction C D]
[MonoidalCategory.MonoidalLeftAction C D']
{F₁ F₂ F₃ : Functor D D'}
[F₁.LaxLeftLinear C]
[F₂.LaxLeftLinear C]
[F₃.LaxLeftLinear C]
(τ : F₁ ⟶ F₂)
(τ' : F₂ ⟶ F₃)
[IsLeftLinear τ C]
[IsLeftLinear τ' C]
:
IsLeftLinear (CategoryStruct.comp τ τ') C
The vertical composite of left-linear natural transformations is left-linear.
instance
CategoryTheory.NatTrans.IsLeftLinear.hcomp
{D : Type u_1}
[Category.{v_1, u_1} D]
{D' : Type u_2}
[Category.{v_2, u_2} D']
{C : Type u_3}
[Category.{v_3, u_3} C]
[MonoidalCategory C]
[MonoidalCategory.MonoidalLeftAction C D]
[MonoidalCategory.MonoidalLeftAction C D']
{D'' : Type u_4}
[Category.{v_4, u_4} D'']
[MonoidalCategory.MonoidalLeftAction C D'']
{F₁ F₂ : Functor D D'}
[F₁.LaxLeftLinear C]
[F₂.LaxLeftLinear C]
(τ : F₁ ⟶ F₂)
{G₁ G₂ : Functor D' D''}
[G₁.LaxLeftLinear C]
[G₂.LaxLeftLinear C]
(τ' : G₁ ⟶ G₂)
[IsLeftLinear τ C]
[IsLeftLinear τ' C]
:
IsLeftLinear (τ ◫ τ') C
The horizontal composite of left-linear natural transformations is left-linear, for the
left-linear structures of Functor.LaxLeftLinear.comp.
instance
CategoryTheory.NatTrans.IsLeftLinear.whiskerRight
{D : Type u_1}
[Category.{v_1, u_1} D]
{D' : Type u_2}
[Category.{v_2, u_2} D']
{C : Type u_3}
[Category.{v_3, u_3} C]
[MonoidalCategory C]
[MonoidalCategory.MonoidalLeftAction C D]
[MonoidalCategory.MonoidalLeftAction C D']
{D'' : Type u_4}
[Category.{v_4, u_4} D'']
[MonoidalCategory.MonoidalLeftAction C D'']
{F₁ F₂ : Functor D D'}
[F₁.LaxLeftLinear C]
[F₂.LaxLeftLinear C]
(τ : F₁ ⟶ F₂)
{G : Functor D' D''}
[G.LaxLeftLinear C]
[IsLeftLinear τ C]
:
IsLeftLinear (Functor.whiskerRight τ G) C
instance
CategoryTheory.NatTrans.IsLeftLinear.whiskerLeft
{D : Type u_1}
[Category.{v_1, u_1} D]
{D' : Type u_2}
[Category.{v_2, u_2} D']
{C : Type u_3}
[Category.{v_3, u_3} C]
[MonoidalCategory C]
[MonoidalCategory.MonoidalLeftAction C D]
[MonoidalCategory.MonoidalLeftAction C D']
{D'' : Type u_4}
[Category.{v_4, u_4} D'']
[MonoidalCategory.MonoidalLeftAction C D'']
{F₁ : Functor D D'}
[F₁.LaxLeftLinear C]
{G₁ G₂ : Functor D' D''}
[G₁.LaxLeftLinear C]
[G₂.LaxLeftLinear C]
(τ' : G₁ ⟶ G₂)
[IsLeftLinear τ' C]
:
IsLeftLinear (F₁.whiskerLeft τ') C
instance
CategoryTheory.NatTrans.IsLeftLinear.instHomFunctorLeftUnitor
{D : Type u_1}
[Category.{v_1, u_1} D]
{D' : Type u_2}
[Category.{v_2, u_2} D']
{C : Type u_3}
[Category.{v_3, u_3} C]
[MonoidalCategory C]
[MonoidalCategory.MonoidalLeftAction C D]
[MonoidalCategory.MonoidalLeftAction C D']
(F : Functor D D')
[F.LaxLeftLinear C]
:
instance
CategoryTheory.NatTrans.IsLeftLinear.instHomFunctorRightUnitor
{D : Type u_1}
[Category.{v_1, u_1} D]
{D' : Type u_2}
[Category.{v_2, u_2} D']
{C : Type u_3}
[Category.{v_3, u_3} C]
[MonoidalCategory C]
[MonoidalCategory.MonoidalLeftAction C D]
[MonoidalCategory.MonoidalLeftAction C D']
(F : Functor D D')
[F.LaxLeftLinear C]
:
instance
CategoryTheory.NatTrans.IsLeftLinear.instHomFunctorAssociator
{D : Type u_1}
[Category.{v_1, u_1} D]
{D' : Type u_2}
[Category.{v_2, u_2} D']
{C : Type u_3}
[Category.{v_3, u_3} C]
[MonoidalCategory C]
[MonoidalCategory.MonoidalLeftAction C D]
[MonoidalCategory.MonoidalLeftAction C D']
{D'' : Type u_4}
[Category.{v_4, u_4} D'']
[MonoidalCategory.MonoidalLeftAction C D'']
{D''' : Type u_5}
[Category.{v_5, u_5} D''']
[MonoidalCategory.MonoidalLeftAction C D''']
(F : Functor D D')
(G : Functor D' D'')
(H : Functor D'' D''')
[F.LaxLeftLinear C]
[G.LaxLeftLinear C]
[H.LaxLeftLinear C]
:
IsLeftLinear (F.associator G H).hom C
theorem
CategoryTheory.NatTrans.IsLeftLinear.app_comp_δₗ
{D : Type u_1}
[Category.{v_1, u_1} D]
{D' : Type u_2}
[Category.{v_2, u_2} D']
{C : Type u_3}
[Category.{v_3, u_3} C]
[MonoidalCategory C]
[MonoidalCategory.MonoidalLeftAction C D]
[MonoidalCategory.MonoidalLeftAction C D']
{F₁ F₂ : Functor D D'}
[F₁.LeftLinear C]
[F₂.LeftLinear C]
(τ : F₁ ⟶ F₂)
[IsLeftLinear τ C]
(c : C)
(d : D)
:
For left-linear functors, a left-linear natural transformation also commutes with the oplax
lineators δₗ.
theorem
CategoryTheory.NatTrans.IsLeftLinear.app_comp_δₗ_assoc
{D : Type u_1}
[Category.{v_1, u_1} D]
{D' : Type u_2}
[Category.{v_2, u_2} D']
{C : Type u_3}
[Category.{v_3, u_3} C]
[MonoidalCategory C]
[MonoidalCategory.MonoidalLeftAction C D]
[MonoidalCategory.MonoidalLeftAction C D']
{F₁ F₂ : Functor D D'}
[F₁.LeftLinear C]
[F₂.LeftLinear C]
(τ : F₁ ⟶ F₂)
[IsLeftLinear τ C]
(c : C)
(d : D)
{Z : D'}
(h : MonoidalCategory.MonoidalLeftActionStruct.actionObj c (F₂.obj d) ⟶ Z)
:
For left-linear functors, a left-linear natural transformation also commutes with the oplax
lineators δₗ.
theorem
CategoryTheory.NatTrans.IsLeftLinear.of_app_comp_δₗ
{D : Type u_1}
[Category.{v_1, u_1} D]
{D' : Type u_2}
[Category.{v_2, u_2} D']
{C : Type u_3}
[Category.{v_3, u_3} C]
[MonoidalCategory C]
[MonoidalCategory.MonoidalLeftAction C D]
[MonoidalCategory.MonoidalLeftAction C D']
{F₁ F₂ : Functor D D'}
[F₁.LeftLinear C]
[F₂.LeftLinear C]
(τ : F₁ ⟶ F₂)
(h :
∀ (c : C) (d : D),
CategoryStruct.comp (τ.app (MonoidalCategory.MonoidalLeftActionStruct.actionObj c d))
(Functor.OplaxLeftLinear.δₗ F₂ c d) = CategoryStruct.comp (Functor.OplaxLeftLinear.δₗ F₁ c d)
(MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c (τ.app d)))
:
IsLeftLinear τ C
For left-linear functors, a natural transformation that commutes with the oplax lineators
δₗ is left-linear.
instance
CategoryTheory.Iso.instIsLeftLinearInvFunctorOfHom
{C : Type u_1}
[Category.{v_1, u_1} C]
[MonoidalCategory C]
{D : Type u_2}
[Category.{v_2, u_2} D]
[MonoidalCategory.MonoidalLeftAction C D]
{D' : Type u_3}
[Category.{v_3, u_3} D']
[MonoidalCategory.MonoidalLeftAction C D']
{F₁ F₂ : Functor D D'}
[F₁.LaxLeftLinear C]
[F₂.LaxLeftLinear C]
(e : F₁ ≅ F₂)
[NatTrans.IsLeftLinear e.hom C]
:
The inverse of a natural isomorphism whose forward map is left-linear is left-linear.
@[instance_reducible]
def
CategoryTheory.Adjunction.rightAdjointLaxLeftLinear
(C : Type u_1)
[Category.{v_1, u_1} C]
[MonoidalCategory C]
{D : Type u_2}
[Category.{v_2, u_2} D]
[MonoidalCategory.MonoidalLeftAction C D]
{D' : Type u_3}
[Category.{v_3, u_3} D']
[MonoidalCategory.MonoidalLeftAction C D']
{F : Functor D D'}
{G : Functor D' D}
(adj : F ⊣ G)
[F.OplaxLeftLinear C]
:
G.LaxLeftLinear C
The right adjoint of an oplax left-linear functor is lax left-linear: the lineator
μₗ G c d : c ⊙ₗ G.obj d ⟶ G.obj (c ⊙ₗ d) is the adjoint of
δₗ F c (G.obj d) ≫ c ⊴ₗ adj.counit.app d : F.obj (c ⊙ₗ G.obj d) ⟶ c ⊙ₗ d.
Instances For
theorem
CategoryTheory.Adjunction.rightAdjointLaxLeftLinear_μₗ
{C : Type u_1}
[Category.{v_1, u_1} C]
[MonoidalCategory C]
{D : Type u_2}
[Category.{v_2, u_2} D]
[MonoidalCategory.MonoidalLeftAction C D]
{D' : Type u_3}
[Category.{v_3, u_3} D']
[MonoidalCategory.MonoidalLeftAction C D']
{F : Functor D D'}
{G : Functor D' D}
(adj : F ⊣ G)
[F.OplaxLeftLinear C]
(c : C)
(d : D')
:
Functor.LaxLeftLinear.μₗ G c d = (adj.homEquiv (MonoidalCategory.MonoidalLeftActionStruct.actionObj c (G.obj d))
(MonoidalCategory.MonoidalLeftActionStruct.actionObj c ((Functor.id D').obj d)))
(CategoryStruct.comp (Functor.OplaxLeftLinear.δₗ F c (G.obj d))
(MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c (adj.counit.app d)))
The lax lineators of adj.rightAdjointLaxLeftLinear C.
theorem
CategoryTheory.Adjunction.isLeftLinear_unit
(C : Type u_1)
[Category.{v_1, u_1} C]
[MonoidalCategory C]
{D : Type u_2}
[Category.{v_2, u_2} D]
[MonoidalCategory.MonoidalLeftAction C D]
{D' : Type u_3}
[Category.{v_3, u_3} D']
[MonoidalCategory.MonoidalLeftAction C D']
{F : Functor D D'}
{G : Functor D' D}
(adj : F ⊣ G)
[F.LeftLinear C]
:
NatTrans.IsLeftLinear adj.unit C
If F is left-linear and G carries the lax left-linear structure of
adj.rightAdjointLaxLeftLinear C, the unit 𝟭 D ⟶ F ⋙ G of the adjunction is left-linear.
theorem
CategoryTheory.Adjunction.isLeftLinear_counit
(C : Type u_1)
[Category.{v_1, u_1} C]
[MonoidalCategory C]
{D : Type u_2}
[Category.{v_2, u_2} D]
[MonoidalCategory.MonoidalLeftAction C D]
{D' : Type u_3}
[Category.{v_3, u_3} D']
[MonoidalCategory.MonoidalLeftAction C D']
{F : Functor D D'}
{G : Functor D' D}
(adj : F ⊣ G)
[F.LeftLinear C]
:
NatTrans.IsLeftLinear adj.counit C
If F is left-linear and G carries the lax left-linear structure of
adj.rightAdjointLaxLeftLinear C, the counit G ⋙ F ⟶ 𝟭 D' of the adjunction is
left-linear.
@[instance_reducible]
noncomputable def
CategoryTheory.Equivalence.inverseLeftLinear
(C : Type u_1)
[Category.{v_1, u_1} C]
[MonoidalCategory C]
{D : Type u_2}
[Category.{v_2, u_2} D]
[MonoidalCategory.MonoidalLeftAction C D]
{D' : Type u_3}
[Category.{v_3, u_3} D']
[MonoidalCategory.MonoidalLeftAction C D']
(e : D ≌ D')
[e.functor.LeftLinear C]
:
e.inverse.LeftLinear C
If the functor of an equivalence e is left-linear, so is its inverse, with lax lineators
those of e.toAdjunction.rightAdjointLaxLeftLinear C.
Instances For
theorem
CategoryTheory.Equivalence.inverseLeftLinear_μₗ
{C : Type u_1}
[Category.{v_1, u_1} C]
[MonoidalCategory C]
{D : Type u_2}
[Category.{v_2, u_2} D]
[MonoidalCategory.MonoidalLeftAction C D]
{D' : Type u_3}
[Category.{v_3, u_3} D']
[MonoidalCategory.MonoidalLeftAction C D']
(e : D ≌ D')
[e.functor.LeftLinear C]
(c : C)
(d : D')
:
Functor.LaxLeftLinear.μₗ e.inverse c d = CategoryStruct.comp (e.unit.app (MonoidalCategory.MonoidalLeftActionStruct.actionObj c (e.inverse.obj d)))
(e.inverse.map
(CategoryStruct.comp (Functor.OplaxLeftLinear.δₗ e.functor c (e.inverse.obj d))
(MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c (e.counit.app d))))
The lax lineators of e.inverseLeftLinear C: μₗ e.inverse c d is the adjoint of
δₗ e.functor c (e.inverse.obj d) ≫ c ⊴ₗ e.counit.app d.
theorem
CategoryTheory.Equivalence.inverseLeftLinear_δₗ
{C : Type u_1}
[Category.{v_1, u_1} C]
[MonoidalCategory C]
{D : Type u_2}
[Category.{v_2, u_2} D]
[MonoidalCategory.MonoidalLeftAction C D]
{D' : Type u_3}
[Category.{v_3, u_3} D']
[MonoidalCategory.MonoidalLeftAction C D']
(e : D ≌ D')
[e.functor.LeftLinear C]
(c : C)
(d : D')
:
The oplax lineators of e.inverseLeftLinear C are the inverses of its lax lineators.
theorem
CategoryTheory.Equivalence.isLeftLinear_unit
(C : Type u_1)
[Category.{v_1, u_1} C]
[MonoidalCategory C]
{D : Type u_2}
[Category.{v_2, u_2} D]
[MonoidalCategory.MonoidalLeftAction C D]
{D' : Type u_3}
[Category.{v_3, u_3} D']
[MonoidalCategory.MonoidalLeftAction C D']
(e : D ≌ D')
[e.functor.LeftLinear C]
:
For the left-linear structure e.inverseLeftLinear C on the inverse, the unit
𝟭 D ⟶ e.functor ⋙ e.inverse of the equivalence is left-linear.
theorem
CategoryTheory.Equivalence.isLeftLinear_counit
(C : Type u_1)
[Category.{v_1, u_1} C]
[MonoidalCategory C]
{D : Type u_2}
[Category.{v_2, u_2} D]
[MonoidalCategory.MonoidalLeftAction C D]
{D' : Type u_3}
[Category.{v_3, u_3} D']
[MonoidalCategory.MonoidalLeftAction C D']
(e : D ≌ D')
[e.functor.LeftLinear C]
:
For the left-linear structure e.inverseLeftLinear C on the inverse, the counit
e.inverse ⋙ e.functor ⟶ 𝟭 D' of the equivalence is left-linear.