Equivalence.lean

import Mathlib.tactic

open CategoryTheory


example [Category X] [Category A] (φ : X ≌ A) :
  φ.functor ⊣ φ.inverse
:= {
  unit := φ.unitIso.hom
  counit := φ.counitIso.hom
  left_triangle_components := λ x => φ.functor_unitIso_comp x
  right_triangle_components := λ a => by
    have H := φ.symm.functor_unitIso_comp a
    unfold Equivalence.symm at H
    conv at H => arg 1; arg 1; simp
    conv at H => arg 1; arg 2; simp
    conv at H => arg 2; simp
    have H' := φ.functor_unitIso_comp (φ.inverse.obj a)
    rw [<- Category.id_comp (φ.unitIso.hom.app _)]
    simp only [Functor.id_obj]
    conv => arg 1; rw [<- H]
    rw [Category.assoc, Category.assoc, <- Category.assoc (φ.unitIso.inv.app _)]
    rw [φ.unitIso.inv_hom_id_app, Category.id_comp, <- φ.inverse.map_comp]
    rw [φ.counitIso.inv_hom_id_app]
    simp
}




#check Equivalence.fun_inv_map
example {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂}
  [Category.{v₂, u₂} D] (e : C ≌ D) (X Y : D) (f : X ⟶ Y) :
  e.functor.map (e.inverse.map f) = e.counit.app X ≫ f ≫ e.counitInv.app Y
:= by
  have E := e.counit.naturality f
  rw [Functor.id_map] at E
  rw [<- Category.assoc, <- E, Category.assoc, e.counitIso.hom_inv_id_app, Category.comp_id, Functor.comp_map]

#check Equivalence.inv_fun_map
example {C : Type u₁} [inst : Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : Category.{v₂, u₂} D] (e : C ≌ D) (X Y : C) (f : X ⟶ Y) :
  e.inverse.map (e.functor.map f) = e.unitInv.app X ≫ f ≫ e.unit.app Y
:= by
  have E := e.unit.naturality f
  rw [Functor.id_map] at E
  rw [E, <- Category.assoc]; clear E
  rw [e.unitIso.inv_hom_id_app X, Category.id_comp, Functor.comp_map]


#check Equivalence.fullyFaithfulFunctor
example [Category X] [Category A] (φ : X ≌ A) :
  φ.functor.FullyFaithful
:= {
  preimage {x x'} f:= φ.unitIso.hom.app x ≫ φ.inverse.map f ≫ φ.unitIso.inv.app x'
  map_preimage {x x'} f := by
    rw [Functor.map_comp, Functor.map_comp]
    rw [φ.fun_inv_map, Category.assoc, Category.assoc]
    rw [<- Category.assoc (φ.functor.map _), φ.functor_unitIso_comp, Category.id_comp]
    suffices : φ.counitInv.app (φ.functor.obj x') ≫ φ.functor.map (φ.unitIso.inv.app x') = 𝟙 (φ.functor.obj x')
    rw [this, Category.comp_id]

    simp
  preimage_map {x x'} g := by
    rw [φ.inv_fun_map]; simp
}

example [Category X] [Category A] (φ : X ≌ A) :
  ∀ a, ∃ c, Nonempty (a ≅ φ.functor.obj c)
:= by
  intro a
  let f := φ.counitInv.app a; simp at f
  let g := φ.counit.app a; simp at g
  use φ.inverse.obj a; constructor
  use f, g
  all_goals unfold autoParam; simp [f, g]

set_option maxHeartbeats 10000000
noncomputable example [Category X] [Category A] (F : X ⥤ A) (HF : F.FullyFaithful) (H : F.EssSurj ) : 
  Equivalence X A
:= by
  rcases HF with ⟨invMap, H1, H2⟩
  rcases H with ⟨H⟩
  choose f Hf using H
  refine {
    functor := F
    inverse := {
      obj := f
      map {a a'} g := invMap ((Hf a).some.hom ≫ g ≫ (Hf a').some.inv)
      map_id a := by
        set σ := (Hf a).some; simp
        rw [<- F.map_id, H2]
      map_comp {a₁ a₂ a₃} g h := by
        set σ₁ := (Hf a₁).some; set σ₂ := (Hf a₂).some; set σ₃ := (Hf a₃).some; simp
        nth_rw 1 [<- Category.comp_id g]
        rw [<- σ₂.inv_hom_id]
        rw [<- Category.assoc, <- Category.assoc, <- Category.assoc, <- Category.assoc, Category.assoc σ₁.hom]
        set g' := σ₁.hom ≫ g ≫ σ₂.inv; simp
        set h' := σ₂.hom ≫ h ≫ σ₃.inv
        rw [<- H2 (invMap g' ≫ invMap h'), F.map_comp, H1, H1]
    }
    counitIso := {
      hom := {
        app a := (Hf a).some.hom
        naturality {a a'} f := by
          simp; rw [H1]; simp
      }
      inv := {
        app a := (Hf a).some.inv
        naturality {a a'} f := by
          simp; rw [H1]; simp
      }
      hom_inv_id := by ext a; simp
      inv_hom_id := by ext a; simp
    }
    unitIso := {
      hom := {
        app x := invMap (Hf (F.obj x)).some.inv
        naturality {x x'} f := by
          simp
          set σ' := (Hf (F.obj x')).some
          set σ := (Hf (F.obj x)).some
          rw [<- H2 (invMap σ.inv ≫ invMap (σ.hom ≫ F.map f ≫ σ'.inv))]
          rw [F.map_comp, H1, H1, <- Category.assoc, <- Category.assoc]
          rw [σ.inv_hom_id, Category.id_comp]
          rw [<- H2 (f ≫ invMap σ'.inv), F.map_comp, H1]
      }
      inv := {
        app x := invMap (Hf (F.obj x)).some.hom
        naturality {x x'} f := by
          simp
          set σ' := (Hf (F.obj x')).some
          set σ := (Hf (F.obj x)).some
          rw [<- H2 (invMap σ.hom ≫ f), F.map_comp, H1]
          rw [<- H2 (invMap (σ.hom ≫ F.map f ≫ σ'.inv) ≫ invMap σ'.hom)]
          rw [F.map_comp, H1, H1]; simp
      }
      hom_inv_id := by
        ext x; simp
        set σ := (Hf (F.obj x)).some
        set σ' := (Hf (F.obj x)).some
        rw [<- H2 (invMap σ.inv ≫ invMap σ.hom), F.map_comp, H1, H1]
        rw [σ.inv_hom_id, <- F.map_id, H2]
      inv_hom_id := by
        ext x; simp
        set σ := (Hf (F.obj x)).some
        set σ' := (Hf (F.obj x)).some
        rw [<- H2 (invMap σ.hom ≫ invMap σ.inv), F.map_comp, H1, H1]
        rw [σ.hom_inv_id, <- F.map_id, H2]
    }
  }