prop_shift_iff_of_isStableUnderShift

English

Let G be an additive group with a shift functor; if P is stable under shifts by elements of G and closed under isomorphisms, then P(X⟦g⟧) ⇔ P(X).

Русский

Пусть G — аддитивная группа с функтою сдвига; если P стабильно по сдвигам на элементы G и замкну по изоморфизмам, тогда P(X⟦g⟧) ⇔ P(X).

LaTeX

$$$P\text{ is stable under shift by } G \;\Rightarrow\; P(X⟦g⟧) \Leftrightarrow P(X)$$$

Lean4

theorem prop_shift_iff_of_isStableUnderShift {G : Type*} [AddGroup G] [HasShift C G] [P.IsStableUnderShift G]
    [P.IsClosedUnderIsomorphisms] (X : C) (g : G) : P (X⟦g⟧) ↔ P X :=
  by
  refine ⟨fun hX ↦ ?_, P.le_shift g _⟩
  rw [← P.shift_zero G, ← P.shift_shift g (-g) 0 (by simp)]
  exact P.le_shift (-g) _ hX

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