compAlternatingMap_codRestrict — Mathlib

English

Composing with a codRestrict on the codomain corresponds to codRestrict after composition.

Русский

Композиция с codRestrict в кодомальной области соответствует codRestrict после композиции.

LaTeX

$$$ (g.codRestrict p h).compAlternatingMap f = (g.compAlternatingMap f).codRestrict p (\lambda v. h (f v)) $$$

Lean4

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

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