mapObj — Mathlib

English

The maps between iterates are equal after applying homOfLE and conjugation by isomorphisms.

Русский

Отображения между итерациями равны после применения homOfLE и сопряжения изоморфизмами.

LaTeX

$$$ \\mathrm{congr\\_map} \\; iter_1 \\; iter_2 \\; h \\; h_1 \\; h_2 $$$

Lean4

/-- Given `iter₁ : Φ.Iteration j₁` and `iter₂ : Φ.Iteration j₂`, with `j₁ ≤ j₂`,
if `k₁ ≤ k₂` are elements such that `k₁ ≤ j₁` and `k₂ ≤ k₂`, then this
is the canonical map `iter₁.F.obj ⟨k₁, h₁⟩ ⟶ iter₂.F.obj ⟨k₂, h₂⟩`. -/
def mapObj {j₁ j₂ : J} (iter₁ : Φ.Iteration j₁) (iter₂ : Φ.Iteration j₂) {k₁ k₂ : J} (h₁₂ : k₁ ≤ k₂) (h₁ : k₁ ≤ j₁)
    (h₂ : k₂ ≤ j₂) (hj : j₁ ≤ j₂) : iter₁.F.obj ⟨k₁, h₁⟩ ⟶ iter₂.F.obj ⟨k₂, h₂⟩ :=
  eqToHom (congr_obj iter₁ iter₂ k₁ h₁ (h₁.trans hj)) ≫ iter₂.F.map (homOfLE h₁₂)

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