English
Validation that the zero, negation, and addition laws satisfy AddCommGroup axioms for multilinear maps.
Русский
Проверка соблюдения аксиом аддитивной коммутативной группы для много-линейных отображений.
LaTeX
$$Axioms of AddCommGroup hold coordinatewise for multilinear maps.$$
Lean4
/-- The pushforward of an indexed collection of submodule `p i ⊆ M₁ i` by `f : M₁ → M₂`.
Note that this is not a submodule - it is not closed under addition. -/
def map [Nonempty ι] (f : MultilinearMap R M₁ M₂) (p : ∀ i, Submodule R (M₁ i)) : SubMulAction R M₂
where
carrier := f '' {v | ∀ i, v i ∈ p i}
smul_mem' := fun c _ ⟨x, hx, hf⟩ => by
let ⟨i⟩ := ‹Nonempty ι›
letI := Classical.decEq ι
refine ⟨update x i (c • x i), fun j => if hij : j = i then ?_ else ?_, hf ▸ ?_⟩
· rw [hij, update_self]
exact (p i).smul_mem _ (hx i)
· rw [update_of_ne hij]
exact hx j
· rw [f.map_update_smul, update_eq_self]
