Module

QuotientTower.lean

Nyll.GaloisCohomology.GroupTheory.QuotientTower

2 declarations indexed from sourceView source ↗

Module documentation

Quotients in subgroup towers

This file supplies the type-level equivalences between the quotient of a subgroup and the corresponding quotient after viewing that subgroup inside a larger group. They complement Mathlib's natural-number relative-index laws when cardinal-valued indices must also cover infinite towers.

Imports1

Mathlib.GroupTheory.Index

Imported by3

def

quotientSubgroupOfEquiv

L30 ↗

Subgroup.quotientSubgroupOfEquiv

Documentation

Viewing H inside K does not change the quotient of H by the subgroup induced by M.

Source context 4 commands

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

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

Lean source · full declaration

def quotientSubgroupOfEquiv {H K M : Subgroup G} (hHK : H ≤ K) :
    (↑(H.subgroupOf K) ⧸ (M.subgroupOf K).subgroupOf (H.subgroupOf K)) ≃
      (↑H ⧸ M.subgroupOf H) where
  toFun := Quotient.map' (subgroupOfEquivOfLe hHK) (by
    intro x y hxy
    rw [QuotientGroup.leftRel_apply] at hxy ⊢
    exact hxy)
  invFun := Quotient.map' (subgroupOfEquivOfLe hHK).symm (by
    intro x y hxy
    rw [QuotientGroup.leftRel_apply] at hxy ⊢
    exact hxy)
  left_inv q := by
    refine Quotient.inductionOn' q ?_
    intro x
    change Quotient.map' _ _ (Quotient.map' _ _ (Quotient.mk'' x)) = Quotient.mk'' x
    simpa only [Quotient.map'_mk''] using
      congrArg Quotient.mk'' ((subgroupOfEquivOfLe hHK).symm_apply_apply x)
  right_inv q := by
    refine Quotient.inductionOn' q ?_
    intro x
    change Quotient.map' _ _ (Quotient.map' _ _ (Quotient.mk'' x)) = Quotient.mk'' x
    simpa only [Quotient.map'_mk''] using
      congrArg Quotient.mk'' ((subgroupOfEquivOfLe hHK).apply_symm_apply x)

def

quotientTowerEquiv

L56 ↗

Subgroup.quotientTowerEquiv