invtSubmodule_reflection_of_invtSubmodule_coreflection

English

For i ∈ ι and q ∈ Submodule R N with q ∈ invtSubmodule(P.coreflection i), the dual annihilator map transports into invtSubmodule(P.reflection i).

Русский

Для i и q ∈ Submodule R N, если q ∈ invtSubmodule(P.coreflection i), то q.dualAnnihilator.map(P.toPerfPair.symm) принадлежит invtSubmodule(P.reflection i).

LaTeX

$$$$ q \in invtSubmodule(P.coreflection(i)) \Rightarrow q.dualAnnihilator.map(P.toPerfPair.symm) \in invtSubmodule(P.reflection(i)). $$$$

Lean4

theorem invtSubmodule_reflection_of_invtSubmodule_coreflection (i : ι) (q : Submodule R N)
    (hq : q ∈ invtSubmodule (P.coreflection i)) :
    q.dualAnnihilator.map P.toPerfPair.symm ∈ invtSubmodule (P.reflection i) :=
  by
  rw [LinearEquiv.map_mem_invtSubmodule_iff, LinearEquiv.symm_symm, toPerfPair_conj_reflection,
    Module.End.mem_invtSubmodule, ← Submodule.map_le_iff_le_comap]
  exact (Submodule.dualAnnihilator_map_dualMap_le _ _).trans <| Submodule.dualAnnihilator_anti hq

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