第73章：局所デカルト閉圏——依存積を再添字付けの右随伴として捉える#

namespace FormalLab.Bridges.LocallyCartesianClosedCategories

universe u

abbrev Family (I : Type u) := I → Type u

abbrev FamilyHom {I : Type u} (A B : Family I) := ∀ i, A i → B i

def reindexFamily {I J : Type u} (f : I → J) (A : Family J) : Family I :=
  fun i => A (f i)

theorem reindexFamily_id {I : Type u} (A : Family I) :
    reindexFamily id A = A := rfl

theorem reindexFamily_comp {I J K : Type u} (f : I → J) (g : J → K) (A : Family K) :
    reindexFamily f (reindexFamily g A) = reindexFamily (g ∘ f) A := rfl

structure SigmaFiber {I J : Type u} (f : I → J) (B : Family I) (j : J) where
  index : I
  value : B index
  equation : f index = j

def sigmaFamily {I J : Type u} (f : I → J) (B : Family I) : Family J :=
  fun j => SigmaFiber f B j

def transportFamily {I : Type u} {A : Family I} {i : I} :
    ∀ {j : I}, i = j → A i → A j
  | _, rfl => id

def sigmaToReindex {I J : Type u} {f : I → J} {B : Family I} {A : Family J}
    (h : FamilyHom (sigmaFamily f B) A) : FamilyHom B (reindexFamily f A) :=
  fun i b => h (f i) ⟨i, b, rfl⟩

def reindexToSigma {I J : Type u} {f : I → J} {B : Family I} {A : Family J}
    (k : FamilyHom B (reindexFamily f A)) : FamilyHom (sigmaFamily f B) A :=
  fun _ x => transportFamily x.equation (k x.index x.value)

theorem sigma_reindex_left_inv {I J : Type u} {f : I → J} {B : Family I} {A : Family J}
    (h : FamilyHom (sigmaFamily f B) A) :
    reindexToSigma (sigmaToReindex h) = h := by
  funext j x
  rcases x with ⟨i, b, equality⟩
  cases equality
  rfl

theorem sigma_reindex_right_inv {I J : Type u} {f : I → J} {B : Family I} {A : Family J}
    (k : FamilyHom B (reindexFamily f A)) :
    sigmaToReindex (reindexToSigma k) = k := by
  funext i b
  simp [sigmaToReindex, reindexToSigma, transportFamily]

def sigmaReindexEquiv {I J : Type u} (f : I → J) (B : Family I) (A : Family J) :
    FamilyHom (sigmaFamily f B) A ≃ FamilyHom B (reindexFamily f A) where
  toFun := sigmaToReindex
  invFun := reindexToSigma
  left_inv := sigma_reindex_left_inv
  right_inv := sigma_reindex_right_inv

def piFamily {I J : Type u} (f : I → J) (B : Family I) : Family J :=
  fun j => ∀ i, f i = j → B i

def reindexToPi {I J : Type u} {f : I → J} {A : Family J} {B : Family I}
    (h : FamilyHom (reindexFamily f A) B) : FamilyHom A (piFamily f B) :=
  fun _ a i equality => h i (transportFamily (A := A) equality.symm a)

def piToReindex {I J : Type u} {f : I → J} {A : Family J} {B : Family I}
    (k : FamilyHom A (piFamily f B)) : FamilyHom (reindexFamily f A) B :=
  fun i a => k (f i) a i rfl

theorem pi_reindex_left_inv {I J : Type u} {f : I → J} {A : Family J} {B : Family I}
    (h : FamilyHom (reindexFamily f A) B) :
    piToReindex (reindexToPi h) = h := by
  funext i a
  simp [piToReindex, reindexToPi, transportFamily]

theorem pi_reindex_right_inv {I J : Type u} {f : I → J} {A : Family J} {B : Family I}
    (k : FamilyHom A (piFamily f B)) :
    reindexToPi (piToReindex k) = k := by
  funext j a i equality
  cases equality
  simp [piToReindex, reindexToPi, transportFamily]

def reindexPiEquiv {I J : Type u} (f : I → J) (A : Family J) (B : Family I) :
    FamilyHom (reindexFamily f A) B ≃ FamilyHom A (piFamily f B) where
  toFun := reindexToPi
  invFun := piToReindex
  left_inv := pi_reindex_left_inv
  right_inv := pi_reindex_right_inv

open _root_.CategoryTheory
open ChosenPullbacksAlong
open ExponentiableMorphism

universe uC vC

variable {C : Type uC} [Category.{vC} C]
variable {I J : C} (f : I ⟶ J)
variable [ChosenPullbacksAlong f] [ExponentiableMorphism f]

def dependentProductFunctor : Over I ⥤ Over J := pushforward f

example : Over.map f ⊣ pullback f := mapPullbackAdj f

example : pullback f ⊣ dependentProductFunctor f := pullbackPushforwardAdj f

variable {A : Over J} {X : Over I}

def dependentCurry (u : (pullback f).obj A ⟶ X) :
    A ⟶ (dependentProductFunctor f).obj X :=
  pushforwardCurry u

def dependentUncurry (v : A ⟶ (dependentProductFunctor f).obj X) :
    (pullback f).obj A ⟶ X :=
  pushforwardUncurry v

theorem dependent_uncurry_curry (u : (pullback f).obj A ⟶ X) :
    dependentUncurry f (dependentCurry f u) = u :=
  pushforward_uncurry_curry u

theorem dependent_curry_uncurry (v : A ⟶ (dependentProductFunctor f).obj X) :
    dependentCurry f (dependentUncurry f v) = v :=
  pushforward_curry_uncurry v