op_σ — Mathlib

English

The degeneracy-like maps σ on X.op correspond to applying σ on X and transporting back through the canonical identification.

Русский

Операции σ на X.op соответствуют применению σ к X и обратной транспортировке через каноническое соответствие.

LaTeX

$$$X.op.\\sigma_i x = opObjEquiv.symm( X.\\sigma_i (opObjEquiv x) )$$$

Lean4

@[simp]
theorem op_σ (X : SSet.{u}) {n : ℕ} (i : Fin (n + 1)) (x : X _⦋n⦌) :
    X.op.σ i x = opObjEquiv.symm (X.σ i.rev (opObjEquiv x)) := by simp [SimplicialObject.σ, op_map]

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