map_strict_mono_or_ker_sup_lt_ker_sup

English

For any index set ι and p_i with ker f ≤ ⨅ i, p_i, we have map f (⨅ i, p_i) = ⨅ i, map f(p_i).

Русский

Для множества индексов ι и p_i c ker f ≤ ⨅ i, p_i имеем map f (⨅ i, p_i) = ⨅ i, map f(p_i).

LaTeX

$$$\operatorname{map}_f\Bigl(\bigwedge_i p_i\Bigr) = \bigwedge_i \operatorname{map}_f(p_i)$$$

Lean4

theorem map_strict_mono_or_ker_sup_lt_ker_sup (f : F) (hab : p < p') :
    Submodule.map f p < Submodule.map f p' ∨ LinearMap.ker f ⊓ p < LinearMap.ker f ⊓ p' :=
  by
  obtain (⟨h, -⟩ | ⟨-, h⟩) := Prod.mk_lt_mk.mp <| strictMono_inf_prod_sup (z := LinearMap.ker f) hab
  · simpa [inf_comm] using Or.inr h
  · apply Or.inl <| map_lt_map_of_le_of_sup_lt_sup hab.le h

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