English
Let α_i be a family of arrows F i ⟶ G i in a category, indexed by i ∈ I. If i = j via h, then α_i equals the conjugation of α_j by the isomorphisms F h and G h.symm, i.e., α_i = eqToHom (congrArg F h) ≫ α_j ≫ eqToHom (congrArg G h.symm).
Русский
Пусть α_i — семейство стрелок F_i ⟶ G_i, индексируемых i ∈ I. Если i = j через h, тогда α_i равно сопряжению α_j с помощью изоморфизмов F_h и G_h.symm, то есть α_i = eqToHom (congrArg F h) ≫ α_j ≫ eqToHom (congrArg G h.symm).
LaTeX
$$$\\alpha_i = \\mathrm{eqToHom}(\\mathrm{congrArg} F h) \\; \\circ \\; \\alpha_j \\; \\circ \\; \\mathrm{eqToHom}(\\mathrm{congrArg} G h^{\\mathrm{symm}}).$$$
Lean4
theorem dcongr_arg {ι : Type*} {F G : ι → C} (α : ∀ i, F i ⟶ G i) {i j : ι} (h : i = j) :
α i = eqToHom (congr_arg F h) ≫ α j ≫ eqToHom (congr_arg G h.symm) :=
by
subst h
simp
