triangle_inv

Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.CatCospanTransform.triangle_inv

English

Inverse whiskering on the left yields a natural isomorphism with whiskerLeft of the inverse morphism.

Русский

Обратное взвешивание слева даёт естественный изоморфизм с whiskerLeft от обратного морфизма.

LaTeX

$$$inv(ψ \\;◁\\; θ) = ψ \\;◁\\; inv(θ)$$$

Lean4

@[reassoc]
theorem triangle_inv : (α_ ψ (.id _ _) φ).inv ≫ (ρ_ ψ).hom ▷ φ = ψ ◁ (λ_ φ).hom := by cat_disch

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

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

Разделы

Аффилиация

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