English
The action by units of A on R-submodules preserves the IsLattice structure: if M is IsLattice over A, then a units-action on M is IsLattice over A.
Русский
Действие единиц A на R-подпространства сохраняет структуру IsLattice: если M является IsLattice над A, то действие над M единицами сохраняет IsLattice над A.
LaTeX
$$$ \\text{instance smul } [IsLattice A M] (a : A^{\\times}) : IsLattice A \\,(a \\cdot M) $$$
Lean4
/-- The action of `Aˣ` on `R`-submodules of `V` preserves `IsLattice`. -/
instance smul [IsLattice A M] (a : Aˣ) : IsLattice A (a • M : Submodule R V)
where
fg := by
obtain ⟨s, rfl⟩ := IsLattice.fg (M := M)
rw [Submodule.smul_span]
have : Finite (a • (s : Set V) : Set V) := Finite.Set.finite_image _ _
exact Submodule.fg_span (Set.toFinite (a • (s : Set V)))
span_eq_top := by
rw [Submodule.coe_pointwise_smul, ← Submodule.smul_span, IsLattice.span_eq_top]
ext x
refine ⟨fun _ ↦ trivial, fun _ ↦ ?_⟩
rw [show x = a • a⁻¹ • x by simp]
exact Submodule.smul_mem_pointwise_smul _ _ _ (by trivial)
