Module

SubgroupChains.lean

Nyll.ProCGroups.LocalWeight.SubgroupChains

8 declarations indexed from sourceView source ↗

Module documentation

Intersections of subgroup chains

This file packages linearly ordered families of subgroups, defines their carrier union and intersection, and gives membership and trivial-intersection criteria used in transfinite closed-normal series arguments.

Imports1

Nyll.ProCGroups.ProC.OpenNormalSubgroups.CountableChains

Imported by2

abbrev

SubgroupChain

L28 ↗

ProCGroups.LocalWeight.SubgroupChain

Documentation

A family of subgroups forming a chain indexed for transfinite local-weight statements.

Source context 5 commands

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

namespace ProCGroups.LocalWeight
universe u v
section Chains
variable {ι : Type v}
variable {G : Type u} [Group G]

Lean source · statement

abbrev SubgroupChain (ι : Type v) (G : Type u) [Group G]

def

subgroupChainCarrier

L31 ↗

ProCGroups.LocalWeight.subgroupChainCarrier

Documentation

The set-theoretic union of the members of a subgroup chain.

Source context 5 commands

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

namespace ProCGroups.LocalWeight
universe u v
section Chains
variable {ι : Type v}
variable {G : Type u} [Group G]

Lean source · statement

def subgroupChainCarrier (c : SubgroupChain ι G) : Set G

def

subgroupChainInf

L35 ↗

ProCGroups.LocalWeight.subgroupChainInf

Documentation

The infimum of all members of a subgroup chain.

Source context 5 commands

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

namespace ProCGroups.LocalWeight
universe u v
section Chains
variable {ι : Type v}
variable {G : Type u} [Group G]

Lean source · statement

def subgroupChainInf (c : SubgroupChain ι G) : Subgroup G

theorem

mem_subgroupChainCarrier_iff

L42 ↗

ProCGroups.LocalWeight.mem_subgroupChainCarrier_iff

Documentation

Membership in the carrier of a subgroup chain is equivalent to the displayed coordinate condition.

Source context 5 commands

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

namespace ProCGroups.LocalWeight
universe u v
section Chains
variable {ι : Type v}
variable {G : Type u} [Group G]

Lean source · statement

theorem mem_subgroupChainCarrier_iff {c : SubgroupChain ι G} {g : G} :
    g ∈ subgroupChainCarrier c ↔ ∃ i, g ∈ c i

theorem

subgroupChainInf_le

L47 ↗

ProCGroups.LocalWeight.subgroupChainInf_le

Documentation

The infimum of a subgroup chain is contained in each subgroup in the chain.

Source context 5 commands

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

namespace ProCGroups.LocalWeight
universe u v
section Chains
variable {ι : Type v}
variable {G : Type u} [Group G]

Lean source · statement

theorem subgroupChainInf_le (c : SubgroupChain ι G) (i : ι) :
    subgroupChainInf c ≤ c i

theorem

mem_subgroupChainInf_iff

L55 ↗

ProCGroups.LocalWeight.mem_subgroupChainInf_iff

Documentation

Membership in the infimum of a subgroup chain is equivalent to the displayed coordinate condition.

Source context 5 commands

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

namespace ProCGroups.LocalWeight
universe u v
section Chains
variable {ι : Type v}
variable {G : Type u} [Group G]

Lean source · statement

theorem mem_subgroupChainInf_iff {c : SubgroupChain ι G} {g : G} :
    g ∈ subgroupChainInf c ↔ ∀ i, g ∈ c i

theorem

subgroupChainInf_eq_bot_iff

L64 ↗

ProCGroups.LocalWeight.subgroupChainInf_eq_bot_iff

Documentation

The subgroup-chain infimum is trivial exactly when every nontrivial element is excluded at some stage.

Source context 5 commands

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

namespace ProCGroups.LocalWeight
universe u v
section Chains
variable {ι : Type v}
variable {G : Type u} [Group G]

Lean source · statement

theorem subgroupChainInf_eq_bot_iff {c : SubgroupChain ι G} :
    subgroupChainInf c = ⊥ ↔ ∀ g : G, (∀ i, g ∈ c i) → g = 1

theorem

subgroupChainInf_eq_bot_iff_forall_ne_one

L91 ↗

ProCGroups.LocalWeight.subgroupChainInf_eq_bot_iff_forall_ne_one

Documentation

The infimum of a subgroup chain is bottom exactly when every nontrivial element is excluded at some stage.

Source context 5 commands

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

namespace ProCGroups.LocalWeight
universe u v
section Chains
variable {ι : Type v}
variable {G : Type u} [Group G]

Lean source · statement

theorem subgroupChainInf_eq_bot_iff_forall_ne_one {c : SubgroupChain ι G} :
    subgroupChainInf c = ⊥ ↔ ∀ g : G, g ≠ 1 → ∃ i, g ∉ c i

Module documentation

Intersections of subgroup chains

Declarations