Theorems · Definition · algebraic topology

SSet.Edge.CompStruct.ofEq

{X : SSet} →
  {x₀ x₁ x₂ y₀ y₁ y₂ : X.obj (Opposite.op { len := 0 })} →
    {e₀₁ : SSet.Edge x₀ x₁} →
      {f₀₁ : SSet.Edge y₀ y₁} →
        {e₁₂ : SSet.Edge x₁ x₂} →
          {f₁₂ : SSet.Edge y₁ y₂} →
            {e₀₂ : SSet.Edge x₀ x₂} →
              {f₀₂ : SSet.Edge y₀ y₂} →
                e₀₁.CompStruct e₁₂ e₀₂ →
                  e₀₁.edge = f₀₁.edge → e₁₂.edge = f₁₂.edge → e₀₂.edge = f₀₂.edge → f₀₁.CompStruct f₁₂ f₀₂

Transports a CompStruct between edges e₀₁, e₁₂ and e₀₂ to a CompStruct between edges f₀₁, f₁₂ and f₀₂ along equalities of 1-simplices eᵢⱼ.edge = fᵢⱼ.edge.

Defined in

Mathlib.AlgebraicTopology.SimplicialSet.CompStruct

Cited by

5 results in Mathlib

Foundations

Depth 41 from the axioms · uses propext, Classical.choice, Quot.sound