English
Let a act on an affine subspace s by applying the scalar action to every point; this defines the pointwise action on subspaces: a · s = s.map (DistribMulAction.toLinearMap k _ a).toAffineMap.
Русский
Пусть некоторая скалярная декомпозиция a действует на афинное подпространство s путём применения действия к каждой точке; это задаёт поэлементное действие над подпространствами: a · s = s.map (DistribMulAction.toLinearMap k _ a).toAffineMap.
LaTeX
$$$ a \\cdot s = s.map\\bigl( (\\mathrm{DistribMulAction.toLinearMap}\\ k\\ V\\ a).toAffineMap \\bigr) $$$
Lean4
/-- The multiplicative action on an affine subspace corresponding to applying the action to every
element.
This is available as an instance in the `Pointwise` locale.
TODO: generalize to include `SMul (P ≃ᵃ[k] P) (AffineSubspace k P)`, which acts on `P` with a
`VAdd` version of a `DistribMulAction`. -/
protected def pointwiseSMul : SMul M (AffineSubspace k V) where
smul a s := s.map (DistribMulAction.toLinearMap k _ a).toAffineMap
