Built with Alectryon, running Coq+SerAPI v8.18.0+0.18.3. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
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. *)LocalOpen Scope mc_scope.LocalOpen Scope mc_mult_scope.(* First we show that the collection of elements that commute with a fixed element [g] is a subgroup. *)Definitioncentralizer {G : Group} (g : G)
:= funh => g * h = h * g.
G: Group g: G
centralizer g mon_unit
G: Group g: G
centralizer g mon_unit
exact (grp_unit_r _ @ (grp_unit_l _)^).Defined.
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)
G: Group g, h, k: G p: centralizer g h q: centralizer g k
g * h * k = h * k * g
G: Group g, h, k: G p: centralizer g h q: centralizer g k
h * g * k = h * k * g
G: Group g, h, k: G p: centralizer g h q: centralizer g k
h * (g * k) = h * k * g
G: Group g, h, k: G p: centralizer g h q: centralizer g k
h * (k * g) = h * k * g
apply grp_assoc.Defined.
G: Group g, h: G p: centralizer g h
centralizer g (- h)
G: Group g, h: G p: centralizer g h
centralizer g (- h)
G: Group g, h: G p: g * h = h * g
g * - h = - h * g
G: Group g, h: G p: g * h = h * g
- h * g = g * - h
G: Group g, h: G p: g * h = h * g
- h * g * mon_unit = mon_unit * (g * - h)
G: Group g, h: G p: g * h = h * g
- h * g * (h * - h) = - h * h * (g * - h)
G: Group g, h: G p: g * h = h * g
- h * g * h * - h = - h * h * g * - h
G: Group g, h: G p: g * h = h * g
- h * g * h = - h * h * g
G: Group g, h: G p: g * h = h * g
- h * (g * h) = - h * (h * g)
exact (ap (funx => (-h) * x) p).Defined.
G: Group g: G
IsSubgroup (centralizer g)
G: Group g: G
IsSubgroup (centralizer g)
G: Group g: G
centralizer g mon_unit
G: Group g: G
forallxy : G,
centralizer g x ->
centralizer g y -> centralizer g (x * y)
G: Group g: G
forallx : G, centralizer g x -> centralizer g (- x)
G: Group g: G
centralizer g mon_unit
apply centralizer_unit.
G: Group g: G
forallxy : G,
centralizer g x ->
centralizer g y -> centralizer g (x * y)
apply centralizer_sgop.
G: Group g: G
forallx : G, centralizer g x -> centralizer g (- x)
apply centralizer_inverse.Defined.Definitioncentralizer_subgroup {G : Group} (g : G)
:= Build_Subgroup G (centralizer g) _.(* 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. *)Definitioncyclic_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]. *)Definitioncyclic_subgroup {G : Group} (g : G) := cyclic_subgroup_from_unit (unit_name g).(* Any cyclic subgroup is commutative. *)
G: Group gen: Unit -> G
Commutative group_sgop
G: Group gen: Unit -> G
Commutative group_sgop
G: Group gen: Unit -> G h, k: cyclic_subgroup_from_unit gen
group_sgop h k = group_sgop k 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)
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)
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
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
mon_unit * k = k * mon_unit
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)
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
gen tt * k = k * gen tt
G: Group gen: Unit -> G k: G q: gen tt = k
gen tt * k = k * gen tt
G: Group gen: Unit -> G
gen tt * mon_unit = mon_unit * 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
G: Group gen: Unit -> G k: G q: gen tt = k
gen tt * k = k * gen tt
G: Group gen: Unit -> G
gen tt * gen tt = gen tt * gen tt
reflexivity.
G: Group gen: Unit -> G
gen tt * mon_unit = mon_unit * gen tt
apply centralizer_unit.
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
G: Group gen: Unit -> G k: G K: subgroup_generated_type (hfiber gen) k
mon_unit * k = k * mon_unit
symmetry; apply centralizer_unit.
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)
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