Coset.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Congruences of coset actions

The full congruence lattice of the left action on a finite group's cosets is the subgroup interval above the stabilizer. No normality assumption is needed.

def OAI.FiniteCongruence.cosetAlgebra line 21
Source documentation
One unary operation for each element of G; no omitted operations.
```
def cosetAlgebra : Algebra (G ⧸ H) where
…
```
Mentions: OAI.FiniteCongruence.Algebra
lemma OAI.FiniteCongruence.compatible_iff_invariant line 26
abbrev OAI.FiniteCongruence.base line 38
def OAI.FiniteCongruence.subgroupOf line 41
Source documentation
The subgroup determined by the class of the identity coset.
```
def subgroupOf (r : Congruence (cosetAlgebra H)) : Subgroup G where
…
```
Mentions: OAI.FiniteCongruence.Congruence, OAI.FiniteCongruence.cosetAlgebra
lemma OAI.FiniteCongruence.le_subgroupOf line 55
def OAI.FiniteCongruence.quotientMap line 63
Source documentation
The canonical quotient-set map exists without a normality assumption.
```
def quotientMap (K : Subgroup G) (h : H ≤ K) : G ⧸ H → G ⧸ K :=
…
```
lemma OAI.FiniteCongruence.quotientMap_mk line 68
lemma OAI.FiniteCongruence.quotientMap_smul line 72
def OAI.FiniteCongruence.congruenceOf line 78
Source documentation
Pullback of equality on G/K, hence an actual equivalence relation on G/H.
```
def congruenceOf (K : Subgroup G) (h : H ≤ K) : Congruence (cosetAlgebra H) :=
…
```
Mentions: OAI.FiniteCongruence.Congruence, OAI.FiniteCongruence.cosetAlgebra
lemma OAI.FiniteCongruence.congruenceOf_mk line 85
lemma OAI.FiniteCongruence.invariant_mk_iff line 90
lemma OAI.FiniteCongruence.subgroupOf_congruenceOf line 103
lemma OAI.FiniteCongruence.congruenceOf_subgroupOf line 109
def OAI.FiniteCongruence.coset_action_correspondence line 120
Source documentation
The full congruence lattice of the coset algebra is order-isomorphic to the subgroup interval.
```
def coset_action_correspondence :
    Congruence (cosetAlgebra H) ≃o Set.Icc H (⊤ : Subgroup G) where
…
```
Mentions: OAI.FiniteCongruence.Congruence, OAI.FiniteCongruence.cosetAlgebra
theorem OAI.FiniteCongruence.coset_action_correspondence_exists line 141
Source documentation
The finite coset algebra realizes the full subgroup interval.
```
theorem coset_action_correspondence_exists :
    Nonempty (Congruence (cosetAlgebra H) ≃o Set.Icc H (⊤ : Subgroup G)) :=
…
```
Mentions: OAI.FiniteCongruence.Congruence, OAI.FiniteCongruence.cosetAlgebra