subtype_compAlternatingMap_codRestrict

English

Restricting to a submodule then including back yields the original map.

Русский

Ограничение до подмодуля затем включение обратно возвращает исходное отображение.

LaTeX

$$$ p.\text{subtype} \circ_{\mathrm{Alt}} (f_{codRestrict}) = f $$$

Lean4

@[simp]
theorem subtype_compAlternatingMap_codRestrict (f : M [⋀^ι]→ₗ[R] N) (p : Submodule R N) (h) :
    p.subtype.compAlternatingMap (f.codRestrict p h) = f :=
  AlternatingMap.ext fun _ => rfl

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