English
If f is alternating with values in N and p is a submodule of N such that all f(v) lie in p, then the restricted map codRestrict(f,p,h) is an alternating map into p.
Русский
Если чередующееся отображение f принимает значения в N и p является подмодулем N, и все значения f(v) лежат в p, то ограниченное отображение codRestrict(f,p,h) является чередующимся отображением в p.
LaTeX
$$$ \text{codRestrict}(f,p,h) \in \operatorname{AltMap}_R(M,p,ι) $$$
Lean4
/-- Restrict the codomain of an alternating map to a submodule. -/
@[simps]
def codRestrict (f : M [⋀^ι]→ₗ[R] N) (p : Submodule R N) (h : ∀ v, f v ∈ p) : M [⋀^ι]→ₗ[R] p :=
{ f.toMultilinearMap.codRestrict p h with
toFun := fun v => ⟨f v, h v⟩
map_eq_zero_of_eq' := fun _ _ _ hv hij => Subtype.ext <| map_eq_zero_of_eq _ _ hv hij }
