A pairing for the pushout-product of a horn inclusion and a boundary inclusion #
Let l : Fin (m + 2) and n : ℕ. In this file, we construct a regular pairing
for the subcomplex unionProd Λ[m + 1, l] ∂Δ[n] of Δ[m + 1] ⊗ Δ[n]. It follows
immediately that the inclusion of the union of Λ[m + 1, l] ⊗ Δ[n] and
Δ[m + 1] ⊗ ∂Δ[n] in Δ[m + 1] ⊗ Δ[n] is a (strong) anodyne extension
(which is inner when l ≠ 0 and l ≠ Fin.last _).
The main construction works only when l ≠ Fin.last _, i.e. l = k.castSucc
for k : Fin (m + 1): the remaining case is obtained using symmetries and
the case k = 0.
In order to do the case of unionProd Λ[m + 1, k.castSucc] ∂Δ[n] for k : Fin (m + 1),
we follow the proof by Sean Moss. Let us consider a nondegenerate d-simplex x of
Δ[m + 1] ⊗ Δ[n] which does not belong to unionProd Λ[m + 1, k.castSucc] ∂Δ[n].
x can be thought as a "walk" on the vertices {0, ..., m + 1} × {0, ..., n}
of Δ[m + 1] ⊗ Δ[n] (this is actually a strictly monotone map
Fin (d + 1) → Fin (m + 2) × Fin (n + 1)).
The condition that x does not belong to unionProd Λ[m + 1, k.castSucc] ∂Δ[n]
translates by saying that x reaches all the rows
(see the lemma prodStdSimplex.pairingCore.mem_range_right)
and all the columns expect the k.castSucc-th
(see the lemma prodStdSimplex.pairingCore.mem_range_left). This puts
constraints for each i on the vector from x i to x (i + 1):
it has to be (0, 1), (1,0), (1,1), (2, 0) or (2, 1) (the last two
cases may appear only if the k.castSucc-th column is skipped).
We introduce a predicate IsIndex taking x and l : Fin (d + 1) as arguments
and which is satisfied if l is the smallest i such that x l is
in the k.succ column, l ≠ 0, and the vector from x (l.pred _) to x l
is exactly (1, 0).
The type (I) simplices for the pairing are those x such that there exists l
such that the predicate IsIndex hold. The corresponding type (II) simplex
is obtained by removing x (l.pred _) from the walk.
References #
Let x be a nondegenerate d-simplex of Δ[m + 1] ⊗ Δ[n] which
does not belong to Λ[m + 1, k.castSucc].unionProd ∂Δ[n]. In particular,
x induces a strictly monotone map from Fin (d + 1) to
{0, ..., m + 1} × {0, ..., n}. We introduce a predicate on elements in
Fin (d + 1) which shall be satisfied for l.succ (l : Fin d)
if x l.castSucc = (k.castSucc, t) and x l.succ = (k.succ, t)
for some t. The nondegenerate simplices x such that there exists
such a l shall be the type (I) simplices of a pairing, and the
corresponding type (II) simplex shall be obtained by deleting x l.castSucc.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Let x be a nondegenerate d-simplex of Δ[m + 1] ⊗ Δ[n] which
does not belong to Λ[m + 1, k.castSucc].unionProd ∂Δ[n]. This is
the finite subset of Fin (d + 1) consisting of those l such
that x l is of the form (k.succ, _).
Equations
Instances For
Let x be a nondegenerate d-simplex of Δ[m + 1] ⊗ Δ[n] which
does not belong to Λ[m + 1, k.castSucc].unionProd ∂Δ[n]. This is
the smallest l : Fin (d + 1) such that x l is of the form (k.succ, _).
Equations
Instances For
The type (II) simplex obtained as a face of a type (I) simplex.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The type of type (I) simplices for the pairing
the nondegenerate simplex
- d : ℕ
the dimension of the 1-codimensional face
the index attached to the corresponding type (II) simplex
Instances For
Let x be a nondegenerate simplex of Δ[m + 1] ⊗ Δ[n] which
does not belong to Λ[m + 1, k.castSucc].unionProd ∂Δ[n]. This is
the property that x is a type (II) simplex for the pairing
prodStdSimplex.pairingCore that is constructed below.
Equations
- SSet.prodStdSimplex.pairingCore.IsType₂ x = ∀ (d : ℕ) (hd : x.dim = d) (l : Fin (d + 1)), ¬SSet.prodStdSimplex.pairingCore.IsIndex x hd l
Instances For
Auxiliary definition for IsType₂.simplex. This gives the underlying
data of the type (I) simplex reconstructed from a type (II) simplex.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The type (I) simplex reconstructed from a type (II) simplex.
Equations
- hx.simplex hd = SSet.prodStdSimplex.objEquiv.symm { toFun := SSet.prodStdSimplex.pairingCore.IsType₂.φ x hd, monotone' := ⋯ }
Instances For
The type (I) simplex reconstructed from a type (II) simplex.
Equations
- hx.type₁ hd = { x := SSet.Subcomplex.N.mk (hx.simplex hd) ⋯ ⋯, d := d, hd := ⋯, index := SSet.prodStdSimplex.pairingCore.min x hd, isIndex := ⋯ }
Instances For
A weak rank function for pairingCore k n.
Equations
- SSet.prodStdSimplex.weakRankFunction k n = { rank := fun (s : (SSet.prodStdSimplex.pairingCore k n).ι) => (SSet.prodStdSimplex.pairingCore.finset s.x ⋯).card, lt := ⋯ }