スケッチ #328

Relative covariety size obstruction ## Trigger [[rze8cb]] で absolute covariety classification を relative topos に「internalize すればよい」としたが、監査すると一般の elementary base \(\mathcal S\) では重要な size/cocompleteness obstruction がある。ここを切り分ける。 ## Correction absolute Grothendieck case の converse \[ \mathcal V\mapsto T_{\mathcal V}X:=\bigvee\{A\hookrightarrow X\mid A\in\mathcal V\} \] は、\(\operatorname{Sub}(X)\) の当該 external set-indexed join を使う。Grothendieck topos では small coproducts からこの join を作れる。 しかし bounded geometric morphism \(p:\mathcal E\to\mathcal S\) で \(\mathcal S\) が一般の elementary topos の場合、\(\mathcal E\) は arbitrary external small coproducts を持つとは限らない。relative Giraud theorem が保証するのは \(\mathcal S\)-internal / indexed cocompletenessであり、外部集合で添字づけた全 \(\mathcal V\)-subobject の join を自動的には作れない。 従って \[ \operatorname{Up}(\Xi_p)\cong \operatorname{Cov}_{\mathcal S}(\mathcal E) \] を「全ての closure-defined relative covarieties」について無条件に主張するのは現段階では正当化されていない。[[rze8cb]] の relative theorem はこの点を強めて修正すべき。 ## Theorem 1: definable/coreflective relative covarieties relative LSC \(\Xi_p\) が存在し、canonical maps \(\xi_X^p\) と order calculus が absolute case と同様に成立するとする。 upward subobject \(U\hookrightarrow\Xi_p\) に \[ \mathcal E_U:=\{X\mid \xi_X^p\text{ factors through }U\} \] を対応させると、これは subobjects, quotients, relative copowers \(p^*I\times-\) で閉じる。 逆に relative full subcategory \(\mathcal V\) が各 \(X\) に最大 \(\mathcal V\)-subobject \(T_{\mathcal V}X\hookrightarrow X\) を持ち、これが monos に沿って pullback-stable なら、absolute proof と同じ LSC universal property により \[ \gamma_{\mathcal V}:\Xi_p\to\Omega_{\mathcal E},\qquad U_{\mathcal V}=\gamma_{\mathcal V}^{-1}(\top) \] が得られ、quotient closure から \(U_{\mathcal V}\) は upward closed、かつ \[ \mathcal V=\mathcal E_{U_{\mathcal V}}. \] したがって upward subobjects は少なくとも **LSC-definable（equivalently, この maximal-subobject/coreflective 条件を満たす）relative covarieties** を完全に分類する。 ## Theorem 2: single-object relative generation is size-safe 対象 \(B\in\mathcal E\) に対し \[ \operatorname{Cov}_p(B):=\{X\mid \exists I\in\mathcal S,\ X\text{ is a subquotient of }p^*I\times B\} \] と置く。この class は subobjects, quotients, relative copowers で閉じ、外部 arbitrary coproduct を使わず定義できる。 relative LSC が base parameters を無視する標準性 \[ \xi^p_{p^*I\times B}=\xi_B^p\pi_B \] および absolute case と同じ local factorization criterion \[ \xi_X^p(x)\le\xi_Y^p(y)\iff\text{locally orbit quotient of }y\text{ factors through that of }x \] を満たすなら、 \[ \boxed{X\in\operatorname{Cov}_p(B)\iff \operatorname{im}(\xi_X^p)\subseteq\uparrow\!\operatorname{im}(\xi_B^p).} \] (⇒) subobject では state は不変、quotient では state は上昇し、\(p^*I\) は relative state を変えない。 (⇐) 各 local state of \(X\) がある state of \(B\) 以上なら、local factorization criterion により局所的に subobject of \(B\) から \(X\) への射でその section を覆える。witnesses は base \(\mathcal S\) 内の indexed familyとしてまとめられ、relative coproductから \(p^*I\times B\) の subobject \(S\) と epi \(S\twoheadrightarrow X\) を得る。 従って singly generated relative covariety に対応する subobject はサイズ問題なく \[ \boxed{U_B^p=\uparrow\!\operatorname{im}(\xi_B^p).} \] 特に \[ \boxed{B\text{ is a bound for }p\iff U_B^p=\Xi_p.} \] これは [[qdhgdp]] の genuine relative analogue であり、full classification の size 問題を必要としない。 ## Three-column safe dictionary | object property | relative LSC spectrum | full subcategory property | |---|---|---| | arbitrary \(B\) | \(U_B^p=\uparrow\operatorname{im}\xi_B^p\) | singly generated \(\operatorname{Cov}_p(B)\) | | \(B\) bound for \(p\) | \(U_B^p=\Xi_p\) | \(\operatorname{Cov}_p(B)=\mathcal E\) | | \(\xi_B^p\) epi | \(\operatorname{im}\xi_B^p=\Xi_p\) | in particular \(B\) is a bound | | \(B\in\mathcal E_U\) | \(U_B^p\subseteq U\) | \(\operatorname{Cov}_p(B)\subseteq\mathcal E_U\) | ## Open point 全 upward subobjects と「closure axiomsだけで定義した全 relative covarieties」の surjectivity を得るには、各 covariety が \(\mathcal S\)-smallly generated / maximal-subobjectを持つことを示す追加定理が必要。これは relative LSC existence [[nfrbb5]] とは別の size problem である。 ## Status absolute Grothendieck classification [[rze8cb]] は影響を受けない。relative partのみ修正。single-object / bound correspondence は明示した relative-LSC axiomsの下で proof-complete。