Equiv.lean

import Mathlib.tactic
open CategoryTheory

-- F.Full := Function.Surjective F.map
-- F.Faithful := Function.Injective F.map
-- F.FullyFaithful := Function.Bijective F.map


structure equiv (𝓐 𝓑 : Type) [Category 𝓐] [Category 𝓑] where
  func : 𝓐 ⥤ 𝓑
  inv : 𝓑 ⥤ 𝓐
  unit : Functor.id 𝓐 ≅ func ⋙ inv
  counit : inv ⋙ func ≅ Functor.id 𝓑
  triangle : (whiskerRight unit.hom func) ≫ (whiskerLeft func counit.hom) =  𝟙 func



def isEquiv [Category 𝓐] [Category 𝓑] (func : 𝓐 ⥤ 𝓑) : Prop :=
  ∃ inv : 𝓑 ⥤ 𝓐,
  ∃ unit : Functor.id 𝓐 ≅ func ⋙ inv,
  ∃ counit : inv ⋙ func ≅ Functor.id 𝓑,
    ((whiskerRight unit.hom func) ≫ (whiskerLeft func counit.hom) =  𝟙 func)

def isDense [Category 𝓐] [Category 𝓑] (F : 𝓐 ⥤ 𝓑) : Prop :=
  ∀ B : 𝓑, ∃ A : 𝓐, ∃ θ : F.obj A ⟶ B, IsIso θ


set_option maxHeartbeats 10000000
lemma equiv_iff [Category 𝓐] [Category 𝓑] (func : 𝓐 ⥤ 𝓑) :
  isEquiv func ↔
  (func.Full ∧ func.Faithful ∧ isDense func)
:= by
  constructor<;> intro H
  · rcases H with ⟨inv, μ, ε, triangle⟩
    constructor
    · constructor
      intro A A' f
      let g := μ.hom.app A; simp at g
      let f' := inv.map f
      let h := μ.inv.app A'; simp at h
      have Hg := μ.hom.naturality; simp at Hg
      use g ≫ f' ≫ h
      simp [g, f', h]
      injection triangle with H
      have E := congr_fun H A'; simp at E
      rw [<- Category.comp_id (func.map (μ.inv.app A'))]
      conv => arg 1; arg 2; arg 2; arg 2; simp
      rw [<- E, <- Category.assoc, <- Category.assoc (func.map (μ.inv.app A'))]
      clear E
      rw [<- func.map_comp, <- func.map_comp]
      simp
      have E := ε.hom.naturality f; simp at E
      rw [E, <- Category.assoc]; clear E
      have E := congr_fun H A; simp at E
      rw [E, Category.id_comp]
    constructor
    · constructor; unfold autoParam
      intro A A' f g H
      have Hf := μ.hom.naturality f; simp at Hf
      have E : f = μ.hom.app A ≫ inv.map (func.map f) ≫ μ.inv.app A' := by {
        rw [<- Category.assoc, <- Hf]; simp
      }
      rw [E, H]; clear E
      have E := μ.inv.naturality g; simp at E
      rw [E]; simp
    · unfold isDense
      intro B
      use (inv.obj B)
      use ε.hom.app B, ε.inv.app B
      simp
  · rcases H with ⟨⟨H1⟩, ⟨H2⟩, H3⟩
    unfold isDense at H3
    refine ⟨?_, ?_, ?_, ?_⟩
    · let obj (B : 𝓑) : 𝓐 := (H3 B).choose
      refine ⟨⟨obj, ?_⟩, ?_, ?_⟩
      · intro B B' g
        simp [obj]
        have HB := H3 B
        have HB' := H3 B'
        set A := HB.choose
        set A' := HB'.choose
        let θ : func.obj A ⟶ B := HB.choose_spec.choose
        let θ' : B' ⟶ func.obj A' := HB'.choose_spec.choose_spec.out.choose
        let h := (H1 (θ ≫ g ≫ θ')).choose
        exact h
      · intro B; simp
        let HB := H3 B
        set A := HB.choose
        set θ := HB.choose_spec.choose
        set θ' := HB.choose_spec.choose_spec.out.choose
        have E : θ ≫ θ' = _ := HB.choose_spec.choose_spec.out.choose_spec.1
        set H := (H1 (θ ≫ θ'))
        set h := H.choose
        have Hh : func.map h = θ ≫ θ' := H.choose_spec
        apply H2
        rw [Hh, E]; simp
      · intro B B' B'' f g; simp
        have HB := H3 B
        have HB' := H3 B'
        have HB'' := H3 B''
        set A := HB.choose
        set A' := HB'.choose
        set A'' := HB''.choose
        let θ : func.obj A ⟶ B := HB.choose_spec.choose
        let θ' : B' ⟶ func.obj A' := HB'.choose_spec.choose_spec.out.choose
        let σ : func.obj A' ⟶ B' := HB'.choose_spec.choose
        let σ' : B'' ⟶ func.obj A'' := HB''.choose_spec.choose_spec.out.choose
        have Hh := (H1 (θ ≫ f ≫ θ'))
        have Hh' := (H1 (σ ≫ g ≫ σ'))
        have Hh'' := (H1 (θ ≫ f ≫ g ≫ σ'))
        set h := Hh.choose
        set h' := Hh'.choose
        set h'' := Hh''.choose
        apply H2; simp
        rw [Hh.choose_spec, Hh'.choose_spec, Hh''.choose_spec]
        simp
        nth_rw 2 [<- Category.assoc _ _ (g ≫ σ')]
        have := HB'.choose_spec.choose_spec.out.choose_spec.2
        rw [this]; simp
    · simp
      refine ⟨?_, ?_, ?_, ?_⟩
      · refine ⟨?_, ?_⟩
        · intro A; simp
          have HA := H3 (func.obj A)
          let θ := HA.choose_spec.choose_spec.out.choose
          use (H1 θ).choose
        · intro A A' f; simp
          have HA := H3 (func.obj A)
          have HA' := H3 (func.obj A')
          let θ := HA.choose_spec.choose_spec.out.choose
          let θ' := HA'.choose_spec.choose_spec.out.choose
          have H := (H1 θ)
          have H' := (H1 θ')
          set F := H.choose
          set F' := H'.choose

          set σ  := HA.choose_spec.choose
          have E : θ ≫ σ = _ := HA.choose_spec.choose_spec.out.choose_spec.2
          set H0 := (H1 (σ ≫ func.map f ≫ θ'))
          have Hg := H0.choose_spec
          set g := H0.choose
          apply H2; simp
          rw [H.choose_spec, H'.choose_spec, Hg, <- Category.assoc, E]
          simp
      · refine ⟨?_, ?_⟩
        · intro A; simp
          have HA := H3 (func.obj A)
          let θ := HA.choose_spec.choose
          use (H1 θ).choose
        · intro A A' f; simp
          have HA := H3 (func.obj A)
          have HA' := H3 (func.obj A')
          let θ := HA.choose_spec.choose
          let θ' := HA'.choose_spec.choose
          have H := (H1 θ)
          have H' := (H1 θ')
          set F := H.choose
          set F' := H'.choose

          let H0 := HA'.choose_spec.choose_spec.out
          have E := H0.choose_spec
          set σ  := H0.choose

          have E0 := H1 (θ ≫ func.map f ≫ σ)
          have Hg := E0.choose_spec
          set g := E0.choose

          apply H2; simp
          rw [H.choose_spec, H'.choose_spec, Hg, Category.assoc, Category.assoc, E.2]
          simp
      · simp
        ext A; simp
        have HA := H3 (func.obj A)
        have Hθ := HA.choose_spec.choose_spec
        set θ := HA.choose_spec.choose
        set θ' := Hθ.out.choose
        have H0 := H1 θ'
        have Hσ := H0.choose_spec
        set σ := H0.choose
        have H0' := H1 θ
        have Hσ' := H0'.choose_spec
        set σ' := H0'.choose
        apply H2; simp
        rw [Hσ, Hσ']
        have E := Hθ.out.choose_spec.2
        rw [E]
      · ext A
        dsimp
        have HA := H3 (func.obj A)
        have Hθ := HA.choose_spec.choose_spec
        set θ := HA.choose_spec.choose
        set θ' := Hθ.out.choose
        have H0 := H1 θ'
        have Hσ := H0.choose_spec
        set σ := H0.choose
        have H0' := H1 θ
        have Hσ' := H0'.choose_spec
        set σ' := H0'.choose
        apply H2; simp
        rw [Hσ, Hσ']
        have E := Hθ.out.choose_spec.1
        rw [E]
    · simp
      refine ⟨?_, ?_, ?_, ?_⟩
      · refine ⟨?_, ?_⟩
        · intro B; simp
          use (H3 B).choose_spec.choose
        · intro B B' f
          dsimp
          have HB := H3 B
          have HB' := H3 B'
          set A := HB.choose
          set A' := HB'.choose
          have Hθ := HB.choose_spec.choose_spec
          have Hσ := HB'.choose_spec.choose_spec
          have Eσ := Hσ.out.choose_spec.2
          set θ : func.obj A ⟶ B := HB.choose_spec.choose
          set σ  := HB'.choose_spec.choose
          conv => arg 1; arg 2; change σ
          set σ' := HB'.choose_spec.choose_spec.out.choose
          have E := (H1 (θ ≫ f ≫ σ')).choose_spec
          set g := (H1 (θ ≫ f ≫ σ')).choose
          rw [E]
          rw [<- Category.assoc, Category.assoc, Eσ, Category.comp_id]
      · refine ⟨?_, ?_⟩
        · intro B; dsimp
          use (H3 B).choose_spec.choose_spec.out.choose
        · intro B B' f
          dsimp
          have HB := H3 B
          have HB' := H3 B'
          set A := HB.choose
          set A' := HB'.choose
          have Hθ := HB.choose_spec.choose_spec
          have Hσ := HB'.choose_spec.choose_spec
          set θ  := HB.choose_spec.choose
          set σ  := HB'.choose_spec.choose
          set θ' := Hθ.out.choose
          set σ' := Hσ.out.choose
          let h := θ ≫ f ≫ σ'
          have Hh := H1 h
          have E := Hh.choose_spec
          set h' := Hh.choose
          rw [E]; simp [h]
          rw [<- Category.assoc]
          rw [Hθ.out.choose_spec.2, Category.id_comp]
      · ext B; dsimp
        have HB := H3 B
        set θ := HB.choose_spec.choose
        set θ' := HB.choose_spec.choose_spec.out.choose
        have := HB.choose_spec.choose_spec.out.choose_spec.1
        rw [this]
      · ext B
        unfold NatTrans.app
        dsimp
        have HB := H3 B
        have := HB.choose_spec.choose_spec.out.choose_spec.2
        set θ := HB.choose_spec.choose
        set θ' := HB.choose_spec.choose_spec.out.choose
        rw [this]
    · ext A; simp
      have HA := H3 (func.obj A)
      set Hθ := HA.choose_spec.choose_spec
      have Eθ := Hθ.out.choose_spec.2
      set θ := HA.choose_spec.choose
      set θ' := HA.choose_spec.choose_spec.out.choose
      have E := (H1 θ').choose_spec
      set σ := (H1 θ').choose
      rw [E, Eθ]