English
An induction principle for reasoning about morphisms in SimplexCategoryGenRel, where we compose with generators on the right.
Русский
Принцип индукции для рассуждений о морфизмах в 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}(n) \\to \\mathrm{mk}(m), \\forall i, P(u) \\to P(u \\circ \\delta_i)\\Big) \\\\ \\land \\Big(\\forall n m, \\forall u: \\mathrm{mk}(n) \\to \\mathrm{mk}(m+1), \\forall i, P(u) \\to P(u \\circ \\sigma_i)\\Big) \\\\ \\Rightarrow \\forall f: a \\to b, P(f) $$$$
Lean4
/-- An unrolled version of the induction principle obtained in the previous lemma. -/
@[elab_as_elim, cases_eliminator, induction_eliminator]
theorem hom_induction (P : MorphismProperty SimplexCategoryGenRel) (id : ∀ {n : ℕ}, P (𝟙 (mk n)))
(comp_δ : ∀ {n m : ℕ} (u : mk n ⟶ mk m) (i : Fin (m + 2)), P u → P (u ≫ δ i))
(comp_σ : ∀ {n m : ℕ} (u : mk n ⟶ mk (m + 1)) (i : Fin (m + 1)), P u → P (u ≫ σ i)) {a b : SimplexCategoryGenRel}
(f : a ⟶ b) : P f :=
by
suffices generators.multiplicativeClosure ≤ P
by
rw [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
| comp_of f g hf hg hrec =>
rcases hg with ⟨⟨i⟩⟩ | ⟨⟨i⟩⟩
· simpa using (comp_δ f i hrec)
· simpa using (comp_σ f i hrec)
