Documentation

Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Op

The opposite of a pairing #

Let A be a subcomplex of a simplicial set X. If P is a pairing of A, we construct a pairing P.op for the subcomplex A.op of X.op.

source
@[implicit_reducible]
def SSet.Subcomplex.Pairing.op {X : SSet} {A : X.Subcomplex} (P : A.Pairing) :
A.op.Pairing

If P is a pairing for a subcomplex A of a simplicial set X, this is the corresponding pairing of A.op.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem SSet.Subcomplex.Pairing.op_II {X : SSet} {A : X.Subcomplex} (P : A.Pairing) :
    P.op.II = ⇑N.opEquiv ⁻¹' P.II
    source
    @[simp]
    theorem SSet.Subcomplex.Pairing.op_I {X : SSet} {A : X.Subcomplex} (P : A.Pairing) :
    P.op.I = ⇑N.opEquiv ⁻¹' P.I
    source
    @[simp]
    theorem SSet.Subcomplex.Pairing.op_p {X : SSet} {A : X.Subcomplex} (P : A.Pairing) (x : ↑P.II) :
    P.op.p ⟨N.opEquiv.symm ↑x, ⋯⟩ = ⟨N.opEquiv.symm ↑(P.p x), ⋯⟩
    source
    theorem SSet.Subcomplex.Pairing.op_ancestralRel_iff {X : SSet} {A : X.Subcomplex} (P : A.Pairing) (x y : ↑P.II) :
    P.op.AncestralRel ⟨N.opEquiv.symm ↑x, ⋯⟩ ⟨N.opEquiv.symm ↑y, ⋯⟩ ↔ P.AncestralRel x y
    source
    instance SSet.Subcomplex.Pairing.instIsProperOp {X : SSet} {A : X.Subcomplex} (P : A.Pairing) [P.IsProper] :
    P.op.IsProper
    source
    instance SSet.Subcomplex.Pairing.instIsRegularOp {X : SSet} {A : X.Subcomplex} (P : A.Pairing) [P.IsRegular] :
    P.op.IsRegular