English
There is an induction principle for properties of structured arrows: if a property holds for the identity arrow and is preserved under composition and certain isomorphisms, then it holds for all arrows in the structured arrow category.
Русский
Существуют индукционные правила для свойств структурированных стрелок: если свойство верно для тождественного стрелки и сохраняется при композиции и при определённых изоморфизмах, то оно верно для всех стрелок в категории структурированных стрелок.
LaTeX
$$$\forall P:\text{StructuredArrow}(L\!\!\! X)L\to\mathrm{Prop},\ P(\text{mk}(\mathrm{id}_{L X})) \\ \quad \Rightarrow \\ (\forall f,\phi,\ P(\text{mk}\,\phi) \Rightarrow P(\text{mk}(\phi \circ L\!\!\mathrm map f))) \\ \quad \Rightarrow \\ \forall g:\text{StructuredArrow}(L X)L,\ P(g) $$$
Lean4
@[elab_as_elim]
theorem induction_structuredArrow (hP₀ : P (StructuredArrow.mk (𝟙 (L.obj X))))
(hP₁ :
∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : L.obj X ⟶ L.obj Y₁),
P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ L.map f)))
(hP₂ :
∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : L.obj X ⟶ L.obj Y₂),
P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom L W w hw).inv)))
(g : StructuredArrow (L.obj X) L) : P g :=
by
let P' : StructuredArrow (W.Q.obj X) W.Q → Prop := fun g ↦ P (structuredArrowEquiv W W.Q L g)
rw [← (structuredArrowEquiv W W.Q L).apply_symm_apply g]
apply induction_structuredArrow' W P'
· convert hP₀
simp
· intro Y₁ Y₂ f φ hφ
convert hP₁ f (homEquiv W W.Q L φ) hφ
simp [homEquiv_comp]
· intro Y₁ Y₂ w hw φ hφ
convert hP₂ w hw (homEquiv W W.Q L φ) hφ
simp [homEquiv_comp, homEquiv_isoOfHom_inv]
