Helper structure in order to construct pairings

In this file, we introduce a helper structure Subcomplex.PairingCore in order to construct a pairing for a subcomplex of a simplicial set. The main difference with Subcomplex.Pairing are that we provide an index type ι and a function dim : ι → ℕ which allow to parametrize type (II) and (I) simplices in such a way that, definitionally, their dimensions are respectively dim s or dim s + 1 for s : ι.

structure SSet.Subcomplex.PairingCore {X : SSet} (A : X.Subcomplex) : Type (max u (v + 1))

An helper structure in order to construct a pairing for a subcomplex of a simplicial set X. The main difference with Pairing is that we provide an index type ι and a function dim : ι → ℕ which allow to parametrize type (I) simplices as simplex s : X _⦋dim s + 1⦌ for s : ι, and type (II) simplices as a face of simplex s in X _⦋dim s⦌.

• ι : Type v

  the index type

• dim (s : self.ι) : ℕ

  the dimension of each type (II) simplex

• simplex (s : self.ι) : X.obj (Opposite.op (SimplexCategory.mk (self.dim s + 1)))

  the family of type (I) simplices

• index (s : self.ι) : Fin (self.dim s + 2)

  the corresponding type (II) simplex is the 1-codimensional face given by this index

• nonDegenerate₁ (s : self.ι) : self.simplex s ∈ X.nonDegenerate (self.dim s + 1)
• nonDegenerate₂ (s : self.ι) : CategoryTheory.SimplicialObject.δ X (self.index s) (self.simplex s) ∈ X.nonDegenerate (self.dim s)
• notMem₁ (s : self.ι) : self.simplex s ∉ A.obj (Opposite.op (SimplexCategory.mk (self.dim s + 1)))
• notMem₂ (s : self.ι) : CategoryTheory.SimplicialObject.δ X (self.index s) (self.simplex s) ∉ A.obj (Opposite.op (SimplexCategory.mk (self.dim s)))
• injective_type₁' {s t : self.ι} (h : { dim := self.dim s + 1, simplex := self.simplex s } = { dim := self.dim t + 1, simplex := self.simplex t }) : s = t
• injective_type₂' {s t : self.ι} (h : { dim := self.dim s, simplex := CategoryTheory.SimplicialObject.δ X (self.index s) (self.simplex s) } = { dim := self.dim t, simplex := CategoryTheory.SimplicialObject.δ X (self.index t) (self.simplex t) }) : s = t
• type₁_ne_type₂' (s t : self.ι) : { dim := self.dim s + 1, simplex := self.simplex s } ≠ { dim := self.dim t, simplex := CategoryTheory.SimplicialObject.δ X (self.index t) (self.simplex t) }
• surjective' (x : A.N) : ∃ (s : self.ι), x.toS = { dim := self.dim s + 1, simplex := self.simplex s } ∨ x.toS = { dim := self.dim s, simplex := CategoryTheory.SimplicialObject.δ X (self.index s) (self.simplex s) }

noncomputable def SSet.Subcomplex.Pairing.pairingCore {X : SSet} {A : X.Subcomplex} (P : A.Pairing) [P.IsProper] : A.PairingCore

The PairingCore structure induced by a pairing. The opposite construction is PairingCore.pairing.

Equations

• One or more equations did not get rendered due to their size.

def SSet.Subcomplex.PairingCore.type₁ {X : SSet} {A : X.Subcomplex} (h : A.PairingCore) (s : h.ι) : A.N

The type (I) simplices of h : A.PairingCore, as a family indexed by h.ι.

Equations

• h.type₁ s = SSet.Subcomplex.N.mk (h.simplex s) ⋯ ⋯

@[simp]

theorem SSet.Subcomplex.PairingCore.type₁_simplex {X : SSet} {A : X.Subcomplex} (h : A.PairingCore) (s : h.ι) : (h.type₁ s).simplex = h.simplex s

@[simp]

theorem SSet.Subcomplex.PairingCore.type₁_dim {X : SSet} {A : X.Subcomplex} (h : A.PairingCore) (s : h.ι) : (h.type₁ s).dim = h.dim s + 1

def SSet.Subcomplex.PairingCore.type₂ {X : SSet} {A : X.Subcomplex} (h : A.PairingCore) (s : h.ι) : A.N

The type (II) simplices of h : A.PairingCore, as a family indexed by h.ι.

Equations

• h.type₂ s = SSet.Subcomplex.N.mk (CategoryTheory.SimplicialObject.δ X (h.index s) (h.simplex s)) ⋯ ⋯

@[simp]

theorem SSet.Subcomplex.PairingCore.type₂_simplex {X : SSet} {A : X.Subcomplex} (h : A.PairingCore) (s : h.ι) : (h.type₂ s).simplex = CategoryTheory.SimplicialObject.δ X (h.index s) (h.simplex s)

@[simp]

theorem SSet.Subcomplex.PairingCore.type₂_dim {X : SSet} {A : X.Subcomplex} (h : A.PairingCore) (s : h.ι) : (h.type₂ s).dim = h.dim s

theorem SSet.Subcomplex.PairingCore.injective_type₁ {X : SSet} {A : X.Subcomplex} (h : A.PairingCore) : Function.Injective h.type₁

theorem SSet.Subcomplex.PairingCore.injective_type₂ {X : SSet} {A : X.Subcomplex} (h : A.PairingCore) : Function.Injective h.type₂

theorem SSet.Subcomplex.PairingCore.type₁_ne_type₂ {X : SSet} {A : X.Subcomplex} (h : A.PairingCore) (s t : h.ι) : h.type₁ s ≠ h.type₂ t

theorem SSet.Subcomplex.PairingCore.surjective {X : SSet} {A : X.Subcomplex} (h : A.PairingCore) (x : A.N) : ∃ (s : h.ι), x = h.type₁ s ∨ x = h.type₂ s

def SSet.Subcomplex.PairingCore.I {X : SSet} {A : X.Subcomplex} (h : A.PairingCore) : Set A.N

The type (I) simplices of h : A.PairingCore, as a subset of A.N.

Equations

• h.I = Set.range h.type₁

def SSet.Subcomplex.PairingCore.II {X : SSet} {A : X.Subcomplex} (h : A.PairingCore) : Set A.N

The type (II) simplices of h : A.PairingCore, as a subset of A.N.

Equations

• h.II = Set.range h.type₂

noncomputable def SSet.Subcomplex.PairingCore.equivI {X : SSet} {A : X.Subcomplex} (h : A.PairingCore) : h.ι ≃ ↑h.I

The bijection h.ι ≃ h.I when h : A.PairingCore.

Equations

• h.equivI = Equiv.ofInjective h.type₁ ⋯

@[simp]

theorem SSet.Subcomplex.PairingCore.equivI_apply_coe {X : SSet} {A : X.Subcomplex} (h : A.PairingCore) (a : h.ι) : ↑(h.equivI a) = h.type₁ a

noncomputable def SSet.Subcomplex.PairingCore.equivII {X : SSet} {A : X.Subcomplex} (h : A.PairingCore) : h.ι ≃ ↑h.II

The bijection h.ι ≃ h.II when h : A.PairingCore.

Equations

• h.equivII = Equiv.ofInjective h.type₂ ⋯

@[simp]

theorem SSet.Subcomplex.PairingCore.equivII_apply_coe {X : SSet} {A : X.Subcomplex} (h : A.PairingCore) (a : h.ι) : ↑(h.equivII a) = h.type₂ a

noncomputable def SSet.Subcomplex.PairingCore.pairing {X : SSet} {A : X.Subcomplex} (h : A.PairingCore) : A.Pairing

The pairing induced by h : A.PairingCore.

Equations

• h.pairing = { I := h.I, II := h.II, inter := ⋯, union := ⋯, p := h.equivII.symm.trans h.equivI }

@[simp]

theorem SSet.Subcomplex.PairingCore.pairing_I {X : SSet} {A : X.Subcomplex} (h : A.PairingCore) : h.pairing.I = h.I

@[simp]

theorem SSet.Subcomplex.PairingCore.pairing_II {X : SSet} {A : X.Subcomplex} (h : A.PairingCore) : h.pairing.II = h.II

@[simp]

theorem SSet.Subcomplex.PairingCore.pairing_p_equivII {X : SSet} {A : X.Subcomplex} (h : A.PairingCore) (x : h.ι) : h.pairing.p (h.equivII x) = h.equivI x

@[simp]

theorem SSet.Subcomplex.PairingCore.pairing_p_symm_equivI {X : SSet} {A : X.Subcomplex} (h : A.PairingCore) (x : h.ι) : h.pairing.p.symm (h.equivI x) = h.equivII x

class SSet.Subcomplex.PairingCore.IsProper {X : SSet} {A : X.Subcomplex} (h : A.PairingCore) : Prop

The condition that h : A.PairingCore is proper, i.e. for each s : h.ι, the type (II) simplex h.type₂ s is uniquely a 1-codimensional face of the type (I) simplex h.type₁ s.

• isUniquelyCodimOneFace (s : h.ι) : (h.type₂ s).IsUniquelyCodimOneFace (h.type₁ s).toS

theorem SSet.Subcomplex.PairingCore.isUniquelyCodimOneFace {X : SSet} {A : X.Subcomplex} (h : A.PairingCore) [h.IsProper] (s : h.ι) : (h.type₂ s).IsUniquelyCodimOneFace (h.type₁ s).toS

instance SSet.Subcomplex.PairingCore.instIsProperPairingOfIsProper {X : SSet} {A : X.Subcomplex} (h : A.PairingCore) [h.IsProper] : h.pairing.IsProper

@[simp]

theorem SSet.Subcomplex.PairingCore.isUniquelyCodimOneFace_index {X : SSet} {A : X.Subcomplex} (h : A.PairingCore) [h.IsProper] (s : h.ι) : ⋯.index ⋯ = h.index s

theorem SSet.Subcomplex.PairingCore.isUniquelyCodimOneFace_index_coe {X : SSet} {A : X.Subcomplex} (h : A.PairingCore) [h.IsProper] (s : h.ι) {d : ℕ} (hd : h.dim s = d) : ↑(⋯.index hd) = ↑(h.index s)

class SSet.Subcomplex.PairingCore.IsInner {X : SSet} {A : X.Subcomplex} (h : A.PairingCore) : Prop

The condition that h : A.PairingCore involves only inner horns.

• ne_zero (s : h.ι) : h.index s ≠ 0
• ne_last (s : h.ι) : h.index s ≠ Fin.last (h.dim s + 1)

instance SSet.Subcomplex.PairingCore.instIsInnerPairingOfIsInner {X : SSet} {A : X.Subcomplex} (h : A.PairingCore) [h.IsInner] [h.IsProper] : h.pairing.IsInner

def SSet.Subcomplex.PairingCore.AncestralRel {X : SSet} {A : X.Subcomplex} (h : A.PairingCore) (s t : h.ι) : Prop

The ancestrality relation on the index type of h : A.PairingCore.

Equations

• h.AncestralRel s t = (s ≠ t ∧ h.type₂ s < h.type₁ t)

theorem SSet.Subcomplex.PairingCore.ancestralRel_iff {X : SSet} {A : X.Subcomplex} (h : A.PairingCore) (s t : h.ι) : h.AncestralRel s t ↔ h.pairing.AncestralRel (h.equivII s) (h.equivII t)

class SSet.Subcomplex.PairingCore.IsRegular {X : SSet} {A : X.Subcomplex} (h : A.PairingCore) extends h.IsProper : Prop

When the ancestrality relation is well founded, we say that h : A.PairingCore is regular.

• isUniquelyCodimOneFace (s : h.ι) : (h.type₂ s).IsUniquelyCodimOneFace (h.type₁ s).toS
• wf : WellFounded h.AncestralRel

instance SSet.Subcomplex.PairingCore.instIsRegularPairingOfIsRegular {X : SSet} {A : X.Subcomplex} (h : A.PairingCore) [h.IsRegular] : h.pairing.IsRegular