[Merged by Bors] - feat(linear_algebra/clifford_algebra/conjugation): reverse and involute are grade-preserving

[eric-wieser]

This shows that various submodules are preserved under submodule.map by reverse or involute.

---

• depends on: [Merged by Bors] - feat(linear_algebra/clifford_algebra): lemmas about mapping submodules #12399

The related results x ∈ even_odd Q 0 ↔ involute x = x and x ∈ even_odd Q 1 ↔ involute x = -x will come in a future PR.

[eric-wieser]

I tried to state this in terms of submodule.map instead, but found it to be rather annoying:

lemma _root_.submodule.map_eq_self_of_involutive_of_le {p : submodule R M}
  {f : M →ₗ[R] M} (hf : function.involutive f) (h : p.map f ≤ p) : p.map f = p :=
have f_comp_f : f.comp f = linear_map.id := linear_map.ext hf,
have heq : p = (p.map f).map f, by rw [←submodule.map_comp, f_comp_f, submodule.map_id],
le_antisymm h $ heq.trans_le $ (submodule.map_strict_mono_of_injective hf.injective).monotone h

lemma ι_range_map_reverse : (ι Q).range.map reverse = (ι Q).range :=
submodule.map_eq_self_of_involutive_of_le reverse_involutive $ begin
  rintros _ ⟨_, ⟨m, rfl⟩, rfl⟩,
  rw reverse_ι,
  exact linear_map.mem_range_self _ _
end

lemma submodule_mul_map_reverse (p q : submodule R $ clifford_algebra Q) :
  (p * q).map reverse = q.map reverse * p.map reverse := sorry

lemma submodule_pow_map_reverse (p : submodule R $ clifford_algebra Q) (n : ℕ):
  (p ^ n).map reverse = p.map reverse ^ n := sorry

The lemmas in #12374 would probably help, but I don't know they'd make the proofs all that much shorter anyway.

[leanprover-community-bot-assistant]

This PR/issue depends on:

• [Merged by Bors] - feat(linear_algebra/clifford_algebra): lemmas about mapping submodules #12399
  By Dependent Issues (🤖). Happy coding!

[leanprover-community-bot-assistant]

This PR/issue depends on:

• [Merged by Bors] - feat(linear_algebra/clifford_algebra): lemmas about mapping submodules #12399
  By Dependent Issues (🤖). Happy coding!

[jcommelin]

Thanks 🎉

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests