U : 𝓐 ⥤ 𝓑 が右随伴である事、 任意のBについてHom(B, U -)が表現可能である事、の同値性を証明

Adj_Represendtable.lean

import Mathlib

open CategoryTheory

example [Category 𝓐] [Category 𝓑] (U : 𝓐 ⥤ 𝓑) :
  U.IsRightAdjoint ↔  ∀ B : 𝓑, (U ⋙ coyoneda.obj (Opposite.op B)).IsCorepresentable
:= by
  constructor<;> intro H
  · rcases H with ⟨F, ⟨σ⟩⟩
    intro B; constructor
    use F.obj B; constructor
    refine {
      homEquiv := by
        intro A; simp
        exact σ.homEquiv B A
      homEquiv_comp {A A'} f g := by
        simp
        rw [σ.homEquiv_apply, σ.homEquiv_apply, U.map_comp, Category.assoc]
    }
  ·
    let F : 𝓑 ⥤ 𝓐 := {
      obj B := (H B).has_corepresentation.choose
      map {B B'} f :=
        (H B).has_corepresentation.choose_spec.some.homEquiv.symm
          (f ≫ (H B').has_corepresentation.choose_spec.some.homEquiv
                (𝟙 (H B').has_corepresentation.choose)
          )
      map_id B := by simp
      map_comp {B₁ B₂ B₃} f g := by
        simp
        let HB₁ := (H B₁).has_corepresentation
        let HB₂ := (H B₂).has_corepresentation
        let HB₃ := (H B₃).has_corepresentation
        let σ₁ := HB₁.choose_spec.some
        let σ₂ := HB₂.choose_spec.some
        let σ₃ := HB₃.choose_spec.some
        let A₁ := HB₁.choose
        let A₂ := HB₂.choose
        let A₃ := HB₃.choose

        set L : A₁ ⟶ A₂ := σ₁.homEquiv.symm (f ≫ σ₂.homEquiv (𝟙 A₂))
        set R : A₂ ⟶ A₃ := σ₂.homEquiv.symm (g ≫ σ₃.homEquiv (𝟙 A₃))
        set F : A₁ ⟶ A₃ := σ₁.homEquiv.symm (f ≫ g ≫ σ₃.homEquiv (𝟙 A₃))
        change F = L ≫ R
        have E :=  σ₁.homEquiv_comp R L; simp at E
        have := (σ₁.homEquiv (Y := A₃)).left_inv (L ≫ R)
        rw [<- this]; clear this
        conv => arg 2; arg 2; simp; rw [E]
        simp; clear E
        conv => arg 2; arg 2; arg 1; simp [L]; change σ₁.homEquiv.toFun (σ₁.homEquiv.invFun (f ≫ σ₂.homEquiv (𝟙 A₂)))
        have E := σ₁.homEquiv.right_inv (f ≫ σ₂.homEquiv (𝟙 A₂))
        rw [E]; simp [F]; clear E
        have E := σ₂.homEquiv_comp R (𝟙 A₂); simp at E
        rw [<- E, Category.id_comp]
        simp only [R]; simp
        have := σ₂.homEquiv.right_inv (g ≫ σ₃.homEquiv (𝟙 A₃)); simp at this
        nth_rw 1 [<- this]
    }
    constructor; use F; constructor
    refine {
      unit := {
        app B :=
          (H B).has_corepresentation.choose_spec.some.homEquiv
          (𝟙 (H B).has_corepresentation.choose)
        naturality {B B'} f := by
          simp [F]
          set HB := (H B).has_corepresentation.choose_spec
          set HB' := (H B').has_corepresentation.choose_spec
          let A := (H B).has_corepresentation.choose
          let A' := (H B').has_corepresentation.choose
          change f ≫ HB'.some.homEquiv (𝟙 A') = HB.some.homEquiv (𝟙 A) ≫ U.map (HB.some.homEquiv.symm (f ≫ HB'.some.homEquiv (𝟙 A')))
          set R := (HB.some.homEquiv.symm (f ≫ HB'.some.homEquiv (𝟙 A')))
          have E := HB.some.homEquiv_comp R (𝟙 A); simp at E
          rw [Category.id_comp] at E
          conv at E => arg 1; simp [R]; change HB.some.homEquiv.toFun (HB.some.homEquiv.invFun (f ≫ HB'.some.homEquiv (𝟙 A')))
          have := HB.some.homEquiv.right_inv (f ≫ HB'.some.homEquiv (𝟙 A'))
          rw [this] at E
          rw [E]; rfl
      }
      counit := {
        app A := ((H (U.obj A)).has_corepresentation.choose_spec.some.homEquiv (Y := A)).symm (𝟙 _)
        naturality {A A'} f := by
          simp [F]
          set HA := (H (U.obj A)).has_corepresentation.choose_spec
          set HA' := (H (U.obj A')).has_corepresentation.choose_spec
          let B' := (H (U.obj A')).has_corepresentation.choose
          let B := (H (U.obj A)).has_corepresentation.choose
          conv => arg 1; arg 1; arg 2; arg 2; arg 2; change 𝟙 B'
          let L : B ⟶ B' :=  HA.some.homEquiv.symm (U.map f ≫ HA'.some.homEquiv (𝟙 B'))
          let R : B' ⟶ A' := HA'.some.homEquiv.symm (𝟙 (U.obj A'))
          change L ≫ R = _

          have E := HA.some.homEquiv_comp R L; simp at E
          have := HA.some.homEquiv.left_inv (L ≫ R)
          conv => arg  1; rw [<- this]; arg 2; simp; rw [E]; arg 1; simp [L]; change HA.some.homEquiv.toFun (HA.some.homEquiv.invFun (U.map f ≫ HA'.some.homEquiv (𝟙 B')))
          clear this E
          have E := HA.some.homEquiv.right_inv (U.map f ≫ HA'.some.homEquiv (𝟙 B'))
          rw [E]; simp; clear E
          have E := HA'.some.homEquiv_comp R (𝟙 B'); simp at E
          rw [<- E, Category.id_comp]; simp [R]; clear E
          conv => arg 1; arg 2; arg 2; change HA'.some.homEquiv.toFun (HA'.some.homEquiv.invFun (𝟙 (U.obj A')))
          have E := HA'.some.homEquiv.right_inv (𝟙 (U.obj A')); rw [E, Category.comp_id]; clear E
          have E := HA.some.homEquiv_comp f (HA.some.homEquiv.symm (𝟙 (U.obj A))); simp at E
          conv at E => arg 2; arg 1; change HA.some.homEquiv.toFun (HA.some.homEquiv.invFun (𝟙 (U.obj A)))
          have := HA.some.homEquiv.right_inv (𝟙 (U.obj A)); rw [this] at E; clear this; simp at E
          apply (Equiv.symm_apply_eq HA.some.homEquiv).mpr
          rw [<- E]; simp
      }
      left_triangle_components B := by
        simp [F]
        set HB := (H B).has_corepresentation.choose_spec
        set HB' := (H (U.obj (F.obj B))).has_corepresentation.choose_spec
        let A := (H B).has_corepresentation.choose
        let A' := (H (U.obj (F.obj B))).has_corepresentation.choose
        change HB.some.homEquiv.symm (HB.some.homEquiv (𝟙 A) ≫ HB'.some.homEquiv (𝟙 A')) ≫ HB'.some.homEquiv.symm (𝟙 (U.obj A)) = 𝟙 A
        set L : A ⟶ A' :=  HB.some.homEquiv.symm (HB.some.homEquiv (𝟙 A) ≫ HB'.some.homEquiv (𝟙 A'))
        set R : A' ⟶ A := HB'.some.homEquiv.symm (𝟙 (U.obj A))
        have E := HB.some.homEquiv.left_inv (L ≫ R)
        have E' := HB.some.homEquiv_comp R L; simp at E'
        conv => arg 1; rw [<- E]; arg 2; simp; rw [E']; simp [L]; simp
        clear E E'
        set F := (HB.some.homEquiv (𝟙 A) ≫ HB'.some.homEquiv (𝟙 A'))
        have E := HB.some.homEquiv.right_inv F; dsimp at F
        conv => arg 1; arg 2; arg 1; change HB.some.homEquiv.toFun (HB.some.homEquiv.invFun F); rw [E]
        simp [F]; clear E F
        have E := HB'.some.homEquiv_comp R (𝟙 A') ; simp at E
        rw [<- E, Category.id_comp]; simp [R]; clear E
        have E := HB'.some.homEquiv.right_inv (𝟙 (U.obj A)); dsimp at E
        rw [E]; simp
      right_triangle_components A := by
        simp
        set σ := (H (U.obj A)).has_corepresentation.choose_spec.some
        let B := (H (U.obj A)).has_corepresentation.choose
        conv => arg 1; arg 1; arg 2; change 𝟙 B
        have E := σ.homEquiv_comp ((σ.homEquiv.symm (𝟙 (U.obj A)))) (𝟙 B); simp at E
        rw [<- E, Category.id_comp]; clear E
        have E := σ.homEquiv.right_inv (𝟙 (U.obj A)); dsimp at E
        rw [E]
    }