Mathlib Map

Theorems · Definition · algebraic topology

SSet.Subcomplex.Pairing.RankFunction.sigmaHorn

{X : SSet} →
  {A : X.Subcomplex} →
    {P : A.Pairing} → {ι : Type v} → [inst : LinearOrder ι] → P.RankFunction ι → [P.IsProper] → ι → SSet

Given a rank function for a proper pairing of a subcomplex of a simplicial set, this is the coproduct of the horns corresponding to all cells of rank j.

Defined in
Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
Cited by
18 results in Mathlib
Foundations
Depth 95 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
LinearOrderSSet.Subcomplex.Pairing.IsProper
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

SSet.Subcomplex.Pairing.RankFunction.m · cited by 12RankFunction.mSSet.Subcomplex.Pairing.RankFunction.Cell.ιSigmaHorn · cited by 10Cell.ιSigmaHornSSet.Subcomplex.Pairing.RankFunction.t · cited by 9RankFunction.tSSet.Subcomplex.Pairing.RankFunction.mapN · cited by 4RankFunction.mapNSSet.Subcomplex.Pairing.RankFunction.Cell.type₁ · cited by 4Cell.type₁SSet.Subcomplex.Pairing.RankFunction.Cell.type₂ · cited by 4Cell.type₂SSet.Subcomplex.Pairing.RankFunction.w · cited by 3RankFunction.wSSet.Subcomplex.Pairing.RankFunction.Cell.ι_m · cited by 3Cell.ι_mSSet.Subcomplex.Pairing.RankFunction.Cell.ι_t · cited by 2Cell.ι_tSSet.Subcomplex.Pairing.RankFunction.Cell.ι_t_app · cited by 2Cell.ι_t_appSSet.Subcomplex.Pairing.RankFunction.Cell.ι_m_assoc · cited by 1Cell.ι_m_assocSSet.Subcomplex.Pairing.RankFunction.Cell.ι_t_app_apply · cited by 1Cell.ι_t_app_applySSet.Subcomplex.Pairing.RankFunction.Cell.ι_t_assoc · cited by 1Cell.ι_t_assocSSet.Subcomplex.Pairing.RankFunction.isPullback · cited by 1RankFunction.isPullbackSSet.Subcomplex.Pairing.RankFunction.w_assoc · cited by 0RankFunction.w_assocLinearOrder · cited by 8572LinearOrderSSet · cited by 1283SSetSSet.Subcomplex · cited by 461SSet.SubcomplexSSet.Subcomplex.toSSet · cited by 315Subcomplex.toSSetCategoryTheory.Limits.sigmaObj · cited by 302Limits.sigmaObjSSet.Subcomplex.Pairing · cited by 117Subcomplex.PairingSSet.Subcomplex.Pairing.RankFunction · cited by 68Pairing.RankFunctionSSet.Subcomplex.Pairing.IsProper · cited by 58Pairing.IsProperSSet.Subcomplex.Pairing.RankFunction.Cell · cited by 55RankFunction.CellSSet.Subcomplex.Pairing.RankFunction.Cell.horn · cited by 19Cell.hornRankFunction.sigmaHornCITED BYCITES

Cites10

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by24

Results whose statement or proof uses this declaration.