Adj.lean

import Mathlib

open CategoryTheory

section Conjugate

variable [Category X] [Category A] {F F' : X ⥤ A} {G G' : A ⥤ X}

def isConjugate (φ : F ⊣ G) (φ' : F'⊣ G') (σ : F ⟶ F') (τ : G' ⟶ G) :=
  ∀ (x : X) (a : A) (f : F'.obj x ⟶ a), (φ.homEquiv x a) (σ.app x ≫ f) = (φ'.homEquiv x a) f ≫ τ.app a


section properties
variable (φ : F ⊣ G) (φ' : F'⊣ G') (σ : F ⟶ F') (τ : G' ⟶ G)

def isConjugate.right_eq :=
  τ = whiskerLeft G' φ.unit ≫ whiskerRight (whiskerLeft G' σ) G ≫ whiskerRight φ'.counit G

def isConjugate.left_eq :=
  σ = whiskerRight φ'.unit F ≫ whiskerRight (whiskerLeft F' τ) F ≫ whiskerLeft F' φ.counit

def isConjugate.counit_comm :=
  whiskerRight τ F ≫ φ.counit = whiskerLeft G' σ ≫ φ'.counit

def isConjugate.unit_comm :=
  φ.unit ≫ whiskerRight σ G = φ'.unit ≫ whiskerLeft F' τ




lemma isConjugate.iff_right_eq :
  isConjugate φ φ' σ τ ↔ right_eq φ φ' σ τ
:= by
  unfold right_eq isConjugate
  constructor <;> intro H
  · ext a; simp
    have E := H (G'.obj a) (F'.obj (G'.obj a)) (𝟙 _); simp at E
    rw [φ.homEquiv_apply, φ'.homEquiv_apply] at E; simp at E
    rw [<- Category.assoc, E]; simp; clear E
    have E := τ.naturality ((φ'.counit.app a))
    conv at E => arg 2; simp
    rw [<- E, <- Category.assoc, φ'.right_triangle_components]
    simp
  · intro x a f
    rw [φ.homEquiv_apply, φ'.homEquiv_apply, H]; simp
    conv => arg 2; rw [<- Category.assoc, <- Category.assoc, Category.assoc _ (G'.map f)]
    have E := φ.unit.naturality (φ'.unit.app x ≫ G'.map f)
    conv at E => arg 1; simp
    rw [E, Category.assoc]; clear E
    conv => arg 2; arg 2; simp
    conv => arg 2; arg 1; simp
    rw [<- G.map_comp, <- G.map_comp, <- G.map_comp, <- G.map_comp]
    rw [<- Category.assoc, <- F.map_comp]
    have E := σ.naturality_assoc (φ'.unit.app x ≫ G'.map f) (φ'.counit.app a)
    rw [E]; clear E
    suffices : F'.map (φ'.unit.app x ≫ G'.map f) ≫ φ'.counit.app a = f; rw [this]; simp
    rw [F'.map_comp, Category.assoc]
    have E := φ'.counit.naturality f
    conv at E => arg 1; arg 1; simp
    rw [E, <- Category.assoc, φ'.left_triangle_components]
    simp

lemma isConjugate.iff_left_eq :
  isConjugate φ φ' σ τ ↔ left_eq φ φ' σ τ
:= by
  unfold left_eq isConjugate
  constructor <;> intro H
  · ext x; simp
    have E := H x (F'.obj x) (𝟙 _); simp at E
    rw [φ.homEquiv_apply, φ'.homEquiv_apply] at E; simp at E
    rw [<- Category.assoc, <- F.map_comp, <- E]
    rw [F.map_comp, Category.assoc]
    have E := φ.counit.naturality (σ.app x)
    rw [<- G.comp_map, E, <- Category.assoc, φ.left_triangle_components]
    simp
  · intro x a f; rw [H]; simp
    rw [φ.homEquiv_apply, φ'.homEquiv_apply]; simp

lemma isConjugate.iff_counit_comm :
  isConjugate φ φ' σ τ ↔ counit_comm φ φ' σ τ
:= by
  unfold counit_comm
  constructor <;> intro H
  · have Eσ := (iff_left_eq φ φ' σ τ).mp H
    unfold left_eq at Eσ
    have Eτ := (iff_right_eq φ φ' σ τ).mp H
    unfold right_eq at Eτ
    rw [Eσ, Eτ]
    ext a; simp
  · intro x a f
    have E := (φ.homEquiv x a).right_inv ((φ'.homEquiv x a) f ≫ τ.app a)
    rw [<- E]; clear E
    suffices : (σ.app x ≫ f) =((φ.homEquiv x a).invFun ((φ'.homEquiv x a) f ≫ τ.app a))
    rw [this]; simp
    simp
    rw [φ.homEquiv_symm_apply, φ'.homEquiv_apply]; simp
    injection H with H
    have Hx := congr_fun H (F'.obj x); simp at Hx
    suffices :
       σ.app x = F.map (φ'.unit.app x) ≫ F.map (τ.app (F'.obj x)) ≫ φ.counit.app (F'.obj x)
    rw [this]; simp
    rw [Hx, ]
    have := σ.naturality_assoc ((φ'.unit.app x)) (φ'.counit.app (F'.obj x))
    conv at this => arg 1; arg 2; arg 1; simp
    rw [this, φ'.left_triangle_components]
    simp

lemma isConjugate.iff_unit_comm :
  isConjugate φ φ' σ τ ↔ unit_comm φ φ' σ τ
:= by
  unfold unit_comm
  constructor <;> intro H
  · have Eσ := (iff_left_eq φ φ' σ τ).mp H
    unfold left_eq at Eσ
    have Eτ := (iff_right_eq φ φ' σ τ).mp H
    unfold right_eq at Eτ
    rw [Eσ, Eτ]
    ext x; simp
  · intro x a f
    have E := (φ.homEquiv x a).right_inv ((φ'.homEquiv x a) f ≫ τ.app a)
    rw [<- E]; clear E

    suffices : (σ.app x ≫ f) = ((φ.homEquiv x a).invFun ((φ'.homEquiv x a) f ≫ τ.app a))
    rw [this]; simp
    simp
    rw [φ.homEquiv_symm_apply, φ'.homEquiv_apply]; simp
    injection H with H
    have Hx := congr_fun H x; simp at Hx
    suffices :
       σ.app x = F.map (φ'.unit.app x) ≫ F.map (τ.app (F'.obj x)) ≫ φ.counit.app (F'.obj x)
    rw [this]; simp
    rw [<- Category.assoc, <- F.map_comp, <- Hx]
    simp

end properties

def isConjugate.right_mkby_left  (φ : F ⊣ G) (φ' : F'⊣ G') (σ : F ⟶ F') :
  G' ⟶ G
:= {
  app a := φ.homEquiv _ _ (σ.app (G'.obj a)) ≫ G.map (φ'.counit.app a)
  naturality {a a'} f := by
    rw [φ.homEquiv_apply, φ.homEquiv_apply]; simp
    rw [<- G.map_comp, <- G.map_comp, <- G.map_comp]
    have E := φ.unit.naturality (G'.map f)
    conv at E => arg 1; simp
    rw [<- Category.assoc, E]; clear E
    rw [Category.assoc, Functor.comp_map, <- G.map_comp]
    suffices :
      (F.map (G'.map f) ≫ σ.app (G'.obj a') ≫ φ'.counit.app a') =
      (σ.app (G'.obj a) ≫ φ'.counit.app a ≫ f); rw [this]
    have E := σ.naturality (G'.map f)
    rw [<- Category.assoc, E, Category.assoc]; clear E
    have E := φ'.counit.naturality f
    conv at E => arg 2; simp
    rw [<- E]; simp
}

lemma isConjugate.right_mkby_left_isConjugate
  (φ : F ⊣ G) (φ' : F'⊣ G') (σ : F ⟶ F') :
  isConjugate φ φ' σ (isConjugate.right_mkby_left φ φ' σ)
:= by
  rw [iff_right_eq]
  ext a; simp [right_mkby_left]
  rw [φ.homEquiv_apply]; simp


def isConjugate.left_mkby_right  (φ : F ⊣ G) (φ' : F'⊣ G') (τ : G' ⟶ G) :
  F ⟶ F' :=
{
  app x := F.map (φ'.unit.app x) ≫ (φ.homEquiv _ _).symm (τ.app (F'.obj x))
  naturality {x x'} f := by
    rw [φ.homEquiv_symm_apply, φ.homEquiv_symm_apply]; simp
    slice_lhs 1 3 => rw [<- F.map_comp, <- F.map_comp]
    have E := φ.counit.naturality (F'.map f)
    conv at E => arg 2; simp
    rw [<- E, Functor.comp_map]; clear E
    slice_rhs 1 3 => rw [<- F.map_comp, <- F.map_comp]
    have E := φ'.unit.naturality_assoc f (τ.app (F'.obj x'))
    conv at E => arg 1; simp
    rw [E]; clear E
    have E := τ.naturality (F'.map f)
    rw [<- E]; simp
}

lemma isConjugate.left_mkby_right_isConjugate
  (φ : F ⊣ G) (φ' : F'⊣ G') (τ : G' ⟶ G) :
  isConjugate φ φ' (isConjugate.left_mkby_right φ φ' τ) τ
:= by
  rw [iff_left_eq]
  ext x; simp [left_mkby_right]
  rw [φ.homEquiv_symm_apply]

structure Adj (X A : Type) [Category X] [Category A] where
  left : X ⥤ A
  right : A ⥤ X
  adj : left ⊣ right

@[ext]
structure Adj.Hom (X A : Type) [Category X] [Category A] (φ φ' : Adj X A) where
  left : φ.left ⟶ φ'.left
  right : φ'.right ⟶ φ.right
  isConj : isConjugate φ.adj φ'.adj left right


instance Adj.Category (X A : Type) [Category X] [Category A] : Category (Adj X A) where
  Hom := Adj.Hom X A
  id φ := {
    left := 𝟙 φ.left
    right := 𝟙 φ.right
    isConj := by
      intro x a f
      rw [φ.adj.homEquiv_apply, φ.adj.homEquiv_apply]
      simp
  }
  comp {φ φ' φ''} f g := {
    left := f.left ≫ g.left
    right := g.right ≫ f.right
    isConj := by
      intro x a h; simp
      have Hg := g.isConj x a h; simp at Hg
      rw [<- Category.assoc ((φ''.adj.homEquiv x a) h), <- Hg]
      have Hf := f.isConj x a (g.left.app x ≫ h)
      rw [Hf]
  }
  id_comp {φ φ'} f := by
    ext x<;> simp
  comp_id {φ φ'} f := by
    ext x<;> simp
  assoc {φ φ' φ'' φ'''} f g h := by
    ext x<;> simp



end Conjugate