proj_comp_transitionMap — Mathlib

English

Let S be a LightProfinite. For every n, the projection S.proj(n+1) followed by the diagram’s transition map to n equals the projection S.proj n; i.e., the family of projections is compatible with the bonding maps.

Русский

Пусть S — светопротрофное пространство. Для каждого n проекция S.proj(n+1), затем переходная карта диаграммы к n, даёт S.proj n; то есть семейство проекций совместимо с переходами.

LaTeX

$$$S\operatorname{proj}(n+1) \;\; \xrightarrow{\;S.diagram.map(\langle homOfLE(\mathrm{Nat}.le_succ _) )\rangle} \; S\operatorname{proj}(n) = S\operatorname{proj}(n)$$$

Lean4

theorem proj_comp_transitionMap (n : ℕ) : S.proj (n + 1) ≫ S.diagram.map ⟨homOfLE (Nat.le_succ _)⟩ = S.proj n :=
  S.asLimitCone.w (homOfLE (Nat.le_succ n)).op

Похожие утверждения