Module

Frattini.lean

Nyll.ProCGroups.Frattini

13 declarations indexed from sourceView source ↗

Module documentation

Pro C Groups / Frattini

This module formalizes Frattini-type constructions for profinite groups.

Imports2

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

Imported by2

def

IsMaximalWithProperty

L31 ↗

ProCGroups.Frattini.Subgroup.IsMaximalWithProperty

Documentation

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.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
open scoped Topology Pointwise
namespace ProCGroups.Frattini
universe u
section MaximalSubgroups
variable {G : Type u} [Group G]

Lean source · statement

def Subgroup.IsMaximalWithProperty (P : Subgroup G → Prop) (H : Subgroup G) : Prop

theorem

property

L41 ↗

ProCGroups.Frattini.Subgroup.IsMaximalWithProperty.property

Documentation

A maximal subgroup with property P satisfies the property P.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
open scoped Topology Pointwise
namespace ProCGroups.Frattini
universe u
section MaximalSubgroups
variable {G : Type u} [Group G]
namespace Subgroup.IsMaximalWithProperty
variable {P : Subgroup G → Prop} {H K : Subgroup G}

Lean source · statement

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

theorem

ne_top

L46 ↗

ProCGroups.Frattini.Subgroup.IsMaximalWithProperty.ne_top

Documentation

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

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
open scoped Topology Pointwise
namespace ProCGroups.Frattini
universe u
section MaximalSubgroups
variable {G : Type u} [Group G]
namespace Subgroup.IsMaximalWithProperty
variable {P : Subgroup G → Prop} {H K : Subgroup G}

Lean source · statement

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

theorem

eq_of_le

L51 ↗

ProCGroups.Frattini.Subgroup.IsMaximalWithProperty.eq_of_le

Documentation

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

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
open scoped Topology Pointwise
namespace ProCGroups.Frattini
universe u
section MaximalSubgroups
variable {G : Type u} [Group G]
namespace Subgroup.IsMaximalWithProperty
variable {P : Subgroup G → Prop} {H K : Subgroup G}

Lean source · statement

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

theorem

isOpen

L63 ↗

ProCGroups.Frattini.Subgroup.IsMaximalOpen.isOpen

Documentation

A subgroup that is maximal among open subgroups is open.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
open scoped Topology Pointwise
namespace ProCGroups.Frattini
universe u
section MaximalSubgroups
variable {G : Type u} [Group G]
namespace Subgroup.IsMaximalOpen
variable [TopologicalSpace G] {H K : Subgroup G}

Lean source · full declaration

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

theorem

ne_top

L69 ↗

ProCGroups.Frattini.Subgroup.IsMaximalOpen.ne_top

Documentation

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

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
open scoped Topology Pointwise
namespace ProCGroups.Frattini
universe u
section MaximalSubgroups
variable {G : Type u} [Group G]
namespace Subgroup.IsMaximalOpen
variable [TopologicalSpace G] {H K : Subgroup G}

Lean source · full declaration

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

theorem

eq_of_le

L75 ↗

ProCGroups.Frattini.Subgroup.IsMaximalOpen.eq_of_le

Documentation

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

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
open scoped Topology Pointwise
namespace ProCGroups.Frattini
universe u
section MaximalSubgroups
variable {G : Type u} [Group G]
namespace Subgroup.IsMaximalOpen
variable [TopologicalSpace G] {H K : Subgroup G}

Lean source · full declaration

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 :=
  hH.2.2 K hHK hKopen hKne

theorem

isClosed

L89 ↗

ProCGroups.Frattini.Subgroup.IsMaximalClosed.isClosed

Documentation

A maximal closed subgroup is closed.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
open scoped Topology Pointwise
namespace ProCGroups.Frattini
universe u
section MaximalSubgroups
variable {G : Type u} [Group G]
namespace Subgroup.IsMaximalClosed
variable [TopologicalSpace G] {H K : Subgroup G}

Lean source · full declaration

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

theorem

ne_top

L95 ↗

ProCGroups.Frattini.Subgroup.IsMaximalClosed.ne_top

Documentation

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

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
open scoped Topology Pointwise
namespace ProCGroups.Frattini
universe u
section MaximalSubgroups
variable {G : Type u} [Group G]
namespace Subgroup.IsMaximalClosed
variable [TopologicalSpace G] {H K : Subgroup G}

Lean source · full declaration

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

theorem

eq_of_le

L101 ↗

ProCGroups.Frattini.Subgroup.IsMaximalClosed.eq_of_le

Documentation

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

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
open scoped Topology Pointwise
namespace ProCGroups.Frattini
universe u
section MaximalSubgroups
variable {G : Type u} [Group G]
namespace Subgroup.IsMaximalClosed
variable [TopologicalSpace G] {H K : Subgroup G}

Lean source · full declaration

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 :=
  hH.2.2 K hHK hKclosed hKne

def

frattiniWithin

L117 ↗

ProCGroups.Frattini.frattiniWithin

Documentation

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

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
open scoped Topology Pointwise
namespace ProCGroups.Frattini
universe u
section FrattiniWithin
variable {G : Type u} [Group G]

Lean source · statement

def frattiniWithin (H : Subgroup G) : Subgroup G

theorem

frattiniWithin_le

L121 ↗

ProCGroups.Frattini.frattiniWithin_le

Documentation

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

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
open scoped Topology Pointwise
namespace ProCGroups.Frattini
universe u
section FrattiniWithin
variable {G : Type u} [Group G]

Lean source · statement

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

theorem

mem_frattiniWithin

L131 ↗

ProCGroups.Frattini.mem_frattiniWithin

Documentation

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

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
open scoped Topology Pointwise
namespace ProCGroups.Frattini
universe u
section FrattiniWithin
variable {G : Type u} [Group G]

Lean source · statement

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

Module documentation

Pro C Groups / Frattini

Declarations