Module

Quotient.lean

Nyll.GaloisCohomology.GroupTheory.Quotient

6 declarations indexed from sourceView source ↗

Module documentation

Quotients represented by a supporting subgroup

If two subgroups generate a commutative group, every class modulo the second subgroup has a representative in the first. This is the precise group-theoretic comparison used when a sufficiently large group of supported ideles represents the full idele class group.

Imports4

Mathlib.Algebra.Group.Equiv.Defs
Mathlib.GroupTheory.Abelianization.Defs
Mathlib.Logic.Equiv.Defs
Mathlib.GroupTheory.QuotientGroup.Basic

Imported by3

def

subgroupQuotientEquivQuotientOfSupEqTop

L27 ↗

Documentation

If S and P generate G, inclusion of S identifies S / (S ∩ P) with G / P.

Source context 2 commands

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

noncomputable section
variable {G : Type*} [CommGroup G]

Lean source · statement

def subgroupQuotientEquivQuotientOfSupEqTop
    (S P : Subgroup G)
    (hSP : S ⊔ P = ⊤) :
    S ⧸ P.subgroupOf S ≃* G ⧸ P

theorem

subgroupQuotientEquivQuotientOfSupEqTop_mk

L49 ↗

Source context 2 commands

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

noncomputable section
variable {G : Type*} [CommGroup G]

Lean source · statement

theorem subgroupQuotientEquivQuotientOfSupEqTop_mk
    (S P : Subgroup G)
    (hSP : S ⊔ P = ⊤)
    (s : S) :
    subgroupQuotientEquivQuotientOfSupEqTop S P hSP
        (QuotientGroup.mk' (P.subgroupOf S) s) =
      QuotientGroup.mk' P (s : G)

theorem

comap_map_abelianization_eq_sup_commutator

L66 ↗

Subgroup.comap_map_abelianization_eq_sup_commutator

Documentation

The inverse image of the image of a subgroup in the abelianization is the subgroup generated by it and the commutator subgroup.

Source context 5 commands

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

noncomputable section
variable {G : Type*} [CommGroup G]
namespace Subgroup
universe u
variable {Gamma : Type u} [Group Gamma]

Lean source · statement

theorem comap_map_abelianization_eq_sup_commutator (H : Subgroup Gamma) :
    (H.map (Abelianization.of : Gamma →* Abelianization Gamma)).comap
        (Abelianization.of : Gamma →* Abelianization Gamma) =
      H ⊔ _root_.commutator Gamma

instance

normal_sup_commutator

L74 ↗

Subgroup.normal_sup_commutator

Documentation

Adjoining the commutator subgroup to any subgroup produces a normal subgroup.

Source context 5 commands

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

noncomputable section
variable {G : Type*} [CommGroup G]
namespace Subgroup
universe u
variable {Gamma : Type u} [Group Gamma]

Lean source · statement

instance normal_sup_commutator (H : Subgroup Gamma) :
    (H ⊔ _root_.commutator Gamma).Normal

def

quotientSupCommutatorEquivMapAbelianization

L81 ↗

Subgroup.quotientSupCommutatorEquivMapAbelianization

Documentation

Quotienting a group by a subgroup together with the commutator subgroup agrees with quotienting its abelianization by the image of that subgroup.

Source context 5 commands

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

noncomputable section
variable {G : Type*} [CommGroup G]
namespace Subgroup
universe u
variable {Gamma : Type u} [Group Gamma]

Lean source · statement

def quotientSupCommutatorEquivMapAbelianization
    (H : Subgroup Gamma) :
    Gamma ⧸ (H ⊔ _root_.commutator Gamma) ≃*
      Abelianization Gamma ⧸
        H.map (Abelianization.of : Gamma →* Abelianization Gamma)

theorem

quotientSupCommutatorEquivMapAbelianization_mk

L103 ↗

Subgroup.quotientSupCommutatorEquivMapAbelianization_mk

Source context 5 commands

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

noncomputable section
variable {G : Type*} [CommGroup G]
namespace Subgroup
universe u
variable {Gamma : Type u} [Group Gamma]

Lean source · statement

theorem quotientSupCommutatorEquivMapAbelianization_mk
    (H : Subgroup Gamma) (g : Gamma) :
    H.quotientSupCommutatorEquivMapAbelianization
        (QuotientGroup.mk' (H ⊔ _root_.commutator Gamma) g) =
      QuotientGroup.mk'
        (H.map (Abelianization.of : Gamma →* Abelianization Gamma))
        (Abelianization.of g)

Module documentation

Quotients represented by a supporting subgroup

Declarations

subgroupQuotientEquivQuotientOfSupEqTop

subgroupQuotientEquivQuotientOfSupEqTop_mk

comap_map_abelianization_eq_sup_commutator

normal_sup_commutator

quotientSupCommutatorEquivMapAbelianization

quotientSupCommutatorEquivMapAbelianization_mk