English
Assume [NeZero 2] and [NoZeroSMulDivisors R M], with h: f x = 2 and Disjoint p (R ∙ x). Then p ∈ End.invtSubmodule (reflection h) iff p ≤ ker f.
Русский
Пусть [2 ≠ 0] и [NoZeroSMulDivisors R M], с h: f x = 2 и Disjoint p (R ∙ x). Тогда p инвариантно относительно reflection h тогда и только тогда, когда p ⊆ ker f.
LaTeX
$$$\\text{Under }[NeZero(2)], [NoZeroSMulDivisors\\ R\\ M],\\ h:\\ f x=2,\\ text{ and }hp:\\ Disjoint\\ p\\ (R\\cdot x),\\\\\n p\\in End.invtSubmodule(\\mathrm{reflection}(h))\\iff p\\le \\ker f.$$$
Lean4
theorem _root_.Submodule.mem_invtSubmodule_reflection_iff [NeZero (2 : R)] [NoZeroSMulDivisors R M] (h : f x = 2)
{p : Submodule R M} (hp : Disjoint p (R ∙ x)) : p ∈ End.invtSubmodule (reflection h) ↔ p ≤ LinearMap.ker f :=
by
refine ⟨fun h' y hy ↦ ?_, fun h' y hy ↦ ?_⟩
· have hx : x ≠ 0 := by rintro rfl; exact two_ne_zero (α := R) <| by simp [← h]
suffices f y • x ∈ p
by
have aux : f y • x ∈ p ⊓ (R ∙ x) := ⟨this, Submodule.mem_span_singleton.mpr ⟨f y, rfl⟩⟩
rw [hp.eq_bot, Submodule.mem_bot, smul_eq_zero] at aux
exact aux.resolve_right hx
specialize h' hy
simp only [Submodule.mem_comap, LinearEquiv.coe_coe, reflection_apply] at h'
simpa using p.sub_mem h' hy
· have hy' : f y = 0 := by simpa using h' hy
simpa [reflection_apply, hy']
