unop — Mathlib

English

There is a natural correspondence that turns a binary cof an in the opposite category into a binary fan in the original category by taking opposites of the legs.

Русский

Существует естественное соответствие между бинарным кофаном в противоположной категории и бинарным фаном в исходной, получаемое взятием противоположностей ножек.

LaTeX

$$$$\\text{unop}(c) = \\text{BinaryFan}(X,Y) \\quad\\text{with}\\quad \\mathrm{fst} = c.inl^{\\mathrm{op}}, \\ \\mathrm{snd} = c.inr^{\\mathrm{op}}.$$$$

Lean4

/-- A binary cofan in the opposite category gives a binary fan. -/
protected abbrev unop (c : BinaryCofan (op X) (op Y)) : BinaryFan X Y :=
  .mk c.inl.unop c.inr.unop

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