instRespectsLeftInd — Mathlib

English

If P respects left, then P.ind respects left; i.e. precomposition preserves the left-respecting structure along Functor.const and its liftings.

Русский

Если P сохраняет свойства слева (RespectsLeft), то и P.ind сохраняет, т.к. предкомпозиция сохраняет структуру слева через константного функторa и его отображения.

LaTeX

$$$ [P.\mathrm{RespectsLeft}\ Q] \Rightarrow P.\mathrm{ind}.\mathrm{RespectsLeft} Q $$$

Lean4

instance [P.RespectsLeft Q] : P.ind.RespectsLeft Q where
  precomp {X Y Z} i hi
    f := fun ⟨J, _, _, D, t, s, hs, hst⟩ ↦
    by
    refine ⟨J, ‹_›, ‹_›, D, (Functor.const J).map i ≫ t, s, hs, fun j ↦ ⟨?_, by simp [hst]⟩⟩
    exact RespectsLeft.precomp _ hi _ (hst j).1

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