Eilenberg-moore adjunction in Mathlib?

Stream: Is there code for X?

[Dean Young]

Does Mathlib have the Eilenberg Moore adjunction of a monad?

[Dean Young]

https://github.com/leanprover-community/mathlib4/blob/3d6112b5c7d095d3088b359c611a5a2704c5dbdc/Mathlib/CategoryTheory/Monad/Algebra.lean

[Scott Morrison]

Yes, line 186 of the file you link to!

[Dean Young]

I'm trying to switch to Mathlib's adjunctions since they seem pretty good. However I was wondering if there is already programmed in a way to obtain a proof the triangle identities from the Adjunction F G type. Like the two sorries at the end:

import Mathlib.CategoryTheory.Bicategory.Basic
import Mathlib.CategoryTheory.Types
import Mathlib.CategoryTheory.DiscreteCategory
import Mathlib.Combinatorics.Quiver.Basic
import Mathlib.CategoryTheory.Category.Init
--import Mathlib.CategoryTheory.Monad.Algebra
import Aesop
import Init
import Mathlib.CategoryTheory.DiscreteCategory
import Mathlib.CategoryTheory.Bicategory.Strict
import Mathlib.CategoryTheory.ConcreteCategory.Bundled
import Mathlib.CategoryTheory.Functor.Basic
import Init.Core
import Mathlib.CategoryTheory.Category.Cat
import Mathlib.CategoryTheory.Monad.Adjunction
import Mathlib.CategoryTheory.Monad.Algebra
import Mathlib.CategoryTheory.Monad.Monadicity
import Mathlib.CategoryTheory.Monad.Basic
universe u
universe v

open CategoryTheory


#check CategoryTheory.Bicategory.mk
#check CategoryTheory.Bicategory.Strict
#check CategoryTheory.Bicategory.Strict.mk
#check CategoryTheory.Functor
#check CategoryTheory.Functor.mk
#check CategoryTheory.CategoryStruct


def zero : Nat := 0


def reflexivity {X : Type} {x : X} : x = x := Eq.refl x


def symmetry {X : Type} {x : X} {y : X}  (p : x = y) := Eq.symm p


def transitivity {X : Type} {x : X} {y : X} {z : X} (p : x = y) (q : y = z) := Eq.trans p q


def extensionality (f g : X → Y) (p : (x:X) → f x = g x) : f = g := funext p


def equal_arguments {X : Type} {Y : Type} {a : X} {b : X} (f : X → Y) (p : a = b) : f a = f b := congrArg f p

def equal_functions {X : Type} {Y : Type} {f₁ : X → Y} {f₂ : X → Y} (p : f₁ = f₂) (x : X) : f₁ x = f₂ x := congrFun p x

def pairwise {A : Type} {B : Type} (a₁ : A) (a₂ : A) (b₁ : B) (b₂ : B) (p : a₁ = a₂) (q : b₁ = b₂) : (a₁,b₁)=(a₂,b₂) := (congr ((congrArg Prod.mk) p) q)


def ℂ𝕒𝕥 : (CategoryTheory.Bicategory CategoryTheory.Cat) := CategoryTheory.Cat.bicategory

#check ℂ𝕒𝕥

variable {C : Cat}
#check C.α
#check C.str
#check C.str.Hom

notation F "◁" η => ℂ𝕒𝕥.whiskerLeft F η
notation η "▷" F => ℂ𝕒𝕥.whiskerRight η F
#check ℂ𝕒𝕥.associator
#check ℂ𝕒𝕥.leftUnitor
#check ℂ𝕒𝕥.rightUnitor
#check ℂ𝕒𝕥.whiskerLeft_id
#check ℂ𝕒𝕥.whiskerLeft_comp
#check ℂ𝕒𝕥.id_whiskerLeft
#check ℂ𝕒𝕥.comp_whiskerLeft
#check ℂ𝕒𝕥.id_whiskerRight
#check ℂ𝕒𝕥.comp_whiskerRight
#check ℂ𝕒𝕥.whiskerRight_comp
#check ℂ𝕒𝕥.whiskerRight_id
#check ℂ𝕒𝕥.whisker_assoc
#check ℂ𝕒𝕥.whisker_exchange
#check ℂ𝕒𝕥.pentagon
#check ℂ𝕒𝕥.triangle

variable {C : Cat}
variable {D : Cat}
variable {Φ  :C ≅ D }
#check Φ.hom
#check Φ.inv
#check Φ.hom_inv_id
#check Φ.inv_hom_id

notation A "∘" B => B ≫ A
notation A "⭢" B => A ⟶ B

structure adjunction where
  Dom : Cat
  Cod : Cat
  Fst : Dom ⭢ Cod
  Snd : Cod ⭢ Dom
  η : (𝟙 Dom) ⭢ (Fst ≫ Snd)
  ε : (Snd ≫ Fst) ⭢ (𝟙 Cod)
  Id₁ : ((η ▷ Fst) ≫ (Fst ◁ ε)) = (𝟙 Fst)
  Id₂ : ((Snd ◁ η) ≫ (ε ▷ Snd)) = (𝟙 Snd)

variable {Dom : Cat}
variable {Cod : Cat}
variable {Fst : Dom ⭢ Cod}
variable {Snd : Cod ⭢ Dom}

def unit (Φ : Adjunction Fst Snd) : (𝟙 Dom) ⭢ (Fst ≫ Snd) := by
sorry

def counit (Φ : Adjunction Fst Snd) : (Snd ≫ Fst) ⭢ (𝟙 Cod) := by
sorry

def first_triangle (Φ : Adjunction Fst Snd) : ((η ▷ Fst) ≫ (Fst ◁ ε)) = (𝟙 Fst):= by
sorry

def second_triangle (Φ : Adjunction Fst Snd) : ((Snd ◁ η) ≫ (ε ▷ Snd)) = (𝟙 Snd) := by
sorry

[Adam Topaz]

docs#CategoryTheory.Adjunction.left_triangle

[Adam Topaz]

etc.