map_comap_eq_of_le — Mathlib

English

Restricting the codomain of f to a submodule p yields a range equal to the preimage of range f under the subtype map: range(codRestrict p f hf) = comap p.subtype (range f).

Русский

Ограничение кодомапа до подмодуля p даёт образ, равный прообразу диапазона f по подтипу: range(codRestrict p f hf) = comap p.subtype (range f).

LaTeX

$$$\operatorname{range}(\operatorname{codRestrict} p f hf) = \operatorname{comap} p.subtype (\operatorname{range} f)$$$

Lean4

theorem _root_.Submodule.map_comap_eq_of_le [RingHomSurjective τ₁₂] {f : F} {p : Submodule R₂ M₂}
    (h : p ≤ LinearMap.range f) : (p.comap f).map f = p :=
  SetLike.coe_injective <| Set.image_preimage_eq_of_subset h

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