K implies Frattinifree
This article gives the statement and possibly, proof, of an implication relation between two group properties. That is, it states that every group satisfying the first group property must also satisfy the second group property
View all group property implications  View all group property nonimplications

This article describes a fact or result that is not basic but it still wellestablished and standard. The fact may involve terms that are themselves nonbasic
View other semibasic facts in group theory
VIEW FACTS USING THIS: directly  directly or indirectly, upto two steps  directly or indirectly, upto three steps
VIEW: Survey articles about this
Contents
Statement
Verbal statement
Every Kgroup is a Frattinifree group. In other words, the Frattini subgroup of any Kgroup is trivial.
Symbolic statement
Let be a Kgroup. Then the Frattini subgroup is trivial.
Propertytheoretic statement
The group property of being a Kgroup is stronger than the group property of being a Frattinifree group.
Definitions used
Definitions for Kgroup
A Kgroup is a group wih the property that every subgroup has a lattice complement. That is, a group is a Kgroup if for any subgroup of , there is a subgroup such that ∩ is trivial and the subgroup generated by and is the whole of .
Definitions for Frattinifree group
A Frattinifree group is a group with the property that the intersection of all its maximal subgroups (called its Frattini subgroup) is trivial. Equivalently, for any nontrivial element, there is a maximal subgroup not containing that element.
Facts used
Proof
Symbolfree proof
 A Kgroup has the property that every cyclic subgroup has a lattice complement.
 The set of subgroups that do not contain the generator of the cyclic subgroup, ordered by subgroup inclusion, satisfies the conditions needed for Zorn's lemma, and hence there is a maximal element in this
 Any subgroup maximal with respect to not containing this element, must be a maximal subgroup of the group.
 Thus, given any element, there is a maximal subgroup not containing it.
Proof with symbols
Let be a Kgroup and a nontrivial element of . We need to show that there is a maximal subgroup of not containing .
Let be the cyclic sugbroup generated by . Since is a Kgroup, there exists a proper subgroup of such that ∩ is trivial and the subgroup generated by and is the whole of .
Consider the family of subgroups of that contain do not contain . Under subgroup inclusion, this family forms a partially ordered set that satisfies the conditions for Zorn's lemma. Hence, by Zorn's lemma, there exists a subgroup maximal with respect to the property of not containing .
Since along with generates , along with also generates . Hence, any proper subgroup of containing must not contain . Since is maximal among such subgroups, is a maximal subgroup.
Thus, starting with an arbitrary nontrivial in , we have produced a maximal subgroup not containing .