comp_inv

Mathlib.CategoryTheory.Monoidal.Cartesian.Grp_

URI: https://scilib.ai/kg/mathlib#GrpObj.comp_inv

English

For f,g:H→G, the division operation distributes over composition with a monoid morphism: f/g ≫ h = (f≫h)/(g≫h).

Русский

Операция деления распределяется над композициями: f/g ≫ h = (f≫h)/(g≫h).

LaTeX

$$$(f/g) \;\circ h = (f\circ h) /(g\circ h)$$$

Lean4

@[reassoc]
theorem comp_inv (f : X ⟶ Y) (g : Y ⟶ G) : f ≫ g⁻¹ = (f ≫ g)⁻¹ :=
  ((yonedaGrp.obj ⟨G⟩).map f.op).hom.map_inv g

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru