map'_inv_eq_inv_map' — Mathlib

English

A concluding form of the map inverse coherence for all levels, with nested isomorphisms.

Русский

Завершающая форма когерентности для обратного отображения map' на всех уровнях.

LaTeX

$$$\\forall {n m} (h: n+1 ≤ m) {f g} (app: f.obj' n ≅ g.obj' n) (app': f.obj' (n+1) ≅ g.obj' (n+1)) (w: f.map' n (n+1) ≫ app'.hom = app.hom ≫ g.map' n (n+1)) : (map' g n (n+1) ≫ app'.inv = app.inv ≫ map' f n (n+1))$$$

Lean4

theorem map'_inv_eq_inv_map' {n m : ℕ} (h : n + 1 ≤ m) {f g : ComposableArrows C m} (app : f.obj' n ≅ g.obj' n)
    (app' : f.obj' (n + 1) ≅ g.obj' (n + 1)) (w : f.map' n (n + 1) ≫ app'.hom = app.hom ≫ g.map' n (n + 1)) :
    map' g n (n + 1) ≫ app'.inv = app.inv ≫ map' f n (n + 1) := by
  rw [← cancel_epi app.hom, ← reassoc_of% w, app'.hom_inv_id, comp_id, app.hom_inv_id_assoc]

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