orthogonal group generated by reflections

Stream: maths

[Heather Macbeth]

I thought it would be nice to do one of the easy entries from the undergrad list: the orthogonal group is generated by reflections.

If anyone is in the mood for a few algebra sorries (dimensions of submodules, generating sets for subgroups, etc), feel free to finish off the proof I have started at branch#three-reflections! I'm going to bed.

[Eric Wieser]

Do we have a group (F ≃ₗᵢ[ℝ] F) instance like docs#linear_equiv.automorphism_group? If so it might be nice to use list.prod instead of list.fold

[Heather Macbeth]

Indeed, docs#linear_isometry_equiv.group. Just hadn't seen list.prod :)

[Heather Macbeth]

In particular,

import group_theory.subgroup.basic

variables {G : Type*} [group G] {s : set G}

example (l : list s) : (l.map coe : list G).prod ∈ subgroup.closure s :=
sorry

[Heather Macbeth]

and

import linear_algebra.finite_dimensional

variables {K : Type*} [field K]
variables {E : Type*} [add_comm_group E] [module K E] [finite_dimensional K E]

open finite_dimensional

example {V W : submodule K E} {v : E} (h₁ : W ≤ V) (h₂ : v ∈ V) (h₃ : v ∉ W) :
  finrank K W < finrank K V :=
sorry

[Deniz Aydin]

For the second one:
submodule.finrank_lt_finrank_of_lt (set_like.lt_iff_le_and_exists.2 ⟨h₁, v, h₂, h₃⟩)

[Deniz Aydin]

the first wasn't quite as nice:

import group_theory.subgroup.basic

variables {G : Type*} [group G] {s : set G}

example (l : list s) : (l.map coe : list G).prod ∈ subgroup.closure s :=
begin
  apply subgroup.list_prod_mem (subgroup.closure s),
  intros x hx,
  rw list.mem_map at hx,
  rcases hx with ⟨a, _, hax⟩,
  rw ←hax,
  exact subgroup.subset_closure a.property,
end

[Heather Macbeth]

@Deniz Aydin Nice work! Feel free to push to the branch and/or open a PR ...