@[instance]
def
category_theory.adjunction.monad
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(R : D ⥤ C)
[category_theory.is_right_adjoint R] :
Equations
- category_theory.adjunction.monad R = let L : C ⥤ D := category_theory.left_adjoint R, h : L ⊣ R := category_theory.is_right_adjoint.adj in {η := h.unit, μ := category_theory.whisker_right (category_theory.whisker_left L h.counit) R, assoc' := _, left_unit' := _, right_unit' := _}
@[simp]
theorem
category_theory.adjunction.monad_η_app
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(R : D ⥤ C)
[category_theory.is_right_adjoint R]
(X : C) :
@[simp]
theorem
category_theory.adjunction.monad_μ_app
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(R : D ⥤ C)
[category_theory.is_right_adjoint R]
(X : C) :
(μ_ (category_theory.left_adjoint R ⋙ R)).app X = R.map (category_theory.is_right_adjoint.adj.counit.app ((category_theory.left_adjoint R).obj X))
def
category_theory.monad.comparison
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(R : D ⥤ C)
[category_theory.is_right_adjoint R] :
Equations
- category_theory.monad.comparison R = let h : category_theory.is_right_adjoint.left R ⊣ R := category_theory.is_right_adjoint.adj in {obj := λ (X : D), {A := R.obj X, a := R.map (h.counit.app X), unit' := _, assoc' := _}, map := λ (X Y : D) (f : X ⟶ Y), {f := R.map f, h' := _}, map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.monad.comparison_map_f
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(R : D ⥤ C)
[category_theory.is_right_adjoint R]
{X Y : D}
(f : X ⟶ Y) :
((category_theory.monad.comparison R).map f).f = R.map f
@[simp]
theorem
category_theory.monad.comparison_obj_a
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(R : D ⥤ C)
[category_theory.is_right_adjoint R]
(X : D) :
def
category_theory.monad.comparison_forget
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(R : D ⥤ C)
[category_theory.is_right_adjoint R] :
Equations
- category_theory.monad.comparison_forget R = {hom := {app := λ (X : D), 𝟙 ((category_theory.monad.comparison R ⋙ category_theory.monad.forget (category_theory.left_adjoint R ⋙ R)).obj X), naturality' := _}, inv := {app := λ (X : D), 𝟙 (R.obj X), naturality' := _}, hom_inv_id' := _, inv_hom_id' := _}
@[class]
structure
category_theory.reflective
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D] :
D ⥤ C → Type (max u₁ u₂ v₁ v₂)
- to_is_right_adjoint : category_theory.is_right_adjoint R
- to_full : category_theory.full R
- to_faithful : category_theory.faithful R
A functor is reflective, or a reflective inclusion, if it is fully faithful and right adjoint.
Instances
@[class]
structure
category_theory.monadic_right_adjoint
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D] :
D ⥤ C → Type (max u₁ u₂ v₁ v₂)
- to_is_right_adjoint : category_theory.is_right_adjoint R
- eqv : category_theory.is_equivalence (category_theory.monad.comparison R)
A right adjoint functor R : D ⥤ C is monadic if the comparison function monad.comparison R from D to the
category of Eilenberg-Moore algebras for the adjunction is an equivalence.
Instances
@[instance]
def
category_theory.μ_iso_of_reflective
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(R : D ⥤ C)
[category_theory.reflective R] :
theorem
category_theory.reflective.comparison_ess_surj_aux
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(R : D ⥤ C)
[category_theory.reflective R]
(X : category_theory.monad.algebra (category_theory.left_adjoint R ⋙ R)) :
@[instance]
def
category_theory.reflective.category_theory.is_iso
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(R : D ⥤ C)
[category_theory.reflective R]
(X : category_theory.monad.algebra (category_theory.left_adjoint R ⋙ R)) :
Equations
- category_theory.reflective.category_theory.is_iso R X = let L : C ⥤ D := category_theory.left_adjoint R, h : L ⊣ R := category_theory.is_right_adjoint.adj in {inv := X.a, hom_inv_id' := _, inv_hom_id' := _}
@[instance]
def
category_theory.reflective.comparison_ess_surj
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(R : D ⥤ C)
[category_theory.reflective R] :
Equations
- category_theory.reflective.comparison_ess_surj R = let L : C ⥤ D := category_theory.left_adjoint R, h : L ⊣ R := category_theory.is_right_adjoint.adj in {obj_preimage := λ (X : category_theory.monad.algebra (category_theory.left_adjoint R ⋙ R)), L.obj X.A, iso' := λ (X : category_theory.monad.algebra (category_theory.left_adjoint R ⋙ R)), {hom := {f := (category_theory.as_iso (h.unit.app X.A)).inv, h' := _}, inv := {f := (category_theory.as_iso (h.unit.app X.A)).hom, h' := _}, hom_inv_id' := _, inv_hom_id' := _}}
@[instance]
def
category_theory.reflective.comparison_full
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(R : D ⥤ C)
[category_theory.full R]
[category_theory.is_right_adjoint R] :
Equations
- category_theory.reflective.comparison_full R = {preimage := λ (X Y : D) (f : (category_theory.monad.comparison R).obj X ⟶ (category_theory.monad.comparison R).obj Y), R.preimage f.f, witness' := _}
@[instance]
def
category_theory.reflective.comparison_faithful
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(R : D ⥤ C)
[category_theory.faithful R]
[category_theory.is_right_adjoint R] :
Equations
- _ = _
@[instance]
def
category_theory.monadic_of_reflective
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(R : D ⥤ C)
[category_theory.reflective R] :
Any reflective inclusion has a monadic right adjoint. cf Prop 5.3.3 of [Riehl][riehl2017]