mathlib

mathlib copied to clipboard

In this file we define lipschitz , pin_group and spin_group.

Here are some discussion about the latent ambiguity of definition : https://mathoverflow.net/q/427881/172242 and https://mathoverflow.net/q/251288/172242

The definition of the Lipschitz group {𝑥 ∈ 𝐶𝑙(𝑉,𝑞) │ 𝑥 𝑖𝑠 𝑖𝑛𝑣𝑒𝑟𝑡𝑖𝑏𝑙𝑒 𝑎𝑛𝑑 𝑥𝑣𝑥⁻¹∈ 𝑉} is given by: • Fulton, W. and Harris, J., 2004. Representation theory. New York: Springer, p.chapter 20. • https://en.wikipedia.org/wiki/Clifford_algebra#Lipschitz_group But they presumably form a group only in finite dimensions. So we define lipschitz with closure of all the elements in the form of ι Q m. We show this definition is at least as large as the other definition (See mem_lipschitz_conj_act_le and mem_lipschitz_involute_le) and the reverse statement presumably being true only in finite dimensions.

Note that the proofs of mem_lipschitz_conj_act_le and mem_lipschitz_involute_le are blocked by some PRs shown below.

---

• [x] depends on: #11468 [clifford algebra is isomorphic to exterior algebra if invertible 2]
• [x] depends on: #16202 [f (⅟r) = ⅟(f r)]
• [x] depends on: #16153 [triple products of repeated vectors]

Note that the proofs of mem_lipschitz_conj_act_le and mem_lipschitz_involute_le are blocked by some PRs.

This PR/issue depends on:

• ~~leanprover-community/mathlib#11468~~
• ~~leanprover-community/mathlib#16202~~
• ~~leanprover-community/mathlib#16153~~ By Dependent Issues (🤖). Happy coding!