edgeTransform — Mathlib

English

edgeTransform collects all edge morphisms into a natural transformation between the two projections composed with the left and right inclusions.

Русский

edgeTransform собирает все реберные морфизмы в натуральное преобразование между двумя проекциями, композициями с левым и правым включениями.

LaTeX

$$edgeTransform : Prod.fst C D ⋙ inclLeft C D ⟶ Prod.snd C D ⋙ inclRight C D$$

Lean4

/-- The "canonical" natural transformation from `(Prod.fst C D) ⋙ inclLeft C D` to
`(Prod.snd C D) ⋙ inclRight C D`. This is bundling together all the edge morphisms
into the data of a natural transformation. -/
@[simps!]
def edgeTransform : Prod.fst C D ⋙ inclLeft C D ⟶ Prod.snd C D ⋙ inclRight C D where app := fun (c, d) ↦ edge c d

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