AdjunctionMap.lean

import Mathlib.tactic

open CategoryTheory

lemma Functor.hcongr [Category X] [Category Y]
  {a b c d : X} {f : a ⟶ b} {g : c ⟶ d}
   (F : X ⥤ Y) (H : HEq f g) (Eac : a = c) (Ebd : b = d):
   HEq (F.map f) (F.map g)
:= by
  subst c d
  rcases H
  rfl

section Map

structure Adjunction.preMap
  [Category X] [Category X'] [Category A] [Category A']
  (F : X ⥤ A) (G : A ⥤ X) (F' : X' ⥤ A') (G' : A' ⥤ X')
where
  domMap : X ⥤ X'
  codMap : A ⥤ A'
  left_comm : F ⋙ codMap = domMap ⋙ F'
  right_comm : G ⋙ domMap = codMap ⋙ G'

section cast
variable [Category X] [Category X'] [Category A] [Category A']
variable {F : X ⥤ A} {F' : X' ⥤ A'} {G : A ⥤ X} {G' : A' ⥤ X'}
variable (M : Adjunction.preMap F G F' G')

lemma Adjunction.preMap.left_comm_obj (x : X) :
M.codMap.obj (F.obj x) = F'.obj (M.domMap.obj x) := by
  rw [<- Functor.comp_obj, M.left_comm, Functor.comp_obj]

lemma Adjunction.preMap.right_comm_obj (a : A) :
M.domMap.obj (G.obj a) = G'.obj (M.codMap.obj a) := by
  rw [<- Functor.comp_obj, M.right_comm, Functor.comp_obj]

lemma Adjunction.preMap.domMap_comm :
  F ⋙ G ⋙ M.domMap = M.domMap ⋙ F' ⋙ G'
:= by
  rw [M.right_comm, <- Functor.assoc, M.left_comm, Functor.assoc]

lemma Adjunction.preMap.codMap_comm :
  G ⋙ F ⋙ M.codMap = M.codMap ⋙ G' ⋙ F'
:= by
  rw [M.left_comm, <- Functor.assoc, M.right_comm, Functor.assoc]

variable (φ : F ⊣ G) (φ' : F' ⊣ G')

def Adjunction.preMap.unit_comm :=
  (whiskerRight φ.unit M.domMap) = (whiskerLeft M.domMap φ'.unit) ≫ (eqToHom M.domMap_comm.symm)

def Adjunction.preMap.counit_comm :=
  (whiskerRight φ.counit M.codMap) = (eqToHom M.codMap_comm) ≫ (whiskerLeft M.codMap φ'.counit)

def Adjunction.preMap.homEquiv_comm (x : X) (a : A) (f : F.obj x ⟶ a) :=
  (M.domMap.map ((φ.homEquiv x a) f)) ≫ eqToHom (M.right_comm_obj a) =
  ((φ'.homEquiv (M.domMap.obj x) (M.codMap.obj a))) (((eqToHom (M.left_comm_obj x).symm) ≫ (M.codMap.map f)))



lemma Adjunction.preMap.homEquiv_comm_iff_unit_comm :
  (∀ x a f , M.homEquiv_comm φ φ' x a f) ↔ M.unit_comm φ φ'
:= by
  unfold homEquiv_comm unit_comm
  constructor<;> intro H
  · ext x; simp
    have Hx := H x (F.obj x) (𝟙 (F.obj x)); simp at Hx
    rw [φ.homEquiv_id x] at Hx
    have E :
      M.domMap.map (φ.unit.app x) ≫ eqToHom (right_comm_obj M (F.obj x)) ≫ eqToHom (right_comm_obj M (F.obj x)).symm =
      (φ'.homEquiv (M.domMap.obj x) (M.codMap.obj (F.obj x))) (eqToHom (homEquiv_comm._proof_2 M x)) ≫ eqToHom (right_comm_obj M (F.obj x)).symm
      := by rw [<- Hx]; simp
    simp at E; rw [E]; clear E
    rw [<- (φ'.homEquiv_id (M.domMap.obj x))]
    congr<;> try rw [M.left_comm_obj]
    · exact eqToHom_heq_id_dom _ _ (homEquiv_comm._proof_2 M x)
    · apply proof_irrel_heq
    · rw [<- Functor.comp_obj, <- Functor.comp_obj, domMap_comm]; simp
    · rw [<- Functor.comp_obj, <- Functor.comp_obj, domMap_comm]; simp
  · intro x a f
    rw [φ.homEquiv_apply, φ'.homEquiv_apply]; simp
    injection H with H
    have Hx := congr_fun H x; simp at Hx; clear H
    rw [Hx]; simp; clear Hx

    suffices :
      eqToHom (Functor.congr_obj (unit_comm._proof_1 M) x) ≫
      M.domMap.map (G.map f) ≫ eqToHom (right_comm_obj M a) =
      G'.map (eqToHom (homEquiv_comm._proof_2 M x)) ≫ G'.map (M.codMap.map f); rw [this]
    apply eq_of_heq
    apply HEq.trans; apply eqToHom_comp_heq
    apply HEq.trans; apply comp_eqToHom_heq
    rw [<- Functor.comp_map]
    apply HEq.trans
    · show HEq ((G ⋙ M.domMap).map f) ((M.codMap ⋙ G').map f)
      apply Functor.hcongr_hom
      exact M.right_comm
    · simp
      rw [<- G'.map_comp]
      have E := (eqToHom_comp_heq (M.codMap.map f) (homEquiv_comm._proof_2 M x)).symm
      apply Functor.hcongr G' E ?_ rfl
      exact M.left_comm_obj x

-- 双対だし、いつかやればいいや
-- lemma Adjunction.preMap.homEquiv_comm_iff_counit_comm :
--   (∀ x a f, M.homEquiv_comm φ φ' x a f) ↔ M.counit_comm φ φ'
-- := by
--   sorry

end cast

structure Adjunction.Map
  [Category X] [Category X'] [Category A] [Category A']
  {F : X ⥤ A} {F' : X' ⥤ A'} {G : A ⥤ X} {G' : A' ⥤ X'}
  (φ : F ⊣ G) (φ' : F' ⊣ G') extends M : Adjunction.preMap F G F' G' where
  homEquiv_comm (x : X) (a : A) (f : F.obj x ⟶ a) : M.homEquiv_comm φ φ' x a f


end Map