English
An induction principle for reasoning about morphisms in SimplexCategoryGenRel, where we compose with generators on the left.
Русский
Принцип индукции для рассуждений о морфизмах в SimplexCategoryGenRel, где мы левобочно композиционируем с генераторами.
LaTeX
$$$$ \\forall P : \\mathrm{MorphismProperty SimplexCategoryGenRel}, \\Big(\\forall n, P(\\mathrm{id}_{\\mathrm{mk}(n)})\\Big) \\\\ \\land \\Big(\\forall n m, \\forall u: \\mathrm{mk}(m+1) \\to \\mathrm{mk}(n), \\forall i, P(u) \\to P(\\delta_i \\circ u)\\Big) \\\\ \\land \\Big(\\forall n m, \\forall u: \\mathrm{mk}(m) \\to \\mathrm{mk}(n), \\forall i, P(u) \\to P(\\sigma_i \\circ u)\\Big) \\\\ \\Rightarrow \\forall f: a \\to b, P(f) $$$$
Lean4
/-- An induction principle for reasonning about morphisms in SimplexCategoryGenRel, where we compose
with generators on the right. -/
theorem hom_induction' (P : MorphismProperty SimplexCategoryGenRel) (id : ∀ {n : ℕ}, P (𝟙 (mk n)))
(δ_comp : ∀ {n m : ℕ} (u : mk (m + 1) ⟶ mk n) (i : Fin (m + 2)), P u → P (δ i ≫ u))
(σ_comp : ∀ {n m : ℕ} (u : mk m ⟶ mk n) (i : Fin (m + 1)), P u → P (σ i ≫ u)) {a b : SimplexCategoryGenRel}
(f : a ⟶ b) : P f :=
by
suffices generators.multiplicativeClosure' ≤ P
by
rw [← MorphismProperty.multiplicativeClosure_eq_multiplicativeClosure', multiplicativeClosure_isGenerator_eq_top,
top_le_iff] at this
rw [this]
apply MorphismProperty.top_apply
intro _ _ f hf
induction hf with
| of f h =>
rcases h with ⟨⟨i⟩⟩ | ⟨⟨i⟩⟩
· simpa using (δ_comp (𝟙 _) i id)
· simpa using (σ_comp (𝟙 _) i id)
| id n => exact id
| of_comp f g hf hg hrec =>
rcases hf with ⟨⟨i⟩⟩ | ⟨⟨i⟩⟩
· simpa using (δ_comp g i hrec)
· simpa using (σ_comp g i hrec)
