transitionMapLE — Mathlib

English

For a LightProfinite S and natural numbers n, m with n ≤ m, there is a canonical morphism from S.component m to S.component n, obtained from the diagram by applying the map corresponding to homOfLE(h).

Русский

Для S и целых чисел n, m с n ≤ m существует канонический морфизм из S.component m в S.component n, полученный из диаграммы путём применения отображения, соответствующего hom Of LE(h).

LaTeX

$$$S_m \to S_n, \quad \text{when } n \le m, \text{ given by } S.diagram.map(\langle homOfLE(h) \rangle)$$$

Lean4

/-- The transition map from `S_m` to `S_n` in `S.diagram`, when `m ≤ n`. -/
abbrev transitionMapLE {n m : ℕ} (h : n ≤ m) : S.component m ⟶ S.component n :=
  S.diagram.map ⟨homOfLE h⟩

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