congr_map — Mathlib

English

Construction mapObj yields a canonical morphism between iterated objects.

Русский

Построение mapObj даёт канонический морфизм между объектами итерации.

LaTeX

$$$ \\mathrm{mapObj} \\; iter_1 \\; iter_2 \\; h_{12} \\; h_1 \\; h_2 \\; hj $$$

Lean4

theorem congr_map {j₁ j₂ : J} (iter₁ : Φ.Iteration j₁) (iter₂ : Φ.Iteration j₂) {k₁ k₂ : J} (h : k₁ ≤ k₂) (h₁ : k₂ ≤ j₁)
    (h₂ : k₂ ≤ j₂) :
    iter₁.F.map (homOfLE h : ⟨k₁, h.trans h₁⟩ ⟶ ⟨k₂, h₁⟩) =
      eqToHom (congr_obj iter₁ iter₂ k₁ (h.trans h₁) (h.trans h₂)) ≫
        iter₂.F.map (homOfLE h) ≫ eqToHom (congr_obj iter₁ iter₂ k₂ h₁ h₂).symm :=
  by
  have := (Arrow.mk_eq_mk_iff _ _).1 (congr_arrowMap iter₁ iter₂ h h₁ h₂)
  tauto

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