Zulip Chat Archive

Stream: maths

Topic: orthogonal group generated by reflections


Heather Macbeth (Nov 16 2021 at 05:20):

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 (Nov 16 2021 at 09:08):

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 (Nov 16 2021 at 12:50):

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

Heather Macbeth (Nov 16 2021 at 17:47):

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 (Nov 16 2021 at 17:48):

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 (Nov 16 2021 at 18:03):

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

Deniz Aydin (Nov 16 2021 at 18:55):

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 (Nov 16 2021 at 19:20):

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


Last updated: Dec 20 2023 at 11:08 UTC