English
For a linear equivalence e, the image under e of a p-invariant submodule is invariant under e.conj f if and only if p is invariant under f.
Русский
Для линейного эквивалента e образ подмодуля p, инвариантного относительно f, инвариантен относительно e.conj f тогда и только тогда, когда p инвариантно относительно f.
LaTeX
$$$p \mapsto p \in f.invtSubmodule \iff p \in (e^{-1} f e).invtSubmodule$$$
Lean4
@[simp]
theorem _root_.LinearEquiv.map_mem_invtSubmodule_conj_iff {R M N : Type*} [CommSemiring R] [AddCommMonoid M]
[Module R M] [AddCommMonoid N] [Module R N] {f : End R M} {e : M ≃ₗ[R] N} {p : Submodule R M} :
p.map e ∈ (e.conj f).invtSubmodule ↔ p ∈ f.invtSubmodule :=
by
change p.map e.toLinearMap ∈ _ ↔ _
have : e.symm.toLinearMap ∘ₗ ((e ∘ₗ f) ∘ₗ e.symm.toLinearMap) ∘ₗ e = f := by ext; simp
rw [LinearEquiv.conj_apply, mem_invtSubmodule, mem_invtSubmodule, Submodule.map_le_iff_le_comap,
Submodule.map_equiv_eq_comap_symm, ← Submodule.comap_comp, ← Submodule.comap_comp, this]
