English
If we have a natural equivalence for the system f and the auxiliary bijection data, then piEquivSucc forms a natural equivalence with f, i.e., it preserves the directed system structure through the successor step.
Русский
Если существует естественная эквиваленция для системы f и сопутствующих биекций, то piEquivSucc образует естественную эквиваленцию по отношению к f, сохраняя структуру направленной системы на шаге преемника.
LaTeX
$$$\\text{IsNatEquiv} f (piEquivSucc\\, equiv\\, e\\, hi)$$$
Lean4
theorem isNatEquiv_piEquivSucc [InverseSystem f] (H : ∀ x, (e x).1 = f (le_succ i) x) (nat : IsNatEquiv f equiv) :
IsNatEquiv f (piEquivSucc equiv e hi) := fun j k hj hk h x ↦
by
have lt_succ {j} := (lt_succ_iff_of_not_isMax (b := j) hi).mpr
obtain rfl | hj := le_succ_iff_eq_or_le.mp hj
· obtain rfl | hk := le_succ_iff_eq_or_le.mp hk
· simp [InverseSystem.map_self]
· funext l
rw [piEquivSucc, piSplitLE_lt (lt_succ hk), ← InverseSystem.map_map (f := f) hk (le_succ i), ← H, piLTProj,
nat le_rfl]
simp [piSplitLE_lt (l.2.trans_le hk)]
· rw [piEquivSucc, piSplitLE_lt (h.trans_lt <| lt_succ hj), nat hj, piSplitLE_lt (lt_succ hj)]
