ProCGroups.Frattini

11 Theorem | 2 Definition

This module formalizes Frattini-type constructions for profinite groups.

import

Mathlib.GroupTheory.Frattini
Mathlib.Topology.Algebra.Group.ClosedSubgroup

Imported by

None

Definition ProCGroups.Frattini.Subgroup.IsMaximalWithProperty GitHub

def Subgroup.IsMaximalWithProperty (P : Subgroup G → Prop) (H : Subgroup G) : Prop :=
  P H ∧
    H ≠ ⊤ ∧
    ∀ K : Subgroup G, H ≤ K → P K → K ≠ ⊤ → K = H

A subgroup is maximal with respect to a predicate P if it satisfies P, is proper, and every proper overgroup satisfying P is equal to it.

Theorem ProCGroups.Frattini.Subgroup.IsMaximalWithProperty.property GitHub

theorem property (hH : Subgroup.IsMaximalWithProperty (G := G) P H) :
    P H

A maximal subgroup with property P satisfies the property P.

Show proof

Theorem ProCGroups.Frattini.Subgroup.IsMaximalWithProperty.ne_top GitHub

theorem ne_top (hH : Subgroup.IsMaximalWithProperty (G := G) P H) :
    H ≠ ⊤

A maximal subgroup in the given class is a proper subgroup.

Show proof

Theorem ProCGroups.Frattini.Subgroup.IsMaximalWithProperty.eq_of_le GitHub

theorem eq_of_le (hH : Subgroup.IsMaximalWithProperty (G := G) P H)
    (hHK : H ≤ K) (hK : P K) (hKne : K ≠ ⊤) :
    K = H

Maximality forces a larger proper subgroup in the same class to be equal.

Show proof

Theorem ProCGroups.Frattini.Subgroup.IsMaximalOpen.isOpen GitHub

theorem isOpen
    (hH : Subgroup.IsMaximalWithProperty (G := G) (fun K => IsOpen (K : Set G)) H) :
    IsOpen (H : Set G)

A subgroup that is maximal among open subgroups is open.

Show proof

Theorem ProCGroups.Frattini.Subgroup.IsMaximalOpen.ne_top GitHub

theorem ne_top
    (hH : Subgroup.IsMaximalWithProperty (G := G) (fun K => IsOpen (K : Set G)) H) :
    H ≠ ⊤

A maximal subgroup in the given class is a proper subgroup.

Show proof

Theorem ProCGroups.Frattini.Subgroup.IsMaximalOpen.eq_of_le GitHub

theorem eq_of_le
    (hH : Subgroup.IsMaximalWithProperty (G := G) (fun K => IsOpen (K : Set G)) H)
    (hHK : H ≤ K)
    (hKopen : IsOpen (K : Set G)) (hKne : K ≠ ⊤) :
    K = H

Maximality forces a larger proper subgroup in the same class to be equal.

Show proof

Theorem ProCGroups.Frattini.Subgroup.IsMaximalClosed.isClosed GitHub

theorem isClosed
    (hH : Subgroup.IsMaximalWithProperty (G := G) (fun K => IsClosed (K : Set G)) H) :
    IsClosed (H : Set G)

A maximal closed subgroup is closed.

Show proof

Theorem ProCGroups.Frattini.Subgroup.IsMaximalClosed.ne_top GitHub

theorem ne_top
    (hH : Subgroup.IsMaximalWithProperty (G := G) (fun K => IsClosed (K : Set G)) H) :
    H ≠ ⊤

A maximal subgroup in the given class is a proper subgroup.

Show proof

Theorem ProCGroups.Frattini.Subgroup.IsMaximalClosed.eq_of_le GitHub

theorem eq_of_le
    (hH : Subgroup.IsMaximalWithProperty (G := G) (fun K => IsClosed (K : Set G)) H)
    (hHK : H ≤ K)
    (hKclosed : IsClosed (K : Set G)) (hKne : K ≠ ⊤) :
    K = H

Maximality forces a larger proper subgroup in the same class to be equal.

Show proof

Definition ProCGroups.frattiniWithin GitHub

def frattiniWithin (H : Subgroup G) : Subgroup G :=
  (frattini H).map H.subtype

The Frattini subgroup of \(H\), viewed back inside the ambient group \(G\).

Theorem ProCGroups.frattiniWithin_le GitHub

theorem frattiniWithin_le (H : Subgroup G) :
    frattiniWithin (G := G) H ≤ H

The Frattini subgroup within a class is contained in every subgroup from that class.

Show proof

Theorem ProCGroups.mem_frattiniWithin GitHub

@[simp] theorem mem_frattiniWithin {H : Subgroup G} {x : H} :
    (x : G) ∈ frattiniWithin (G := G) H ↔ x ∈ frattini H

Membership in the Frattini subgroup within a class means membership in every subgroup from that class.

Show proof

ProCGroups.Frattini

Declarations