Representable.lean

import Mathlib.CategoryTheory.RepresentedBy

open CategoryTheory
open Opposite
open scoped CategoryTheory

namespace Closure

/-!
# Exercises on representable functors

Mathlib では、反変関手 `F : Cᵒᵖ ⥤ Type _` が `Y : C` で表現されることを
`F.RepresentableBy Y` で表す。共変関手 `F : C ⥤ Type _` の `Hom(X, -)`
型の表現は `F.CorepresentableBy X` という名前になっている。

各演習では、直前に `#check` した定理そのものを使わずに、
構造体のフィールド、自然性、`yoneda` / `coyoneda` の定義、
以前の演習などから証明することを想定する。
-/

universe w v u

section RepresentableExercises

variable {C : Type u} [Category.{v} C]

/-!
## `RepresentableBy`
-/

-- Exercise 1 (Core):
-- `RepresentableBy` の値は、恒等射に対応する普遍元への作用で決まる。
--
-- Forbidden shortcut: `Functor.RepresentableBy.homEquiv_eq`.
-- Allowed tools: `Functor.RepresentableBy.homEquiv_comp`, category laws, basic rewrites.
-- Hint: `f = f ≫ 𝟙 Y` と見て、`homEquiv_comp` を適用する。
#check Functor.RepresentableBy.homEquiv_eq

example {F : Cᵒᵖ ⥤ Type v} {Y X : C} (R : F.RepresentableBy Y) (f : X ⟶ Y) :
    R.homEquiv f = F.map f.op (R.homEquiv (𝟙 Y)) := by
  sorry

-- Exercise 2 (Core):
-- `homEquiv.symm` は、`F.map` の作用を射の前合成に戻す。
--
-- Forbidden shortcut: `Functor.RepresentableBy.comp_homEquiv_symm`.
-- Allowed tools: `R.homEquiv.injective`, Exercise 1, `homEquiv_comp`, `simp`.
-- Hint: 両辺に `R.homEquiv` をかけて等しさを示す。
#check Functor.RepresentableBy.comp_homEquiv_symm

example {F : Cᵒᵖ ⥤ Type v} {Y X X' : C} (R : F.RepresentableBy Y)
    (x : F.obj (op X')) (f : X ⟶ X') :
    f ≫ R.homEquiv.symm x = R.homEquiv.symm (F.map f.op x) := by
  sorry

-- Exercise 3 (Preservation/Transport):
-- 自然同型 `F ≅ F'` に沿って、表現可能性の具体的データを移送する。
--
-- Forbidden shortcut: `Functor.RepresentableBy.ofIso`.
-- Allowed tools: `RepresentableBy` constructor, componentwise equivalences, naturality.
-- Hint: `(X ⟶ Y) ≃ F.obj (op X)` と `(e.app (op X)).toEquiv` を合成する。
#check Functor.RepresentableBy.ofIso

example {F F' : Cᵒᵖ ⥤ Type v} {Y : C} (R : F.RepresentableBy Y) (e : F ≅ F') :
    F'.RepresentableBy Y := by
  sorry

-- Exercise 4 (Preservation/Transport):
-- 表現対象を同型な対象に取り替えても、同じ関手を表現できる。
--
-- Forbidden shortcut: `Functor.RepresentableBy.ofIsoObj`.
-- Allowed tools: `RepresentableBy` constructor, `Iso.homToEquiv`, `R.homEquiv_comp`.
-- Hint: `(Z ⟶ Y) ≃ (Z ⟶ X)` を、対象同型 `e : Y ≅ X` との後合成で作る。
#check Functor.RepresentableBy.ofIsoObj

example {F : Cᵒᵖ ⥤ Type v} {X Y : C} (R : F.RepresentableBy X) (e : Y ≅ X) :
    F.RepresentableBy Y := by
  sorry

-- Exercise 5 (Construction):
-- `yoneda.obj X` は `X` 自身で表現される。
--
-- Forbidden shortcut: `Functor.RepresentableBy.yoneda`.
-- Allowed tools: `Functor.representableByEquiv`, `Iso.refl`, definitions of `yoneda`.
-- Hint: `yoneda.obj X ≅ yoneda.obj X` から `RepresentableBy` に戻す。
#check Functor.RepresentableBy.yoneda

example (X : C) : (yoneda.obj X).RepresentableBy X := by
  sorry

-- Exercise 6 (Bridge):
-- `RepresentableBy` は、`yoneda.obj Y ≅ F` と同じデータである。
--
-- Forbidden shortcut: `Functor.representableByEquiv`.
-- Allowed tools: `NatIso.ofComponents`, `Equiv.toIso`, naturality, `RepresentableBy` constructor.
-- Hint: 一方向は `R.homEquiv` を各成分にした自然同型、逆方向は
-- 自然同型の成分から `homEquiv` を取り出す。
#check Functor.representableByEquiv

example {F : Cᵒᵖ ⥤ Type v} {Y : C} :
    F.RepresentableBy Y ≃ (yoneda.obj Y ≅ F) := by
  sorry

-- Exercise 7 (Construction):
-- `yoneda.obj X ≅ F` があれば、`F` は表現可能である。
--
-- Forbidden shortcut: `Functor.IsRepresentable.mk'`.
-- Allowed tools: Exercise 6, `Functor.RepresentableBy.isRepresentable`.
-- Hint: 自然同型を `RepresentableBy` に変換してから、存在命題に包む。
#check Functor.IsRepresentable.mk'

example {F : Cᵒᵖ ⥤ Type v} {X : C} (e : yoneda.obj X ≅ F) :
    F.IsRepresentable := by
  sorry

-- Exercise 8 (Characterization):
-- 表現対象は同型を除いて一意である。
--
-- Forbidden shortcut: `Functor.RepresentableBy.uniqueUpToIso`.
-- Allowed tools: `Yoneda.ext`, Exercise 2, `homEquiv_comp`, basic `simp`.
-- Hint: 任意の `Z` について `(Z ⟶ Y) ≃ (Z ⟶ Y')` を作り、
-- Yoneda の外延性に渡す。
#check Functor.RepresentableBy.uniqueUpToIso

example {F : Cᵒᵖ ⥤ Type v} {Y Y' : C}
    (R : F.RepresentableBy Y) (R' : F.RepresentableBy Y') : Y ≅ Y' := by
  sorry

-- Exercise 9 (API Signpost):
-- `IsRepresentable` から Mathlib が選ぶ代表対象 `reprX` も、
-- 任意の表現対象と同型である。
--
-- Forbidden shortcut: `Functor.RepresentableBy.isoReprX`.
-- Allowed tools: Exercise 8, `F.representableBy`.
-- Hint: `R` と、`IsRepresentable` から選ばれた `F.representableBy` を
-- Exercise 8 に渡す。
#check Functor.RepresentableBy.isoReprX

example {F : Cᵒᵖ ⥤ Type v} [F.IsRepresentable] {Y : C} (R : F.RepresentableBy Y) :
    Y ≅ F.reprX := by
  sorry

-- Exercise 10 (API Signpost):
-- 表現可能な関手 `F` は、選ばれた代表対象から来る `yoneda` と
-- 同型である。
--
-- Forbidden shortcut: `Functor.reprW`.
-- Allowed tools: `Functor.RepresentableBy.toIso`, `F.representableBy`.
-- Hint: `F.representableBy : F.RepresentableBy F.reprX` を自然同型に変換する。
#check Functor.reprW

example (F : Cᵒᵖ ⥤ Type v) [F.IsRepresentable] :
    yoneda.obj F.reprX ≅ F := by
  sorry

-- Exercise 11 (Preservation/Transport):
-- `Type` の universe を `ULift` で上げても、表現可能性は変わらない。
--
-- Forbidden shortcut: `Functor.isRepresentable_comp_uliftFunctor_iff`.
-- Allowed tools: `Functor.representableByUliftFunctorEquiv`, existence unpacking.
-- Hint: `IsRepresentable` の中身の `∃ X, Nonempty (F.RepresentableBy X)` を開いて、
-- `representableByUliftFunctorEquiv` で往復する。
#check Functor.isRepresentable_comp_uliftFunctor_iff

example {F : Cᵒᵖ ⥤ Type v} :
    (F ⋙ uliftFunctor.{w}).IsRepresentable ↔ F.IsRepresentable := by
  sorry

/-!
## Universal elements
-/

-- Exercise 12 (Bridge):
-- 普遍元 `x` による表現 `IsRepresentedBy x` は、`RepresentableBy` と
-- `R.homEquiv (𝟙 X) = x` の組と同じである。
--
-- Forbidden shortcut: `Functor.IsRepresentedBy.iff_exists_representableBy`.
-- Allowed tools: `Functor.IsRepresentedBy.representableBy`,
-- `Functor.RepresentableBy.isRepresentedBy`, Exercise 1.
-- Hint: 左から右は `h.representableBy` を作る。右から左は等式で
-- 普遍元を置き換える。
#check Functor.IsRepresentedBy.iff_exists_representableBy

example {F : Cᵒᵖ ⥤ Type w} {X : C} {x : F.obj (op X)} :
    F.IsRepresentedBy x ↔ ∃ (R : F.RepresentableBy X), R.homEquiv (𝟙 X) = x := by
  sorry

-- Exercise 13 (Characterization):
-- 表現可能性は、ある対象と普遍元で表現されることと同値である。
--
-- Forbidden shortcut: `Functor.IsRepresentable.iff_exists_isRepresentedBy`.
-- Allowed tools: Exercise 12, `Functor.RepresentableBy.isRepresentable`,
-- `Functor.IsRepresentedBy.of_isRepresentable`.
-- Hint: `IsRepresentable` の代表対象と代表元 `reprx` を使う向きと、
-- `IsRepresentedBy.representableBy` から表現可能性を作る向きに分ける。
#check Functor.IsRepresentable.iff_exists_isRepresentedBy

example {F : Cᵒᵖ ⥤ Type w} :
    F.IsRepresentable ↔ ∃ (X : C) (x : F.obj (op X)), F.IsRepresentedBy x := by
  sorry

/-!
## `CorepresentableBy`

共変関手 `F : C ⥤ Type _` の `Hom(X, -)` 型の表現は、Mathlib では
`CorepresentableBy` と呼ばれる。反変版と双対的な形を確認する。
-/

-- Exercise 14 (Core):
-- 共変版では、普遍元からの写像は後合成と `F.map` で記述される。
--
-- Forbidden shortcut: `Functor.CorepresentableBy.homEquiv_eq`.
-- Allowed tools: `Functor.CorepresentableBy.homEquiv_comp`, category laws.
-- Hint: 反変版の Exercise 1 と同じだが、合成の向きが逆になる。
#check Functor.CorepresentableBy.homEquiv_eq

example {F : C ⥤ Type v} {X Y : C} (R : F.CorepresentableBy X) (f : X ⟶ Y) :
    R.homEquiv f = F.map f (R.homEquiv (𝟙 X)) := by
  sorry

-- Exercise 15 (Bridge):
-- `CorepresentableBy` は、`coyoneda.obj (op X) ≅ F` と同じデータである。
--
-- Forbidden shortcut: `Functor.corepresentableByEquiv`.
-- Allowed tools: `NatIso.ofComponents`, `Equiv.toIso`, naturality,
-- `CorepresentableBy` constructor.
-- Hint: Exercise 6 の双対版として、各成分の同値を自然同型に組み立てる。
#check Functor.corepresentableByEquiv

example {F : C ⥤ Type v} {X : C} :
    F.CorepresentableBy X ≃ (coyoneda.obj (op X) ≅ F) := by
  sorry

-- Exercise 16 (Construction):
-- `coyoneda.obj X` は `X.unop` で corepresent される。
--
-- Forbidden shortcut: `Functor.CorepresentableBy.coyoneda`.
-- Allowed tools: Exercise 15, `Iso.refl`, definitions of `coyoneda`.
-- Hint: `coyoneda.obj X ≅ coyoneda.obj X` から `CorepresentableBy` に戻す。
#check Functor.CorepresentableBy.coyoneda

example (X : Cᵒᵖ) : (coyoneda.obj X).CorepresentableBy X.unop := by
  sorry

end RepresentableExercises

end Closure