faceRepresentableBy — Mathlib

English

If S is order-isomorphic to Fin(m+1), the face S is representable by Δ[m].

Русский

Если S упорядочиваемо подобен Fin(m+1), грань S представима Δ[m].

LaTeX

$$faceRepresentableBy {n} (S : Finset (Fin (n+1))) (m : Nat) …$$

Lean4

/-- If `S : Finset (Fin (n + 1))` is order isomorphic to `Fin (m + 1)`,
then the face `face S` of `Δ[n]` is representable by `m`,
i.e. `face S` is isomorphic to `Δ[m]`, see `stdSimplex.isoOfRepresentableBy`. -/
def faceRepresentableBy {n : ℕ} (S : Finset (Fin (n + 1))) (m : ℕ) (e : Fin (m + 1) ≃o S) :
    (face S : SSet.{u}).RepresentableBy ⦋m⦌
    where
  homEquiv
    {j} :=
    { toFun
        f :=
        ⟨objMk ((OrderHom.Subtype.val S.toSet).comp (e.toOrderEmbedding.toOrderHom.comp f.toOrderHom)), fun _ ↦ by
          aesop⟩
      invFun := fun ⟨x, hx⟩ ↦
        SimplexCategory.Hom.mk
          { toFun i := e.symm ⟨(objEquiv x).toOrderHom i, hx (by aesop)⟩
            monotone' i₁ i₂
              h :=
              e.symm.monotone
                (by
                  simp only [Subtype.mk_le_mk]
                  exact OrderHom.monotone _ h) }
      left_inv
        f := by
        ext i : 3
        apply e.symm_apply_apply
      right_inv := fun ⟨x, hx⟩ ↦
        by
        induction j using SimplexCategory.rec with
        | _ j
        dsimp
        ext i : 2
        exact congr_arg Subtype.val (e.apply_symm_apply ⟨(objEquiv x).toOrderHom i, _⟩) }
  homEquiv_comp f g := by aesop

Похожие утверждения