Relative monad

This file defines the RelativeMonad type class, both as a category-theoretic object and a programming object.

structure CategoryTheory.RelativeMonad (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (J : Functor C D) : Type (max (max u₁ u₂) v₂)

The data of a relative monad over a functor J : C ⟶ D consists of:

• a map between objects T : C → D
• a natural transformation η : ∀ {X}, J X ⟶ T X
• a natural transformation μ : ∀ {X Y}, (J X ⟶ T Y) ⟶ (T X ⟶ T Y) satisfying three equations:
• μ_{X, X} ∘ η_X = 1_{T X} (left unit)
• ∀ f, η_X ≫ μ_{X, Y} = f (right unit)
• ∀ f g, μ_{X, Z} (f ≫ μ_{Y, Z} g) = μ_{X, Y} f ≫ μ_{Y, Z} g (associativity)

• T : C → D

  The monadic mapping on objects.

• η {X : C} : J.obj X ⟶ self.T X

  The unit for the relative monad.

• μ {X Y : C} : (J.obj X ⟶ self.T Y) → (self.T X ⟶ self.T Y)

  The multiplication for the monad.

• left_unit {X : C} : self.μ self.η = CategoryStruct.id (self.T X)

  μ applied to η is identity.

• right_unit {X Y : C} (f : J.obj X ⟶ self.T Y) : CategoryStruct.comp self.η (self.μ f) = f

  η composed with μ is identity.

• assoc {X Y Z : C} (f : J.obj X ⟶ self.T Y) (g : J.obj Y ⟶ self.T Z) : self.μ (CategoryStruct.comp f (self.μ g)) = CategoryStruct.comp (self.μ f) (self.μ g)

  μ is associative.

@[simp]

theorem CategoryTheory.RelativeMonad.right_unit_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Functor C D} (self : RelativeMonad C D J) {X Y : C} (f : J.obj X ⟶ self.T Y) {Z : D} (h : self.T Y ⟶ Z) : CategoryStruct.comp self.η (CategoryStruct.comp (self.μ f) h) = CategoryStruct.comp f h

η composed with μ is identity.

@[simp]

theorem CategoryTheory.RelativeMonad.left_unit_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Functor C D} (self : RelativeMonad C D J) {X : C} {Z : D} (h : self.T X ⟶ Z) : CategoryStruct.comp (self.μ self.η) h = h

μ applied to η is identity.

@[simp]

theorem CategoryTheory.RelativeMonad.assoc_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Functor C D} (self : RelativeMonad C D J) {X Y Z : C} (f : J.obj X ⟶ self.T Y) (g : J.obj Y ⟶ self.T Z) {Z✝ : D} (h : self.T Z ⟶ Z✝) : CategoryStruct.comp (self.μ (CategoryStruct.comp f (self.μ g))) h = CategoryStruct.comp (self.μ f) (CategoryStruct.comp (self.μ g) h)

μ is associative.

def CategoryTheory.RelativeMonad.inducedFunctor {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Functor C D} (M : RelativeMonad C D J) : Functor C D

The functor induced by a relative monad.

Note: this is not the same as the underlying functor of the relative monad.

@[simp]

theorem CategoryTheory.RelativeMonad.inducedFunctor_map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Functor C D} (M : RelativeMonad C D J) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : M.inducedFunctor.map f = M.μ (CategoryStruct.comp (J.map f) M.η)

@[simp]

theorem CategoryTheory.RelativeMonad.inducedFunctor_obj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Functor C D} (M : RelativeMonad C D J) (X : C) : M.inducedFunctor.obj X = M.T X

def CategoryTheory.RelativeMonad.inducedNatTrans {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Functor C D} (M : RelativeMonad C D J) : NatTrans J M.inducedFunctor

The natural transformation from the underlying functor of the relative monad, to the functor induced by the relative monad.

def CategoryTheory.RelativeMonad.monadOfId {C : Type u₁} [Category.{v₁, u₁} C] (M : RelativeMonad C C (Functor.id C)) : Monad C

If a relative monad is over the identity functor, it is a monad.

def CategoryTheory.RelativeMonad.ofNatIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J₁ J₂ : Functor C D} (φ : J₁ ≅ J₂) (M : RelativeMonad C D J₁) : RelativeMonad C D J₂

Transport a relative monad along a natural isomorphism of the underlying functor.

def CategoryTheory.RelativeMonad.precompose {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Functor C D} {C' : Type u₃} [Category.{v₃, u₃} C'] (J' : Functor C' C) (M : RelativeMonad C D J) : RelativeMonad C' D (J'.comp J)

Precompose a relative monad M : RelativeMonad C D J along a functor J' : C' ⥤ C.

def CategoryTheory.RelativeMonad.prod {C₁ : Type u₁} [Category.{v₁, u₁} C₁] {D₁ : Type u₂} [Category.{v₂, u₂} D₁] {C₂ : Type u₃} [Category.{v₃, u₃} C₂] {D₂ : Type u₄} [Category.{v₄, u₄} D₂] {J₁ : Functor C₁ D₁} {J₂ : Functor C₂ D₂} (M₁ : RelativeMonad C₁ D₁ J₁) (M₂ : RelativeMonad C₂ D₂ J₂) : RelativeMonad (C₁ × C₂) (D₁ × D₂) (J₁.prod J₂)

The product of two relative monads is a relative monad on the corresponding product categories.

@[simp]

theorem CategoryTheory.RelativeMonad.prod_μ {C₁ : Type u₁} [Category.{v₁, u₁} C₁] {D₁ : Type u₂} [Category.{v₂, u₂} D₁] {C₂ : Type u₃} [Category.{v₃, u₃} C₂] {D₂ : Type u₄} [Category.{v₄, u₄} D₂] {J₁ : Functor C₁ D₁} {J₂ : Functor C₂ D₂} (M₁ : RelativeMonad C₁ D₁ J₁) (M₂ : RelativeMonad C₂ D₂ J₂) {X✝ Y✝ : C₁ × C₂} (f : (J₁.prod J₂).obj X✝ ⟶ (M₁.T Y✝.1, M₂.T Y✝.2)) : (M₁.prod M₂).μ f = (M₁.μ f.1, M₂.μ f.2)

@[simp]

theorem CategoryTheory.RelativeMonad.prod_η {C₁ : Type u₁} [Category.{v₁, u₁} C₁] {D₁ : Type u₂} [Category.{v₂, u₂} D₁] {C₂ : Type u₃} [Category.{v₃, u₃} C₂] {D₂ : Type u₄} [Category.{v₄, u₄} D₂] {J₁ : Functor C₁ D₁} {J₂ : Functor C₂ D₂} (M₁ : RelativeMonad C₁ D₁ J₁) (M₂ : RelativeMonad C₂ D₂ J₂) {X✝ : C₁ × C₂} : (M₁.prod M₂).η = (M₁.η, M₂.η)

@[simp]

theorem CategoryTheory.RelativeMonad.prod_T {C₁ : Type u₁} [Category.{v₁, u₁} C₁] {D₁ : Type u₂} [Category.{v₂, u₂} D₁] {C₂ : Type u₃} [Category.{v₃, u₃} C₂] {D₂ : Type u₄} [Category.{v₄, u₄} D₂] {J₁ : Functor C₁ D₁} {J₂ : Functor C₂ D₂} (M₁ : RelativeMonad C₁ D₁ J₁) (M₂ : RelativeMonad C₂ D₂ J₂) (X : C₁ × C₂) : (M₁.prod M₂).T X = (M₁.T X.1, M₂.T X.2)

structure CategoryTheory.RelativeMonadHom {C : Type u₁} [Category.{v₁, u₁} C] {D₁ : Type u₂} [Category.{v₂, u₂} D₁] {D₂ : Type u₃} [Category.{v₃, u₃} D₂] {J₁ : Functor C D₁} {J₂ : Functor C D₂} (M₁ : RelativeMonad C D₁ J₁) (M₂ : RelativeMonad C D₂ J₂) : Type (max (max (max (max u₁ u₂) u₃) v₂) v₃)

A morphism of relative monads, where the two ending categories may be different. We require another functor & a natural isomorphism to correct for this discrepancy.

• J₁₂ : Functor D₁ D₂
• φ : J₂ ≅ J₁.comp self.J₁₂
• map {X : C} : self.J₁₂.obj (M₁.T X) ⟶ M₂.T X
• map_η {X : C} : CategoryStruct.comp (self.J₁₂.map M₁.η) self.map = CategoryStruct.comp (self.φ.inv.app X) M₂.η
• map_μ {X Y : C} (f : J₁.obj X ⟶ M₁.T Y) : CategoryStruct.comp (self.J₁₂.map (M₁.μ f)) self.map = CategoryStruct.comp self.map (M₂.μ (CategoryStruct.comp (self.φ.hom.app X) (CategoryStruct.comp (self.J₁₂.map f) self.map)))

@[simp]

theorem CategoryTheory.RelativeMonadHom.map_η_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D₁ : Type u₂} [Category.{v₂, u₂} D₁] {D₂ : Type u₃} [Category.{v₃, u₃} D₂] {J₁ : Functor C D₁} {J₂ : Functor C D₂} {M₁ : RelativeMonad C D₁ J₁} {M₂ : RelativeMonad C D₂ J₂} (self : RelativeMonadHom M₁ M₂) {X : C} {Z : D₂} (h : M₂.T X ⟶ Z) : CategoryStruct.comp (self.J₁₂.map M₁.η) (CategoryStruct.comp self.map h) = CategoryStruct.comp (self.φ.inv.app X) (CategoryStruct.comp M₂.η h)

@[simp]

theorem CategoryTheory.RelativeMonadHom.map_μ_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D₁ : Type u₂} [Category.{v₂, u₂} D₁] {D₂ : Type u₃} [Category.{v₃, u₃} D₂] {J₁ : Functor C D₁} {J₂ : Functor C D₂} {M₁ : RelativeMonad C D₁ J₁} {M₂ : RelativeMonad C D₂ J₂} (self : RelativeMonadHom M₁ M₂) {X Y : C} (f : J₁.obj X ⟶ M₁.T Y) {Z : D₂} (h : M₂.T Y ⟶ Z) : CategoryStruct.comp (self.J₁₂.map (M₁.μ f)) (CategoryStruct.comp self.map h) = CategoryStruct.comp self.map (CategoryStruct.comp (M₂.μ (CategoryStruct.comp (self.φ.hom.app X) (CategoryStruct.comp (self.J₁₂.map f) self.map))) h)

Old stuff below.

Turns out one cannot just work with Type u → Type v, since in the relational context, relative relational specification monad actually has signature Type u₁ × Type u₂ → Type v₁ × Type v₂. This means that we have to develop the general theory at the category-theoretic level.

class RelativePure (j : Type u → Type w) (f : Type u → Type v) : Type (max (max (u + 1) v) w)

Type class for the relative pure operation

• pureᵣ {α : Type u} : j α → f α

  The relative pure operation

class RelativeBind (j : Type u → Type w) (m : Type u → Type v) : Type (max (max (u + 1) v) w)

Type class for the relative bind operation

• bindᵣ {α β : Type u} : m α → (j α → m β) → m β

  The relative bind operation

class RelativeFunctor (j : Type u → Type w) (f : Type u → Type v) : Type (max (max (u + 1) v) w)

Type class for the relative map operation

• mapᵣ {α β : Type u} : (j α → j β) → f α → f β

  The relative map operation

• mapConstᵣ {α β : Type u} : j α → f β → f α

def «term_>>=ᵣ_» : Lean.TrailingParserDescr

The relative bind operation

def «term_<$>ᵣ_» : Lean.TrailingParserDescr

The relative map operation

class RelativeMonad (j : Type u → Type w) (m : Type u → Type v) extends RelativePure j m, RelativeBind j m, RelativeFunctor j m : Type (max (max (u + 1) v) w)

Type class for the relative monad

• pureᵣ {α : Type u} : j α → m α
• bindᵣ {α β : Type u} : m α → (j α → m β) → m β
• mapᵣ {α β : Type u} : (j α → j β) → m α → m β
• mapConstᵣ {α β : Type u} : j α → m β → m α

def instFunctorOfRelativeMonad {j : Type u → Type w} [Functor j] {m : Type u → Type v} [RelativeMonad j m] : Functor m

def instSeqOfRelativeMonadOfSeq {j : Type u → Type w} [Seq j] {m : Type u → Type v} [RelativeMonad j m] : Seq m

instance instPureOfRelativePureId {f : Type u → Type v} [RelativePure Id f] : Pure f

instance instBindOfRelativeBindId {m : Type u → Type v} [RelativeBind Id m] : Bind m

instance instFunctorOfRelativeFunctorId {f : Type u → Type v} [RelativeFunctor Id f] : Functor f

instance instMonadOfRelativeMonadId {m : Type u → Type v} [RelativeMonad Id m] : Monad m

class LawfulRelativeFunctor (j : Type u → Type w) (f : Type u → Type v) [RelativeFunctor j f] : Prop

• map_constᵣ {α β : Type u} : mapConstᵣ = mapᵣ ∘ Function.const (j β)
• id_mapᵣ {α : Type u} (x : f α) : id <$>ᵣ x = x
• comp_mapᵣ {α β γ : Type u} (g : j α → j β) (h : j β → j γ) (x : f α) : (h ∘ g) <$>ᵣ x = h <$>ᵣ g <$>ᵣ x

@[simp]

theorem id_mapᵣ' {j : Type u → Type w} {f : Type u → Type v} {α : Type u} [RelativeFunctor j f] [LawfulRelativeFunctor j f] (x : f α) : (fun (a : j α) => a) <$>ᵣ x = x

@[simp]

theorem RelativeFunctor.map_map {j : Type u → Type w} {f : Type u → Type v} {α β γ : Type u} [RelativeFunctor j f] [LawfulRelativeFunctor j f] (h : j α → j β) (g : j β → j γ) (x : f α) : g <$>ᵣ h <$>ᵣ x = (fun (a : j α) => g (h a)) <$>ᵣ x

class LawfulRelativeMonad (j : Type u → Type w) (m : Type u → Type v) [RelativeMonad j m] extends LawfulRelativeFunctor j m : Prop

• map_constᵣ {α β : Type u} : mapConstᵣ = mapᵣ ∘ Function.const (j β)
• id_mapᵣ {α : Type u} (x : m α) : id <$>ᵣ x = x
• comp_mapᵣ {α β γ : Type u} (g : j α → j β) (h : j β → j γ) (x : m α) : (h ∘ g) <$>ᵣ x = h <$>ᵣ g <$>ᵣ x
• pure_bindᵣ {α β : Type u} (x : j α) (f : j α → m β) : pureᵣ x >>=ᵣ f = f x
• bind_pure_compᵣ {α β : Type u} (f : j α → j β) (x : m α) : (x >>=ᵣ fun (y : j α) => pureᵣ (f y)) = f <$>ᵣ x
• bind_assocᵣ {α β γ : Type u} (x : m α) (f : j α → m β) (g : j β → m γ) : x >>=ᵣ f >>=ᵣ g = x >>=ᵣ fun (x : j α) => f x >>=ᵣ g

@[simp]

theorem bind_pureᵣ {j : Type u → Type w} {m : Type u → Type v} {α : Type u} [RelativeMonad j m] [LawfulRelativeMonad j m] (x : m α) : x >>=ᵣ pureᵣ = x

theorem map_eq_pure_bindᵣ {j : Type u → Type w} {m : Type u → Type v} {α β : Type u} [RelativeMonad j m] [LawfulRelativeMonad j m] (f : j α → j β) (x : m α) : f <$>ᵣ x = x >>=ᵣ fun (a : j α) => pureᵣ (f a)

theorem bind_congrᵣ {j : Type u → Type w} {m : Type u → Type v} {α β : Type u} [RelativeBind j m] {x : m α} {f g : j α → m β} (h : ∀ (a : j α), f a = g a) : x >>=ᵣ f = x >>=ᵣ g

theorem bind_pure_unitᵣ {j : Type u → Type w} {m : Type u → Type v} [RelativeMonad j m] [LawfulRelativeMonad j m] {x : m PUnit.{u + 1}} : (x >>=ᵣ fun (y : j PUnit.{u + 1}) => pureᵣ y) = x

theorem map_congrᵣ {j : Type u → Type w} {m : Type u → Type v} {α β : Type u} [RelativeFunctor j m] {x : m α} {f g : j α → j β} (h : ∀ (a : j α), f a = g a) : f <$>ᵣ x = g <$>ᵣ x

@[simp]

theorem map_bindᵣ {j : Type u → Type w} {m : Type u → Type v} {α β γ : Type u} [RelativeMonad j m] [LawfulRelativeMonad j m] (f : j β → j γ) (x : m α) (g : j α → m β) : f <$>ᵣ (x >>=ᵣ g) = x >>=ᵣ fun (a : j α) => f <$>ᵣ g a

@[simp]

theorem bind_map_leftᵣ {j : Type u → Type w} {m : Type u → Type v} {α β γ : Type u} [RelativeMonad j m] [LawfulRelativeMonad j m] (f : j α → j β) (x : m α) (g : j β → m γ) : (f <$>ᵣ x >>=ᵣ fun (b : j β) => g b) = x >>=ᵣ fun (a : j α) => g (f a)

theorem RelativeFunctor.map_unitᵣ {j : Type u → Type w} {m : Type u → Type v} [RelativeMonad j m] [LawfulRelativeMonad j m] {a : m PUnit.{u + 1}} : (fun (y : j PUnit.{u + 1}) => y) <$>ᵣ a = a

instance instLawfulFunctorOfLawfulRelativeFunctorId {f : Type u → Type v} [RelativeFunctor Id f] [LawfulRelativeFunctor Id f] : LawfulFunctor f

class MonadIso (m : Type u → Type v) (n : Type u → Type w) : Type (max (max (u + 1) v) w)

• toLift : MonadLiftT m n
• invLift : MonadLiftT n m
• monadLift_left_inv {α : Type u} : Function.LeftInverse monadLift monadLift
• monadLift_right_inv {α : Type u} : Function.RightInverse monadLift monadLift

class RelativeMonadMorphism (r₁ m₁ : Type u → Type v₁) (r₂ m₂ : Type u → Type v₂) [RelativeMonad r₁ m₁] [RelativeMonad r₂ m₂] : Type (max (max (u + 1) (v₁ + 1)) (v₂ + 1))

• r₁₂ : Type v₁ → Type v₂
• instFunctor : Functor (r₁₂ r₁ m₁ r₂ m₂)
• φ : MonadIso r₂ (r₁₂ r₁ m₁ r₂ m₂ ∘ r₁)
• mmapᵣ {α : Type u} : r₁₂ r₁ m₁ r₂ m₂ (m₁ α) → m₂ α
• mmapᵣ_pureᵣ {α : Type u} : mmapᵣ ∘ Functor.map pureᵣ = pureᵣ ∘ monadLift
• mmapᵣ_bindᵣ {α β : Type u} (f : r₁ α → m₁ β) : (mmapᵣ ∘ Functor.map fun (x : m₁ α) => x >>=ᵣ f) = (fun (x : m₂ α) => x >>=ᵣ mmapᵣ ∘ Functor.map f ∘ monadLift) ∘ mmapᵣ