HoTT.Algebra.AbGroups.Centralizer.v.alectryon.json

From HoTT Require Import Basics Types Truncations.Core.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).G: Group
g, h, k: G
p: centralizer g h
q: centralizer g k
centralizer g (h * k)
Proof.G: Group
g, h, k: G
p: centralizer g h
q: centralizer g k
centralizer g (h * k)
  refine (grp_assoc _ _ _ @ _).G: Group
g, h, k: G
p: centralizer g h
q: centralizer g k
g * h * k = h * k * g
  refine (ap (fun x => x * k) p @ _).G: Group
g, h, k: G
p: centralizer g h
q: centralizer g k
h * g * k = h * k * g
  refine ((grp_assoc _ _ _)^ @ _).G: Group
g, h, k: G
p: centralizer g h
q: centralizer g k
h * (g * k) = h * k * g
  refine (ap (fun x => h * x) q @ _).G: Group
g, h, k: G
p: centralizer g h
q: centralizer g k
h * (k * g) = h * k * g
  apply grp_assoc.
Defined.

Definition centralizer_inverse {G : Group} (g h : G)
           (p : centralizer g h)
  : centralizer g h^.G: Group
g, h: G
p: centralizer g h
centralizer g h^
Proof.G: Group
g, h: G
p: centralizer g h
centralizer g h^
  unfold centralizer in *.G: Group
g, h: G
p: g * h = h * g
g * h^ = h^ * g
  symmetry.G: Group
g, h: G
p: g * h = h * g
h^ * g = g * h^
  apply grp_g1_1g.G: Group
g, h: G
p: g * h = h * g
h^ * g * 1 = 1 * (g * h^)
  refine (ap ((_ * g) *.) (grp_inv_r h)^ @ _ @ ap (.* (g * _)) (grp_inv_l h)).G: Group
g, h: G
p: g * h = h * g
h^ * g * (h * h^) = h^ * h * (g * h^)
  refine (grp_assoc _ _ _ @ _ @ (grp_assoc _ _ _)^).G: Group
g, h: G
p: g * h = h * g
h^ * g * h * h^ = h^ * h * g * h^
  refine (ap (.* h^) _).G: Group
g, h: G
p: g * h = h * g
h^ * g * h = h^ * h * g
  refine ((grp_assoc _ _ _)^ @ _ @ grp_assoc _ _ _).G: Group
g, h: G
p: g * h = h * g
h^ * (g * h) = h^ * (h * g)
  exact (ap (h^ *.) p).
Defined.

Instance issubgroup_centralizer {G : Group} (g : G)
  : IsSubgroup (centralizer g).G: Group
g: G
IsSubgroup (centralizer g)
Proof.G: Group
g: G
IsSubgroup (centralizer g)
  srapply Build_IsSubgroup.G: Group
g: G
centralizer g 1
G: Group
g: G
forall x y : G, centralizer g x -> centralizer g y -> centralizer g (x * y)
G: Group
g: G
forall x : G, centralizer g x -> centralizer g x^
  -G: Group
g: G
centralizer g 1 apply centralizer_unit.
  -G: Group
g: G
forall x y : G, centralizer g x -> centralizer g y -> centralizer g (x * y) apply centralizer_sgop.
  -G: Group
g: G
forall x : G, centralizer g x -> centralizer g x^ 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').G, H: Group
f: GroupHomomorphism G H
g, g': G
centralizer g g' -> centralizer (f g) (f g')
Proof.G, H: Group
f: GroupHomomorphism G H
g, g': G
centralizer g g' -> centralizer (f g) (f g')
  unfold centralizer.G, H: Group
f: GroupHomomorphism G H
g, g': G
g * g' = g' * g -> f g * f g' = f g' * f g
  intro p.G, H: Group
f: GroupHomomorphism G H
g, g': G
p: g * g' = g' * g
f g * f g' = f g' * f g
  lhs_V napply grp_homo_op; rhs_V napply grp_homo_op.G, H: Group
f: GroupHomomorphism G H
g, g': G
p: g * g' = g' * g
f (g * g') = f (g' * g)
  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'.G, H: Group
f: GroupIsomorphism G H
g, g': G
centralizer (f g) (f g') -> centralizer g g'
Proof.G, H: Group
f: GroupIsomorphism G H
g, g': G
centralizer (f g) (f g') -> centralizer g g'
  intro p.G, H: Group
f: GroupIsomorphism G H
g, g': G
p: centralizer (f g) (f g')
centralizer g g'
  rewrite <- (eissect f g), <- (eissect f g').G, H: Group
f: GroupIsomorphism G H
g, g': G
p: centralizer (f g) (f g')
centralizer (f^-1 (f g)) (f^-1 (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)).G: Group
gen: Unit -> G
Commutative group_sgop
Proof.G: Group
gen: Unit -> G
Commutative group_sgop
  intros h k.G: Group
gen: Unit -> G
h, k: cyclic_subgroup_from_unit gen
group_sgop h k = group_sgop k h
  destruct h as [h H]; cbn in H.G: Group
gen: Unit -> G
h: G
H: Trunc (-1) (subgroup_generated_type (hfiber gen) h)
k: cyclic_subgroup_from_unit gen
group_sgop (h; H) k = group_sgop k (h; H)
  destruct k as [k K]; cbn in K.G: Group
gen: Unit -> G
h: G
H: Trunc (-1) (subgroup_generated_type (hfiber gen) h)
k: G
K: Trunc (-1) (subgroup_generated_type (hfiber gen) k)
group_sgop (h; H) (k; K) = group_sgop (k; K) (h; H)
  strip_truncations.G: Group
gen: Unit -> G
h, k: G
K: subgroup_generated_type (hfiber gen) k
H: subgroup_generated_type (hfiber gen) h
group_sgop (h; tr H) (k; tr K) = group_sgop (k; tr K) (h; tr H)
  (* It's enough to check equality after including into [G]: *)
  apply (equiv_ap_isembedding (subgroup_incl _) _ _)^-1.G: Group
gen: Unit -> G
h, k: G
K: subgroup_generated_type (hfiber gen) k
H: subgroup_generated_type (hfiber gen) h
subgroup_incl (cyclic_subgroup_from_unit gen)
  (group_sgop (h; tr H) (k; tr K)) =
subgroup_incl (cyclic_subgroup_from_unit gen)
  (group_sgop (k; tr K) (h; tr H))  cbn.G: Group
gen: Unit -> G
h, k: G
K: subgroup_generated_type (hfiber gen) k
H: subgroup_generated_type (hfiber gen) h
h * k = k * h
  induction H as [h [[] p]| |h1 h2 H1 H2 IHH1 IHH2].G: Group
gen: Unit -> G
k: G
K: subgroup_generated_type (hfiber gen) k
h: G
p: gen tt = h
h * k = k * h
G: Group
gen: Unit -> G
k: G
K: subgroup_generated_type (hfiber gen) k
1 * k = k * 1
G: Group
gen: Unit -> G
k: G
K: subgroup_generated_type (hfiber gen) k
h1, h2: G
H1: subgroup_generated_type (hfiber gen) h1
IHH1: subgroup_generated_type (hfiber gen) h2
H2: h1 * k = k * h1
IHH2: h2 * k = k * h2
h1 * h2^ * k = k * (h1 * h2^)
  - (* The case when [h = g]: *)G: Group
gen: Unit -> G
k: G
K: subgroup_generated_type (hfiber gen) k
h: G
p: gen tt = h
h * k = k * h
    induction p.G: Group
gen: Unit -> G
k: G
K: subgroup_generated_type (hfiber gen) k
gen tt * k = k * gen tt
    induction K as [k [[] q]| |k1 k2 K1 K2 IHK1 IHK2].G: Group
gen: Unit -> G
k: G
q: gen tt = k
gen tt * k = k * gen tt
G: Group
gen: Unit -> G
gen tt * 1 = 1 * gen tt
G: Group
gen: Unit -> G
k1, k2: G
K1: subgroup_generated_type (hfiber gen) k1
IHK1: subgroup_generated_type (hfiber gen) k2
K2: gen tt * k1 = k1 * gen tt
IHK2: gen tt * k2 = k2 * gen tt
gen tt * (k1 * k2^) = k1 * k2^ * gen tt
    + (* The case when k = g: *)G: Group
gen: Unit -> G
k: G
q: gen tt = k
gen tt * k = k * gen tt
      induction q.G: Group
gen: Unit -> G
gen tt * gen tt = gen tt * gen tt
      reflexivity.
    + (* The case when [k = mon_unit]: *)G: Group
gen: Unit -> G
gen tt * 1 = 1 * gen tt
      apply centralizer_unit.
    + (* The case when [k = k1 (-k2)]: *)G: Group
gen: Unit -> G
k1, k2: G
K1: subgroup_generated_type (hfiber gen) k1
IHK1: subgroup_generated_type (hfiber gen) k2
K2: gen tt * k1 = k1 * gen tt
IHK2: gen tt * k2 = k2 * gen tt
gen tt * (k1 * k2^) = k1 * k2^ * gen tt
      srapply (issubgroup_in_op_inv (H:=centralizer (gen tt))); assumption.
  - (* The case when [h = mon_unit]: *)G: Group
gen: Unit -> G
k: G
K: subgroup_generated_type (hfiber gen) k
1 * k = k * 1
    symmetry; apply centralizer_unit.
  - (* The case when [h = h1 (-h2)]: *)G: Group
gen: Unit -> G
k: G
K: subgroup_generated_type (hfiber gen) k
h1, h2: G
H1: subgroup_generated_type (hfiber gen) h1
IHH1: subgroup_generated_type (hfiber gen) h2
H2: h1 * k = k * h1
IHH2: h2 * k = k * h2
h1 * h2^ * k = k * (h1 * h2^)
    symmetry.G: Group
gen: Unit -> G
k: G
K: subgroup_generated_type (hfiber gen) k
h1, h2: G
H1: subgroup_generated_type (hfiber gen) h1
IHH1: subgroup_generated_type (hfiber gen) h2
H2: h1 * k = k * h1
IHH2: h2 * k = k * h2
k * (h1 * h2^) = h1 * h2^ * k
    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).G: Group
H: G -> Type
IsSubgroup (subtype_centralizer H)
Proof.G: Group
H: G -> Type
IsSubgroup (subtype_centralizer H)
  srapply Build_IsSubgroup.G: Group
H: G -> Type
subtype_centralizer H 1
G: Group
H: G -> Type
forall x y : G,
subtype_centralizer H x ->
subtype_centralizer H y -> subtype_centralizer H (x * y)
G: Group
H: G -> Type
forall x : G, subtype_centralizer H x -> subtype_centralizer H x^
  -G: Group
H: G -> Type
subtype_centralizer H 1 apply tr.G: Group
H: G -> Type
forall h : G, H h -> centralizer h 1
    intros h Hh.G: Group
H: G -> Type
h: G
Hh: H h
centralizer h 1
    exact (centralizer_unit h).
  -G: Group
H: G -> Type
forall x y : G,
subtype_centralizer H x ->
subtype_centralizer H y -> subtype_centralizer H (x * y) intros x y cx cy.G: Group
H: G -> Type
x, y: G
cx: subtype_centralizer H x
cy: subtype_centralizer H y
subtype_centralizer H (x * y)
    strip_truncations; apply tr.G: Group
H: G -> Type
x, y: G
cy: forall h : G, H h -> centralizer h y
cx: forall h : G, H h -> centralizer h x
forall h : G, H h -> centralizer h (x * y)
    intros h Hh.G: Group
H: G -> Type
x, y: G
cy: forall h0 : G, H h0 -> centralizer h0 y
cx: forall h0 : G, H h0 -> centralizer h0 x
h: G
Hh: H h
centralizer h (x * y)
    exact (centralizer_sgop _ _ _ (cx h Hh) (cy h Hh)).
  -G: Group
H: G -> Type
forall x : G, subtype_centralizer H x -> subtype_centralizer H x^ intros x Hx.G: Group
H: G -> Type
x: G
Hx: subtype_centralizer H x
subtype_centralizer H x^
    strip_truncations; apply tr.G: Group
H: G -> Type
x: G
Hx: forall h : G, H h -> centralizer h x
forall h : G, H h -> centralizer h x^
    intros h Hh.G: Group
H: G -> Type
x: G
Hx: forall h0 : G, H h0 -> centralizer h0 x
h: G
Hh: H h
centralizer h x^
    exact (centralizer_inverse h x (Hx h Hh)).
Defined.

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