Group Theory in Mizar

• Inverse operator is denoted by double quotes, so x" denotes \(x^{-1}\) as defined in group_1.miz line 210 (func h" -> Element of G means h * it = 1_G & it * h = 1_G;)
  • This is also extended to, for a group \(G\), subsets \(A\subset G\) we'd have A" be the collection of g" for g in A, i.e., \(A^{-1}=\{g^{-1}|g\in A\}\); see line 57 of group_2.miz

let G be Group;
let A be Subset of G;
func A " -> Subset of G equals :: GROUP_2:def 1
{ (g ") where g is Element of G : g in A } ;

• the mode definition Subgroup of G, line 853 of group_2.miz; for some reason, if \(H\lt G\), then carr(H) is defined as the subset of the underlying set of \(G\) equal to the set underlying \(H\)
• The trivial subgroup of \(G\) is denoted (1).G, defined on line 1258 of group_2.miz as

  func (1).G -> strict Subgroup of G means
  :Def7:
  the carrier of it = {1_G};

• NOTE: the adjective "trivial" isn't actually defined until GROUP_6
• "strict" is a weird meta-term (c.f., discussion),

"strict" doesn't have its own definition as it is a special (in a way "meta" attribute) - it means that a term which has a structure type <Theta> has exactly the same selectors (fields) as introduced in the definition of the type <Theta>, so in your case only the selectors of a doubleLoopStr - any extension to that would break the "strictness". So you may think of a vector space as of a group, but it's not a "strict" group.

• "strict" for subgroup is on line 1011 of group_2.miz; it's a registration of a cluster. I believe it refers to being a "just" subgroup — your intuition should be "a set [not a topological space, not a manifold, not an algebraic variety, not any other gadget] equipped with a group structure and nothing else".
• (Omega).G (line of group_2.miz) seems to be the other trivial subgroup of \(G\), i.e., \(G\) itself
  • This seems to be following notation introduced in rlsub_1.miz, line 764; a comment before it notes this notation is used for improper subspaces
• Left cosets are defined on line 2448 of group_2.miz (right cosets are defined on line 2468)

• The index of a subgroup \(H\lt G\) is defined as the cardinality of left cosets of \(H\) on line 2789 of group_2.miz
• The intersection of two subgroups \(H_{1}\cap H_{2}\) is defined as H1 /\ H2 in group_2.miz
  • The join of two subgroups \(H_{1}\vee H_{2}\) is defined as H1 "\/" H2 in group_4.miz and this corresponds to \(\langle H_{1}, H_{2}\rangle\) (the subgroup generated by the elements of \(H_{1}\) and \(H_{2}\))
  • For normal subgroups \(N_{1}\), \(N_{2}\) of \(G\), their product \(N_{1}N_{2}\) is precisely \(N_{1}\vee N_{2}\), as proven in group_4:Th53
  • The lattice G of subgroups of \(G\) is defined in group_4.miz
  • More results concerning the lattice of subgroups may be found in latsubgr.miz, for example, the meet of a [nonempty] set of subgroups is defined in latsubgr.miz
• Conjugation of \(a\) by \(b\) (both elements of \(G\)) is denoted a |^ b, defined on lines 299–300 of group_3.miz
  • This is extended to subsets \(A\) and \(B\) of \(G\), A |^ B is the collection of conjugating elements of \(A\) by elements of \(B\) func A |^ B -> Subset of G equals {g |^ h : g in A & h in B};
  • We also have g |^ A and A |^ g for conjugating an element by members of a subset, and conjugating a subset by an element
• Conjugate subgroup to \(H\lt G\) is defined lines 897 et seq of group_3.miz as H |^ a (conjugate subgroup of a finite group is itself finite, as registration on line 1068 notes)
• a,b are_conjugated defined on line 1270 of group_3.miz if there is a \(g\in G\) such that a = b |^ g (and two subsets are conjugated, defined on line 1523; for two subgroups on line 1738)
• Conjugacy class of \(a\in G\) is defined as the subset of \(G\) given by a |^ carr (Omega).G around line 1367 of group_3.miz (and the conjugacy class of a subset of \(G\) is defined around line 1615; the conjugacy class for a subgroup defined on line 1810)
  • conjugate_Classes G defined line 1131 of weddwit.miz
• A normal subgroup is defined on line 1956 of group_3.miz as for a holds IT |^ a = the multMagma of IT and then it is registered as strict normal
• The normalizer for a subset \(A\subset G\) is defined on line 2419 of group_3.miz as func Normalizer A -> strict Subgroup of G means :Def14: the carrier of it = {h : A |^ h = A}; (normalizer of a subgroup is defined on line 2638)
• If \(A\) is a subset of a group \(G\), the gr A seems to be the smallest subgroup containing \(A\); this is defined in group_4.miz
  • This corresponds to the subgroup generated by \(A\subset G\), which we usually write as \(\langle A\rangle\)
• Frattini subgroup is tricky. Relevant code starts around 1371 of group_4.miz

::$N Frattini subgroup
  func Phi(G) -> strict Subgroup of G means
  :Def7:
  the carrier of it = meet{A
where A is Subset of G : ex H being strict Subgroup of G st A = the carrier of
H & H is maximal} if ex H being strict Subgroup of G st H is maximal otherwise
  it = the multMagma of G;

• The notation \(H_{1}\wedge H_{2}\) for the smallest group containing both \(H_{1}\) and \(H_{2}\) (defined line 1877 group_4.miz) it is given the name SubJoin on line 2636; dually, the submeet is defined on line 2680
• Lattice of subgroups defined line 2795 of group_4.miz
• Commutator of group elements line 331 of group_5.miz; commutators(A,B) for subsets of \(G\) on line 964; commutators(H1,H2) of subgroups defined on line 1091; and commutators G is defined as the commutator of the underlying set of \(G\) with itself
• A triple \([a,b,c]=[[a,b],c]\) line 662 of group_5.miz
• the smallest group containing commutators(A,B) is defined as [.A,B.] on line 1262; and similarly for subgroups [.H1,H2.] defined on line 1297
• the derived group is define on line 1578 of group_5.miz
• the center of \(G\) is defined on line 1775 of group_5.miz as a strict subgroup of \(G\) consisting of {a : for b holds a * b = b * a};
  • The Centralizer of an element \(a\in G\) is defined line 739 of weddwit.miz
  • The center for a skew-field \(R\) is defined on line 1508 of weddwit.miz, and the centralizer for an element of \(R\) is defined on line 1978
• The quotient group \(G/N\) is denoted as G./.N in Mizar, and it is defined on line 505 of group_6; the canonical mapping of \(N\to G/N\) is defined on line 1084 as the nat_hom
• Group morphisms are defined in group_6 as multiplicative functions between two groups
• Two groups \(G\) and \(H\) are_isomorphic if there exists a bijective group morphism between them ( group_6);
• The kernel of a morphism of groups is defined in group_6;
• The isomorphism theorems for groups is also defined in group_6;
  • There seems to be a small hack to describe the subgroup \(N\leq H\leq G\) corresponding to \(H/N\) as H./.(H,N)`*`
  • GROUP_6:Th29 says if M and N are normal subgroups of G such that M is a subgroup of N, then N./.(N,M)`*` is a normal Subgroup of G./.M
• a group \(G\) is "simple" if IT is not trivial and there is no nontrivial normal subgroup \(H\triangleleft G\) (i.e., \(H\neq 1\) and \(H\neq G\)) line 998 of group_9.miz
  • Be careful! There is some confusing double-negation in the definition of simple, but it is logically equivalent to

definition
  let IT be Group;
  attr IT is simple means :: GROUP_9:def 12
  (not IT is trivial &
  (for H being strict normal Subgroup of IT
   holds (H = (Omega).IT or H = (1).IT)));
end; 

• The chunk of text dealing with composition series begins on line 6701 of group_9.miz (the composition_series is defined on line 6708)
• The Jordan-Holder attribute for composition series of \(G\) (line 6821 of group_9.miz)
• Equivalence of composition series is defined (line 6835 of group_9.miz)
• Schreier refinement theorem begins (line 10378 of group_9.miz); the_schreier_series_of is defined 10383
• p-subgroup defined on line 1786 of group_10.miz
• is_Sylow_p-subgroup_of_prime defined line 2196 of group_10.miz
• the_sylow_p-subgroups_of_prime(p,G) defined line 3109 of group_10.miz

• Product groups are discussed in group_7, group_12, group_19, and briefly in a few other articles.
• For sets, the Cartesian product of a family of sets is scattered in several articles.
  • The Cartesian product of a family of sets is defined in CARD_3:def 2
  • A family of sets indexed by \(I\) is called a ManySortedSet of I in Mizar, and defined in pboole.miz
• The notion of a "family of groups" is defined using the following strategy in group_7:
  • A binary relation is defined as multMagma-yielding if every object in its range is a multMagma (GROUP_7:def 1)
  • A family of magmas indexed by \(I\) is defined as a multMagma-Family of I
  • We define a product of a family of magmas, which produces a [strict] magma.
  • We then define a number of attributes for a family of magmas: associative, commutative, Group-like; we cluster functorial registrations indicating the product of an associative family of magmas is an associative magma, etc.
  • This will give us, from the power of Mizar adjectives, the product of an associative group-like family of magmas is a group.
• If \(\mathcal{F}\) is a family of groups indexed by \(I\), the isomorphism of \(\mathcal{F}_{i}\) with "its obvious subgroup" in \(\prod\mathcal{F}\) is defined in group_12 (the isomorphism is (1ProdHom (F, i)) and the subgroup is ProjGroup (F,i)).
• In group_19, a family of groups indexed by \(I\) is defined as a group-like associative family of magmas.
• The basic design here is
  • if \(\mathcal{F}\) is a family of groups indexed by \(I\), then \(\mathcal{F}_{i}\) is a group and the Mizar notation for this would be F.i
  • if \(g\in\prod\mathcal{F}\) is an element of the product group, then \(g_{i}\in\mathcal{F}_{i}\) is written in Mizar as g.i (so g is a function with dom g = I).

• The permutation group is defined in MATRIX_1 as Group_of_Perm n
  • The attribute even is defined there
  • This is the Symmetric group on \(n\) symbols — i.e., \(S_{n}\) = Group_of_Perm n
  • The symmetric group on an arbitrary set \(X\) is defined in CAYLEY as SymGroup X — i.e., \(\mathrm{Sym}(X)\) = SymGroup X
  • If you want to prove properties about permutation groups, you should work with Group_of_Perm n.
• The group \(\mathbb{Z}\) is defined in GR_CY_1 as INT.Group
• The finite cyclic group \(\mathbb{Z}/n\mathbb{Z}\) is defined as INT.Group(n) in GR_CY_1

It seems that the notion of a group action and group representation are…well, kind of muddled in Mizar.

• Action of O,E defines how a set O acts on E, it's an abbreviation for the type Function of O,(Funcs (E,E)).
  • For O being a group, this is really "almost" a representation. We'd need to prove it's a homomorphism, in the sense that for any g,h in O we would have a.(g*h) = (a.g) * (a.h).
  • This is not a group action, which would be a type Function of [:O,E:],E such that for any g,h being Element of O and for any e being Element of E we would have it.(g,it.(h,e))=it.(g*h,e) as desired.
  • This definition is from Bourbaki; see Algebra chapter I § 3.1, §5.1 et seq.
• If we wanted to define a Representation of a group, probably we would need to:
  1. Define an adjective Representation-like on a Function of G,(Funcs (E,E)) as something like for g,h being Element of G holds IT.(g * h) = (IT.g) * (IT.h)
  2. Register Representation-like for Function of G,(Funcs (E,E))
  3. Define a type Representation of G means ex E st it is Representation-like for Function of G,(Funcs (E,E))
• An alternative plan would be:
  1. Define a structure RepresentationStr consisting of a set E and a mapping Function of G,(Funcs (E,E))
  2. Define an adjective Representation-like for RepresentationStr which ensures the Function of G,(Funcs (E,E)) is multiplicative
  3. Define a mode Representation is Representation-like RepresentationStr.