Centralizer.v

From HoTT Require Import Basics Types Truncations.Core.

Require Import HFiber AbelianGroup.


(* Given a group [G], we define the centralizer of an element [g : G] as a subgroup and use this to show that the cyclic subgroup generated by [g] is abelian. *)

Local Open Scope mc_scope.

Local Open Scope mc_mult_scope.


(* First we show that the collection of elements that commute with a fixed element [g] is a subgroup. *)

Definition centralizer {G : Group} (g : G)
  := fun h => g * h = h * g.


Definition centralizer_unit {G : Group} (g : G) : centralizer g mon_unit
  := grp_g1_1g _ _ idpath.


Definition centralizer_sgop {G : Group} (g h k : G)
           (p : centralizer g h) (q : centralizer g k)
  : centralizer g (h * k).

Proof.

  refine (grp_assoc _ _ _ @ _).

  refine (ap (fun x => x * k) p @ _).

  refine ((grp_assoc _ _ _)^ @ _).

  refine (ap (fun x => h * x) q @ _).

  apply grp_assoc.

Defined.


Definition centralizer_inverse {G : Group} (g h : G)
           (p : centralizer g h)
  : centralizer g h^.

Proof.

  unfold centralizer in *.

  symmetry.

  apply grp_g1_1g.

  refine (ap ((_ * g) *.) (grp_inv_r h)^ @ _ @ ap (.* (g * _)) (grp_inv_l h)).

  refine (grp_assoc _ _ _ @ _ @ (grp_assoc _ _ _)^).

  refine (ap (.* h^) _).

  refine ((grp_assoc _ _ _)^ @ _ @ grp_assoc _ _ _).

  exact (ap (h^ *.) p).

Defined.


Instance issubgroup_centralizer {G : Group} (g : G)
  : IsSubgroup (centralizer g).

Proof.

  srapply Build_IsSubgroup.

 apply centralizer_unit.

 apply centralizer_sgop.

 apply centralizer_inverse.

Defined.


Definition centralizer_subgroup {G : Group} (g : G)
  := Build_Subgroup G (centralizer g) _.


(** Homomorphisms preserve centralizers. *)

Definition centralizer_hom {G H : Group} (f : GroupHomomorphism G H) (g g' : G)
  : centralizer g g' -> centralizer (f g) (f g').

Proof.

  unfold centralizer.

  intro p.

  lhs_V napply grp_homo_op; rhs_V napply grp_homo_op.

  exact (ap f p).

Defined.


(** Isomorphisms reflect centralizers. *)

Definition centralizer_iso {G H : Group} (f : GroupIsomorphism G H) (g g' : G)
  : centralizer (f g) (f g') -> centralizer g g'.

Proof.

  intro p.

  rewrite <- (eissect f g), <- (eissect f g').

  exact (centralizer_hom (grp_iso_inverse f) _ _ p).

Defined.


(* Now we define cyclic subgroups.  We allow any map [Unit -> G] in this definition, because in applications (such as [Z_commutative]) we have no control over the map. *)

Definition cyclic_subgroup_from_unit {G : Group} (gen : Unit -> G) := subgroup_generated (hfiber gen).


(* When we have a particular element [g] of [G], we could choose the predicate to be [fun h => h = g], but to fit into the above definition, we use [unit_name g], which gives the predicate [fun h => hfiber (unit_name g) h]. *)

Definition cyclic_subgroup {G : Group} (g : G) := cyclic_subgroup_from_unit (unit_name g).


(* Any cyclic subgroup is commutative. *)

Instance commutative_cyclic_subgroup {G : Group} (gen : Unit -> G)
  : Commutative (@group_sgop (cyclic_subgroup_from_unit gen)).

Proof.

  intros h k.

  destruct h as [h H]; cbn in H.

  destruct k as [k K]; cbn in K.

  strip_truncations.

  (* It's enough to check equality after including into [G]: *)

apply (equiv_ap_isembedding (subgroup_incl _) _ _)^-1.

  cbn.

  induction H as [h [[] p]| |h1 h2 H1 H2 IHH1 IHH2].

 (* The case when [h = g]: *)

induction p.

    induction K as [k [[] q]| |k1 k2 K1 K2 IHK1 IHK2].

 (* The case when k = g: *)

induction q.

      reflexivity.

 (* The case when [k = mon_unit]: *)

apply centralizer_unit.

 (* The case when [k = k1 (-k2)]: *)

srapply (issubgroup_in_op_inv (H:=centralizer (gen tt))); assumption.

 (* The case when [h = mon_unit]: *)

symmetry; apply centralizer_unit.

 (* The case when [h = h1 (-h2)]: *)

symmetry.

    srapply (issubgroup_in_op_inv (H:=centralizer k)); unfold centralizer; symmetry; assumption.

Defined.


Definition abgroup_cyclic_subgroup {G : Group} (g : G) : AbGroup
  := Build_AbGroup (cyclic_subgroup g) _.


(** ** Centralizers of general subsets *)

(** The centralizer of the elements of [G] for which [H] holds. *)

Definition subtype_centralizer {G : Group} (H : G -> Type)
  : G -> Type
  (* Note the order of operations here.  We do this to match the original proofs for the centraliser of an element. *)
  := fun g => merely (forall h : G, H h -> centralizer h g).


(** The centralizer of any subset of [G] is a subgroup of [G]. *)

Instance issubgroup_subtype_centralizer {G : Group} (H : G -> Type)
  : IsSubgroup (subtype_centralizer H).

Proof.

  srapply Build_IsSubgroup.

 apply tr.

    intros h Hh.

    exact (centralizer_unit h).

 intros x y cx cy.

    strip_truncations; apply tr.

    intros h Hh.

    exact (centralizer_sgop _ _ _ (cx h Hh) (cy h Hh)).

 intros x Hx.

    strip_truncations; apply tr.

    intros h Hh.

    exact (centralizer_inverse h x (Hx h Hh)).

Defined.


Definition subtype_centralizer_subgroup
  {G : Group} (H : G -> Type)
  := Build_Subgroup G (subtype_centralizer H) _.

Timings for Centralizer.v