Lee 與 van Oosten 閱讀筆記，Proposition 1.2

為什麼要在意 local operator？因為一個 topos $\mathcal{E}$ 的子拓樸（subtopos）跟 $\mathcal{E}$ 上的 local operator 一一對應：子拓樸就是對有限極限封閉、且包含函子有保持有限極限左伴隨的全子範疇，而這樣的資料剛好被 $\Omega$ 上的某類自映射編碼。所以「構造並區分 local operator」等於「構造並區分子拓樸」。

舞台上的角色： $\Omega$ 是子物件分類子， $\text{Mon}$ 是 $\Omega \to \Omega$ 的單調自映射， $\text{Loc}$ 則是 local operator。論文指出 $\text{Mon}$ 與 $\text{Loc}$ 都是 internal locale，因為 Proposition 1.2 這個 Topos Theory 的一個 folklore 結果：包含映射 $\text{Loc} \hookrightarrow \text{Mon}$ 有一個左伴隨 $L$ 保持有限 meet

首先看用到的四個定義

Definition Mon（單調自映射） [ag-V2O7]

{-# OPTIONS --safe --without-K #-}
open import MLTT.Spartan
open import UF.FunExt
open import UF.PropTrunc
open import UF.Subsingletons
open import UF.SubtypeClassifier
open import UF.Size
open import UF.Logic

module ag-V2O7
  (pt : propositional-truncations-exist)
  (fe : Fun-Ext)
  (pe : propext 𝓤)
  (ρ  : propositional-resizing (𝓤 ⁺) 𝓤)
  where

open Conjunction
open Universal   fe
open Implication fe

Monotone map 是 Ω 的自映射 f : Ω → Ω，滿足 p ⇒ q 蘊涵 f p ⇒ f q

is-monotone : (Ω 𝓤 → Ω 𝓤) → Ω (𝓤 ⁺)
is-monotone f = Ɐ p ꞉ Ω 𝓤 , Ɐ q ꞉ Ω 𝓤 , (p ⇒ q) ⇒ (f p ⇒ f q)

Mon 代表所有 monotone maps 的 type

Mon : 𝓤 ⁺ ̇
Mon = Σ f ꞉ (Ω 𝓤 → Ω 𝓤) , is-monotone f holds

我們定義一個輔助函數讓之後的證明可讀一點

monotone-function : Mon → (Ω 𝓤 → Ω 𝓤)
monotone-function m = pr₁ m

Definition Local operator [ag-5W9X]

{-# OPTIONS --safe --without-K #-}
open import MLTT.Spartan
open import UF.FunExt
open import UF.PropTrunc
open import UF.Subsingletons
open import UF.SubtypeClassifier
open import UF.Size
open import UF.Logic

module ag-5W9X
  (pt : propositional-truncations-exist)
  (fe : Fun-Ext)
  (pe : propext 𝓤)
  (ρ  : propositional-resizing (𝓤 ⁺) 𝓤)
  where

open Conjunction
open Universal   fe
open Implication fe

open import ag-V2O7 pt fe pe ρ

Local operator 是一個 Ω 自映射 j : Ω → Ω，滿足

單調（mono）
保持 ⊤（unit）
冪等（idem）

三個條件定義在 record 中

record is-local-operator (j : Ω 𝓤 → Ω 𝓤) : 𝓤 ⁺ ̇ where
  field
    mono : is-monotone j holds
    unit : (⊤ {𝓤} ⇒ j ⊤) holds
    idem : (p : Ω 𝓤) → (j (j p) ⇒ j p) holds

Definition $\Omega^\Omega$ 的逐點序 ≼ [ag-UAEO]

{-# OPTIONS --safe --without-K #-}
open import MLTT.Spartan
open import UF.FunExt
open import UF.PropTrunc
open import UF.Subsingletons
open import UF.SubtypeClassifier
open import UF.Size
open import UF.Logic

module ag-UAEO
  (pt : propositional-truncations-exist)
  (fe : Fun-Ext)
  (pe : propext 𝓤)
  (ρ  : propositional-resizing (𝓤 ⁺) 𝓤)
  where

open Conjunction
open Universal   fe
open Implication fe

$\Omega^\Omega$ 的元素之間我們可以用 pointwise 的方式定義一個順序 f ≼ g：對每個 p，f p ⇒ g p

_≼_ : (Ω 𝓤 → Ω 𝓤) → (Ω 𝓤 → Ω 𝓤) → Ω (𝓤 ⁺)
f ≼ g = Ɐ p ꞉ Ω 𝓤 , f p ⇒ g p

後面談 L 是左伴隨時就是用這個順序。

Definition Left adjoint $L$ [ag-GY8B]

{-# OPTIONS --safe --without-K #-}
open import MLTT.Spartan
open import UF.FunExt
open import UF.PropTrunc
open import UF.Subsingletons
open import UF.SubtypeClassifier
open import UF.Size
open import UF.Logic

module ag-GY8B
  (pt : propositional-truncations-exist)
  (fe : Fun-Ext)
  (pe : propext 𝓤)
  (ρ  : propositional-resizing (𝓤 ⁺) 𝓤)
  where

open Conjunction
open Universal   fe
open Implication fe

Proposition 1.2 的左伴隨 L 定義為 L(f)(p) = ∀q. (((p → q) ∧ (f q → q)) → q)

但因為類型論的關係，它落在 Ω (𝓤 ⁺) 上（L⁺）

L⁺ : (Ω 𝓤 → Ω 𝓤) → Ω 𝓤 → Ω (𝓤 ⁺)
L⁺ f p = Ɐ q ꞉ Ω 𝓤 , ((p ⇒ q) ∧ (f q ⇒ q)) ⇒ q

論文裡 Ω 是 impredicative，全稱量化後仍落在 Ω；所以要靠 propositional resizing 把它放回去 Ω 𝓤 得到 L

L : (Ω 𝓤 → Ω 𝓤) → Ω 𝓤 → Ω 𝓤
L f p = resize         ρ (L⁺ f p holds) (holds-is-prop (L⁺ f p))
      , resize-is-prop ρ (L⁺ f p holds) (holds-is-prop (L⁺ f p))

ηL、εL 是在兩種 size 之間搬動證明的轉換器。讀法上，(L⁺ f p) holds 展開後就是

(q : Ω 𝓤) → (p ⇒ q) holds × (f q ⇒ q) holds → q holds

後面所有證明都先用 εL 把 L f p 拆成上面的 universal property、再用 ηL 把證明包回去。

ηL : (f : Ω 𝓤 → Ω 𝓤) (p : Ω 𝓤) → (L⁺ f p) holds → (L f p) holds
ηL f p = to-resize ρ (L⁺ f p holds) (holds-is-prop (L⁺ f p))

εL : (f : Ω 𝓤 → Ω 𝓤) (p : Ω 𝓤) → (L f p) holds → (L⁺ f p) holds
εL f p = from-resize ρ (L⁺ f p holds) (holds-is-prop (L⁺ f p))

有了這些定義，可以開始證明 Proposition 1.2。第一步：L 把每個 Mon 成員都變成 Loc 的成員。

Theorem $L(f)$ 是一個 local operator [ag-95LU]

Proposition 1.2 的核心：只要 $f$ 是 monotone，套上 $L$ 之後就變成一個 local operator。換句話說 $L$ 把 $\text{Mon}$ 成員升級成 $\text{Loc}$ 成員

Proof [local-0]

{-# OPTIONS --safe --without-K #-}
open import MLTT.Spartan
open import UF.FunExt
open import UF.PropTrunc
open import UF.Subsingletons
open import UF.SubtypeClassifier
open import UF.Size
open import UF.Logic

module ag-95LU
  (pt : propositional-truncations-exist)
  (fe : Fun-Ext)
  (pe : propext 𝓤)
  (ρ  : propositional-resizing (𝓤 ⁺) 𝓤)
  where

open Conjunction
open Universal   fe
open Implication fe

open import ag-V2O7 pt fe pe ρ
open import ag-5W9X pt fe pe ρ
open import ag-GY8B pt fe pe ρ
open is-local-operator

L-is-local-operator : (m : Mon) → is-local-operator (L (monotone-function m))

每個欄位對應 local operator 的一個條件，每個都需要「εL 拆開 → 操作 → ηL 包裝」

(i) 單調：給定 p ⇒ q，把目標裡的 q ⇒ r 沿著 p ⇒ q 前接成 p ⇒ r，再餵回 L f p

L-is-local-operator (f , fm) .mono p q p⇒q lfp = ηL f q goal
  where
  goal : (L⁺ f q) holds
  goal r (q⇒r , fr⇒r) = εL f p lfp r (p⇒r , fr⇒r)
    where
    p⇒r : (p ⇒ r) holds
    p⇒r p = q⇒r (p⇒q p)

(ii) ⊤ ⇒ L f ⊤：此時 q 直接由 ⊤ ⇒ q 得到

L-is-local-operator (f , fm) .unit _ = ηL f ⊤ goal
  where
  goal : (L⁺ f ⊤) holds
  goal q (⊤⇒q , fq⇒q) = ⊤⇒q ⊤-holds

(iii) 冪等 L f (L f p) ⇒ L f p：在外層代入 q := L f p。關鍵的小引理 f (L f p) ⇒ L f p 正好用到 f 的單調性

L-is-local-operator (f , f-is-monotone) .idem p ll =
  εL f (L f p) ll (L f p) (id-L , f∘L⇒Lf)
  where
  id-L : (L f p ⇒ L f p) holds
  id-L x = x

  f∘L⇒Lf : (f (L f p) ⇒ L f p) holds
  f∘L⇒Lf f[L[f[p]]] = ηL f p I
    where
    I : (L⁺ f p) holds
    I q (p⇒q , fq⇒q) = fq⇒q f[q]
      where
      -- 把 (p ⇒ q), (f q ⇒ q) 餵給 L f p
      Lfp⇒q : (L f p ⇒ q) holds
      Lfp⇒q L[f[p]] = εL f p L[f[p]] q (p⇒q , fq⇒q)

      -- f 單調表示 L f p ⇒ q 可以變成 f (L f p) ⇒ f q
      f[q] : f q holds
      f[q] = f-is-monotone (L f p) q Lfp⇒q f[L[f[p]]]

第二步是伴隨。需要一個關於任意 local operator 的小引理：

Lemma Local operator 是 inflationary [ag-GK6B]

任何 local operator $j$ 都是 inflationary 的，也就是 $p \Rightarrow j\ p$

Proof [local-0]

{-# OPTIONS --safe --without-K #-}
open import MLTT.Spartan
open import UF.FunExt
open import UF.PropTrunc
open import UF.Subsingletons
open import UF.SubtypeClassifier
open import UF.Size
open import UF.Logic

module ag-GK6B
  (pt : propositional-truncations-exist)
  (fe : Fun-Ext)
  (pe : propext 𝓤)
  (ρ  : propositional-resizing (𝓤 ⁺) 𝓤)
  where

open Conjunction
open Universal   fe
open Implication fe

open import ag-5W9X pt fe pe ρ
open is-local-operator

證明方式：若 p 成立則 p ＝ ⊤（用到 propext），再由 unit 得到 j ⊤。

LO-infl : {j : Ω 𝓤 → Ω 𝓤} → is-local-operator j → (p : Ω 𝓤) → (p ⇒ j p) holds
LO-infl {j} j-is-local-op p p-holds = transport (λ - → j - holds) ⊤＝p j⊤
  where
  -- p 成立，故 p ＝ ⊤
  ⊤＝p : ⊤ ＝ p
  ⊤＝p = (holds-gives-equal-⊤ pe fe p p-holds) ⁻¹

  -- 由 unit
  j⊤ : j ⊤ holds
  j⊤ = unit j-is-local-op ⋆

Proposition $L \dashv \text{Loc} \hookrightarrow \text{Mon}$ [ag-XCL4]

$L$ 是包含映射 $\text{Loc} \hookrightarrow \text{Mon}$ 的左伴隨

Proof [local-0]

{-# OPTIONS --safe --without-K #-}
open import MLTT.Spartan
open import UF.FunExt
open import UF.PropTrunc
open import UF.Subsingletons
open import UF.SubtypeClassifier
open import UF.Size
open import UF.Logic

module ag-XCL4
  (pt : propositional-truncations-exist)
  (fe : Fun-Ext)
  (pe : propext 𝓤)
  (ρ  : propositional-resizing (𝓤 ⁺) 𝓤)
  where

open Conjunction
open Universal   fe
open Implication fe

open import ag-V2O7 pt fe pe ρ
open import ag-5W9X pt fe pe ρ
open import ag-UAEO pt fe pe ρ
open import ag-GY8B pt fe pe ρ
open import ag-GK6B pt fe pe ρ
open is-local-operator

(→) 對任意 local operator j，若 f ≼ j 則 L f ≼ j，在 L f p 裡代入 q := j p

L-adjunction-→ :
  (m : Mon) {j : Ω 𝓤 → Ω 𝓤} → is-local-operator j
  → (monotone-function m ≼ j) holds → (L (monotone-function m) ≼ j) holds
L-adjunction-→ (f , _) {j} j-is-local-op f≼j p L[f][p] = εL f p L[f][p] (j p) (p⇒jp , fjp⇒jp)
  where
  p⇒jp : (p ⇒ j p) holds
  p⇒jp = LO-infl j-is-local-op p

  fjp⇒jp : (f (j p) ⇒ j p) holds
  fjp⇒jp x = idem j-is-local-op p (f≼j (j p) x)

(←)：伴隨的單位是 f ≼ L f，要用到 f 的單調性。

f≼Lf : ((f , f-is-monotone) : Mon) → (f ≼ L f) holds
f≼Lf (f , f-is-monotone) p f[p] = ηL f p I
  where
  I : (L⁺ f p) holds
  I q (p⇒q , fq⇒q) = fq⇒q f[q]
    where
    f[q] : f q holds
    f[q] = f-is-monotone p q p⇒q f[p]

L-adjunction-← : (m : Mon) {j : Ω 𝓤 → Ω 𝓤} → is-local-operator j
              → (L (monotone-function m) ≼ j) holds → (monotone-function m ≼ j) holds
L-adjunction-← m {j} j-is-local-op Lf≼j p fp = Lf≼j p (f≼Lf m p fp)

第三步：除了是左伴隨， $L$ 還保持有限 meet。

Proposition $L$ 保持有限 meet [ag-V7YV]

Proposition 1.2 的另一半： $L$ 保持有限 meet。有限 meet 等於頂元素 $\top$ 加上二元 meet $\land$

Proof [local-0]

{-# OPTIONS --safe --without-K #-}
open import MLTT.Spartan
open import UF.FunExt
open import UF.PropTrunc
open import UF.Subsingletons
open import UF.SubtypeClassifier
open import UF.Size
open import UF.Logic

module ag-V7YV
  (pt : propositional-truncations-exist)
  (fe : Fun-Ext)
  (pe : propext 𝓤)
  (ρ  : propositional-resizing (𝓤 ⁺) 𝓤)
  where

open Conjunction
open Universal   fe
open Implication fe

open import ag-UAEO pt fe pe ρ
open import ag-GY8B pt fe pe ρ

(⇐) 方向：由 L f p 與 L g p 可以得出 L (f ∧ g) p。

L-preserves-∧-⇐ : (f g : Ω 𝓤 → Ω 𝓤) (p : Ω 𝓤)
               → (L f p holds × L g p holds)
               → L (λ x → f x ∧ g x) p holds
L-preserves-∧-⇐ f g p (Lfp , Lgp) = ηL (λ x → f x ∧ g x) p I
  where
  Lf = εL f p Lfp
  Lg = εL g p Lgp

  I : (L⁺ (λ x → f x ∧ g x) p) holds
  I s (p⇒s , fs∧gs⇒s) = Lf s (p⇒s , fs⇒s)
    where
    fs⇒s : f s holds → s holds
    fs⇒s fs = Lg s (p⇒s , gs⇒s)
      where
      gs⇒s : g s holds → s holds
      gs⇒s gs = fs∧gs⇒s (fs , gs)

(⇒) 方向由 L-operator-mono（一個輔助證明：f ≼ g 蘊涵 L f ≼ L g）配上 f ∧ g ≼ f、f ∧ g ≼ g 得到。

L-operator-mono : (f g : Ω 𝓤 → Ω 𝓤)
                → (f ≼ g) holds
                → (L f ≼ L g) holds
L-operator-mono f g f≼g p lfp = ηL g p I
  where
  I : (L⁺ g p) holds
  I q (p⇒q , gq⇒q) = εL f p lfp q (p⇒q , fq⇒q)
    where
    fq⇒q : (f q ⇒ q) holds
    fq⇒q x = gq⇒q (f≼g q x)

L-preserves-∧-⇒ : (f g : Ω 𝓤 → Ω 𝓤) (p : Ω 𝓤)
               → L (λ x → f x ∧ g x) p holds
               → (L f p holds × L g p holds)
L-preserves-∧-⇒ f g p lfgp = to-f , to-g
  where
  to-f : L f p holds
  to-f = L-operator-mono (λ x → f x ∧ g x) f (λ q → pr₁) p lfgp

  to-g : L g p holds
  to-g = L-operator-mono (λ x → f x ∧ g x) g (λ q → pr₂) p lfgp

兩個方向合併就得到逐點的等式 L (f ∧ g) p ＝ L f p ∧ L g p

L-preserves-∧ : (f g : Ω 𝓤 → Ω 𝓤) (p : Ω 𝓤)
             → L (λ x → f x ∧ g x) p ＝ L f p ∧ L g p
L-preserves-∧ f g p = Ω-extensionality pe fe (L-preserves-∧-⇒ f g p)
                                             (L-preserves-∧-⇐ f g p)

Basic Subtoposes of the Effective Topos：Proposition 1.2 [ECDG]

Definition Mon（單調自映射） [ag-V2O7]

Definition Local operator [ag-5W9X]

Definition ΩΩ\Omega^\OmegaΩΩ 的逐點序 ≼ [ag-UAEO]

Definition Left adjoint LLL [ag-GY8B]

Theorem L(f)L(f)L(f) 是一個 local operator [ag-95LU]

Proof [local-0]

Lemma Local operator 是 inflationary [ag-GK6B]

Proof [local-0]

Proposition L⊣Loc↪MonL \dashv \text{Loc} \hookrightarrow \text{Mon}L⊣Loc↪Mon [ag-XCL4]

Proof [local-0]

Proposition LLL 保持有限 meet [ag-V7YV]

Proof [local-0]

Definition $\Omega^\Omega$ 的逐點序 ≼ [ag-UAEO]

Definition Left adjoint $L$ [ag-GY8B]

Theorem $L(f)$ 是一個 local operator [ag-95LU]

Proposition $L \dashv \text{Loc} \hookrightarrow \text{Mon}$ [ag-XCL4]

Proposition $L$ 保持有限 meet [ag-V7YV]