congr — Mathlib

English

A compatibility relation for a family of morphisms indexed by ι under a equality between indices.

Русский

Совместное соотношение семейства морфизмов, индексируемого по ι, при равенстве индексов.

LaTeX

$$$\\alpha_i = \\mathrm{eqToHom}(\\mathrm{congrArg} F\\, h) \\,\\circ \\, \\alpha_j \\,\\circ \\, \\mathrm{eqToHom}(\\mathrm{congrArg} G\\, h^{\\mathrm{symm}})$$$

Lean4

theorem congr {F G : C ⥤ D} (α : F ⟶ G) {X Y : C} (h : X = Y) :
    α.app X = F.map (eqToHom h) ≫ α.app Y ≫ G.map (eqToHom h.symm) :=
  by
  rw [α.naturality_assoc]
  simp [eqToHom_map]

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