Library HoTT.Algebra.AbGroups.Centralizer

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) _.

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.

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) _.

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 (∀ h : G, H h → centralizer h 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) _.