span_orbit_mem_invtSubmodule — Mathlib

English

The span of the orbit of x under G lies in the invariant submodule corresponding to the action by g.

Русский

Образ порожденный орбитой x по действию G лежит в инвариантной подмодуле, соответствующей действию g.

LaTeX

$$x : M, g : G \;\Rightarrow\; \text{span}_R (MulAction.orbit G x) \in invtSubmodule (DistribMulAction.toLinearMap R M g)$$

Lean4

theorem span_orbit_mem_invtSubmodule {G : Type*} [Monoid G] [DistribMulAction G M] [SMulCommClass G R M] (x : M)
    (g : G) : span R (MulAction.orbit G x) ∈ invtSubmodule (DistribMulAction.toLinearMap R M g) :=
  by
  rw [mem_invtSubmodule, Submodule.span_le, Submodule.comap_coe]
  intro y hy
  simp only [Set.mem_preimage, DistribMulAction.toLinearMap_apply, SetLike.mem_coe]
  exact Submodule.subset_span <| MulAction.mem_orbit_of_mem_orbit g hy

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