📐 Proposition XXIV.2.7（始収束 $f^-\sigma$ に対する $[\theta,f^-\sigma]$ の $f_*$ による引き戻し表示）
- 📐 Proposition XXIV.2.7（始収束 $f^-\sigma$ に対する $[\theta,f^-\sigma]$ の $f_*$ による引き戻し表示） #Card
- $cards/topology/prop-xxiv-2-5-dual-convergence-pullback-surjective の始収束版（lower adjoint 経由）はどう書けるか。
Proposition XXIV.2.7: 任意の $\theta,\sigma$ と $f:\vert\theta\vert\to\vert\sigma\vert$ に対し $$[\theta, f^-\sigma] = (f_*)^-[\theta,\sigma].$$
証明: cards/topology/prop-xxiv-2-6-lower-adjoint-continuity を $f\in C(f^-\sigma,\sigma)$ に適用して $[\theta,f^-\sigma]\geq(f_)^-[\theta,\sigma]$。逆向きは $g\in\lim_{(f_)^-[\theta,\sigma]}G$、すなわち $f_(g)\in\lim_{[\theta,\sigma]}f_[G]$ から、$\langle g(w),f\rangle\in\lim_\sigma f[\langle W,G\rangle]$（$w\in\lim_\theta W$ のとき）が $\langle w,g\rangle\in\lim_{f^-\sigma}\langle W,G\rangle$ と同値であることを使い、$g\in\lim_{[\theta,f^-\sigma]}G$ を結論。
cards/topology/prop-xxiv-2-5-dual-convergence-pullback-surjective（終収束・upper adjoint 版）と対をなす、始収束・lower adjoint 版。この2つの公式が cards/topology/lemma-xxiv-2-8-reflector-coreflector-density-criterion の証明（(XXIV.2.3) の導出）で組み合わせて使われる。