English
A face S is equal to a particular Subcomplex obtained by representing S via an order-isomorphism; equivalently, face S = Subcomplex.ofSimplex(...).
Русский
Грань S равна заданной подподслою, полученному через представление S через упорядочение; то есть face S = Subcomplex.ofSimplex(...).
LaTeX
$$face(S) = Subcomplex.ofSimplex (X := Δ[n]) (objMk ((OrderHom.Subtype.val _).comp e.toOrderEmbedding.toOrderHom))$$
Lean4
theorem face_eq_ofSimplex {n : ℕ} (S : Finset (Fin (n + 1))) (m : ℕ) (e : Fin (m + 1) ≃o S) :
face.{u} S =
Subcomplex.ofSimplex (X := Δ[n]) (objMk ((OrderHom.Subtype.val _).comp e.toOrderEmbedding.toOrderHom)) :=
by
apply le_antisymm
· rintro ⟨k⟩ x hx
induction k using SimplexCategory.rec with
| _ k
rw [mem_face_iff] at hx
let φ : Fin (k + 1) →o S :=
{ toFun i := ⟨x i, hx i⟩
monotone' := (objEquiv x).toOrderHom.monotone }
refine ⟨Quiver.Hom.op (SimplexCategory.Hom.mk ((e.symm.toOrderEmbedding.toOrderHom.comp φ))), ?_⟩
obtain ⟨f, rfl⟩ := objEquiv.symm.surjective x
ext j : 1
simpa only [Subtype.ext_iff] using e.apply_symm_apply ⟨_, hx j⟩
· simp
