The transversal word of a subgroup

Let U be a subgroup of a group G and let t : G ⧸ U → G be a transversal, that is, a map picking a representative of each coset. The transversal word

ℓᵗ_u(γ) = (t u)⁻¹ * γ * t (γ⁻¹ • u)

measures the failure of γ * t (γ⁻¹ • u) to be the chosen representative t u of its coset. It lies in U whenever t really is a transversal, and it is a 1-cocycle for the action of G on G ⧸ U:

ℓᵗ_u(γ) * ℓᵗ_{γ⁻¹ • u}(η) = ℓᵗ_u(γ * η).

This file records the word calculus through TauCeti.lWord and the three identities that make it useful: TauCeti.lWord_mem, TauCeti.lWord_mul_lWord, and TauCeti.transversal_mul_lWord, the last of which is the rewriting rule t u * ℓᵗ_u(γ) = γ * t (γ⁻¹ • u) that turns a U-cocycle relation into a G-cocycle relation. It also records how the word changes when the transversal does (TauCeti.transversalDiff and TauCeti.transversalDiff_mul_lWord), builds the transversal adapted to a map w : G → U that is equivariant for left multiplication by U (TauCeti.factorizationTransversal), on which w reads off the transversal word, and computes the word for a subgroup of index two at the two-element transversal {1, s} (Subgroup.indexTwoTransversal): on an element γ of the subgroup it is γ at the trivial coset and s⁻¹ * γ * s at the other, and on an element outside it is γ * s and s⁻¹ * γ respectively. For a normal subgroup, the word of an element of the subgroup at any coset is its conjugate by the representative (TauCeti.lWord_of_mem_of_normal). Continuity of γ ↦ ℓᵗ_u(γ) for an open subgroup of a topological group is TauCeti.continuous_lWord, in TauCeti/Topology/Algebra/Group/TransversalWord.lean; nothing in this file needs a topology.

In the word calculus, the transversal is a variable, and only lWord_mem and transversalDiff_mem ask that t actually represent each coset.

Implementation notes

The word calculus takes a map t : G ⧸ U → G because its consuming formulas index by G ⧸ U. The map satisfies ↑(t u) = u when membership in U is needed; Quotient.out is the canonical example. A Mathlib Subgroup.LeftTransversal yields the map Subgroup.leftTransversalRep via Subgroup.IsComplement.leftQuotientEquiv; Subgroup.leftTransversalRep_mk gives its representative property.

The transversal word supplies the subgroup-valued arguments in the cochain formulas for corestriction; its cocycle and change-of-transversal identities support their algebraic proofs.

def TauCeti.lWord {G : Type u_1} [Group G] (U : Subgroup G) (t : G ⧸ U → G) (u : G ⧸ U) (γ : G) : G

The transversal word ℓᵗ_u(γ) = (t u)⁻¹ * γ * t (γ⁻¹ • u) of a subgroup U ≤ G, a map t : G ⧸ U → G, a coset u and a group element γ. It lies in U as soon as t is a transversal (TauCeti.lWord_mem).

Equations

• TauCeti.lWord U t u γ = (t u)⁻¹ * γ * t (γ⁻¹ • u)

theorem TauCeti.lWord_def {G : Type u_1} [Group G] (U : Subgroup G) (t : G ⧸ U → G) (u : G ⧸ U) (γ : G) : lWord U t u γ = (t u)⁻¹ * γ * t (γ⁻¹ • u)

@[simp]

theorem TauCeti.lWord_one {G : Type u_1} [Group G] (U : Subgroup G) (t : G ⧸ U → G) (u : G ⧸ U) : lWord U t u 1 = 1

theorem TauCeti.transversal_mul_lWord {G : Type u_1} [Group G] (U : Subgroup G) (t : G ⧸ U → G) (u : G ⧸ U) (γ : G) : t u * lWord U t u γ = γ * t (γ⁻¹ • u)

The rewriting rule t u * ℓᵗ_u(γ) = γ * t (γ⁻¹ • u). It is what turns the cocycle relation of a function on U into the cocycle relation of the corresponding sum over G ⧸ U.

theorem TauCeti.transversal_smul_mul_lWord {G : Type u_1} [Group G] (U : Subgroup G) (t : G ⧸ U → G) (u : G ⧸ U) (γ : G) : t (γ • u) * lWord U t (γ • u) γ = γ * t u

The rewriting rule at the translated coset: t (γ • u) * ℓᵗ_{γ • u}(γ) = γ * t u.

theorem TauCeti.lWord_mul_lWord {G : Type u_1} [Group G] (U : Subgroup G) (t : G ⧸ U → G) (u : G ⧸ U) (γ η : G) : lWord U t u γ * lWord U t (γ⁻¹ • u) η = lWord U t u (γ * η)

The transversal 1-cocycle law ℓᵗ_u(γ) * ℓᵗ_{γ⁻¹ • u}(η) = ℓᵗ_u(γ * η). It holds for an arbitrary map t, with no normality, no finite index and no transversal condition.

theorem TauCeti.lWord_inv {G : Type u_1} [Group G] (U : Subgroup G) (t : G ⧸ U → G) (u : G ⧸ U) (γ : G) : lWord U t u γ⁻¹ = (lWord U t (γ • u) γ)⁻¹

The transversal word of γ⁻¹ is the inverse of the transversal word of γ, at the translated coset. This is the cocycle law at η = γ⁻¹.

theorem TauCeti.lWord_mk_one_of_mem {G : Type u_1} [Group G] (U : Subgroup G) (t : G ⧸ U → G) {γ : G} (hγ : γ ∈ U) : lWord U t (↑1) γ = (t ↑1)⁻¹ * γ * t ↑1

At the coset of the identity, the transversal word of an element of U is that element conjugated by the chosen representative of that coset: no hypothesis on t is needed, and for a transversal normalized by t 1 = 1 the word is the element itself. This is the reduction that identifies the restriction of a cochain to U inside a corestriction sum.

theorem TauCeti.lWord_of_mem_of_normal {G : Type u_1} [Group G] (U : Subgroup G) (t : G ⧸ U → G) [U.Normal] {γ : G} (hγ : γ ∈ U) (u : G ⧸ U) : lWord U t u γ = (t u)⁻¹ * γ * t u

For a normal subgroup U, the transversal word of an element of U at any coset is that element conjugated by the chosen representative of the coset: an element of U fixes every coset, so no hypothesis on t is needed. This is the reduction that turns the restriction of a corestriction sum into a sum of conjugates.

theorem TauCeti.lWord_mem {G : Type u_1} [Group G] (U : Subgroup G) (t : G ⧸ U → G) (ht : ∀ (u : G ⧸ U), ↑(t u) = u) (u : G ⧸ U) (γ : G) : lWord U t u γ ∈ U

The transversal word of a genuine transversal lies in U.

def TauCeti.transversalDiff {G : Type u_1} [Group G] (U : Subgroup G) (t t' : G ⧸ U → G) (u : G ⧸ U) : G

The difference of two transversals, d^{t,t'}_u = (t u)⁻¹ * t' u. It lies in U when both are transversals, and it intertwines the two transversal words in the twisted form d_u * ℓᵗ'_u(γ) = ℓᵗ_u(γ) * d_{γ⁻¹ • u} (TauCeti.transversalDiff_mul_lWord).

Equations

• TauCeti.transversalDiff U t t' u = (t u)⁻¹ * t' u

theorem TauCeti.transversalDiff_def {G : Type u_1} [Group G] (U : Subgroup G) (t t' : G ⧸ U → G) (u : G ⧸ U) : transversalDiff U t t' u = (t u)⁻¹ * t' u

@[simp]

theorem TauCeti.transversalDiff_self {G : Type u_1} [Group G] (U : Subgroup G) (t : G ⧸ U → G) (u : G ⧸ U) : transversalDiff U t t u = 1

@[simp]

theorem TauCeti.transversal_mul_transversalDiff {G : Type u_1} [Group G] (U : Subgroup G) (t t' : G ⧸ U → G) (u : G ⧸ U) : t u * transversalDiff U t t' u = t' u

The chosen representative of the second transversal, recovered from the first.

theorem TauCeti.transversalDiff_mem {G : Type u_1} [Group G] (U : Subgroup G) (t t' : G ⧸ U → G) (ht : ∀ (u : G ⧸ U), ↑(t u) = u) (ht' : ∀ (u : G ⧸ U), ↑(t' u) = u) (u : G ⧸ U) : transversalDiff U t t' u ∈ U

The difference of two genuine transversals lies in U: if both t and t' pick representatives of every coset, then (t u)⁻¹ * t' u is a member of U for every u.

theorem TauCeti.transversalDiff_mul_lWord {G : Type u_1} [Group G] (U : Subgroup G) (t t' : G ⧸ U → G) (u : G ⧸ U) (γ : G) : transversalDiff U t t' u * lWord U t' u γ = lWord U t u γ * transversalDiff U t t' (γ⁻¹ • u)

Change of transversal. The two transversal words differ by the transversal difference, in the twisted form the change-of-transversal computations use. No hypothesis on t or t' is needed for the identity itself.

The transversal adapted to a right-coset factorization

noncomputable def TauCeti.factorizationTransversal {G : Type u_1} [Group G] {U : Subgroup G} (w : G → ↥U) (x : G ⧸ U) : G

The transversal of G ⧸ U adapted to a map w : G → U that is U-equivariant for left multiplication, such as the U-component of a factorization G = U · R over the right cosets: the representative r * w r⁻¹ of the coset of r = x.out. When w is equivariant it sends the inverse of every chosen representative to 1 (TauCeti.apply_inv_factorizationTransversal), and it sends (t x)⁻¹ * γ to the transversal word ℓᵗ_x(γ) (TauCeti.apply_inv_factorizationTransversal_mul).

Equations

• TauCeti.factorizationTransversal w x = Quotient.out x * ↑(w (Quotient.out x)⁻¹)

theorem TauCeti.factorizationTransversal_def {G : Type u_1} [Group G] {U : Subgroup G} (w : G → ↥U) (x : G ⧸ U) : factorizationTransversal w x = Quotient.out x * ↑(w (Quotient.out x)⁻¹)

@[simp]

theorem TauCeti.factorizationTransversal_mk {G : Type u_1} [Group G] {U : Subgroup G} (w : G → ↥U) (x : G ⧸ U) : ↑(factorizationTransversal w x) = x

The adapted transversal picks a representative of every coset.

theorem TauCeti.apply_inv_factorizationTransversal {G : Type u_1} [Group G] {U : Subgroup G} (w : G → ↥U) (hwmul : ∀ (u : ↥U) (g : G), w (↑u * g) = u * w g) (x : G ⧸ U) : w (factorizationTransversal w x)⁻¹ = 1

An equivariant w sends the inverse of every representative of the adapted transversal to 1.

theorem TauCeti.apply_inv_factorizationTransversal_mul {G : Type u_1} [Group G] {U : Subgroup G} (w : G → ↥U) (hwmul : ∀ (u : ↥U) (g : G), w (↑u * g) = u * w g) (x : G ⧸ U) (γ : G) : w ((factorizationTransversal w x)⁻¹ * γ) = ⟨lWord U (factorizationTransversal w) x γ, ⋯⟩

An equivariant w sends (t x)⁻¹ * γ to the transversal word ℓᵗ_x(γ) of the adapted transversal t.

Representatives of a bundled left transversal

noncomputable def Subgroup.leftTransversalRep {G : Type u_1} [Group G] (U : Subgroup G) (s : U.LeftTransversal) : G ⧸ U → G

Representatives supplied by Mathlib's bundled left transversal.

Equations

• U.leftTransversalRep s x = ↑(⋯.leftQuotientEquiv x)

theorem Subgroup.leftTransversalRep_apply {G : Type u_1} [Group G] (U : Subgroup G) (s : U.LeftTransversal) (x : G ⧸ U) : U.leftTransversalRep s x = ↑(⋯.leftQuotientEquiv x)

The representative of a coset from a bundled left transversal.

theorem Subgroup.leftTransversalRep_mem {G : Type u_1} [Group G] (U : Subgroup G) (s : U.LeftTransversal) (x : G ⧸ U) : U.leftTransversalRep s x ∈ ↑s

The chosen representative belongs to the left transversal.

@[simp]

theorem Subgroup.leftTransversalRep_mk {G : Type u_1} [Group G] (U : Subgroup G) (s : U.LeftTransversal) (x : G ⧸ U) : ↑(U.leftTransversalRep s x) = x

The chosen representative maps back to its coset.

@[simp]

theorem Subgroup.leftTransversalRep_range {G : Type u_1} [Group G] (U : Subgroup G) (t : G ⧸ U → G) (ht : ∀ (u : G ⧸ U), ↑(t u) = u) : U.leftTransversalRep ⟨Set.range t, ⋯⟩ = t

Packaging a section as a left transversal recovers the original representative map.

The two-element transversal of a subgroup of index two

noncomputable def Subgroup.indexTwoTransversal {G : Type u_1} [Group G] (U : Subgroup G) (s : G) : G ⧸ U → G

The map G ⧸ U → G sending the coset of 1 to 1 and every other coset to s. For a subgroup U of index two and s ∉ U it is the transversal {1, s} (Subgroup.indexTwoTransversal_mk), the one on which the index-two corestriction formulas are computed.

Equations

• U.indexTwoTransversal s u = if u = ↑1 then 1 else s

@[simp]

theorem Subgroup.indexTwoTransversal_mk_one {G : Type u_1} [Group G] {U : Subgroup G} (s : G) : U.indexTwoTransversal s ↑1 = 1

The two-element transversal sends the trivial coset to 1.

@[simp]

theorem Subgroup.indexTwoTransversal_of_ne {G : Type u_1} [Group G] {U : Subgroup G} (s : G) {u : G ⧸ U} (hu : u ≠ ↑1) : U.indexTwoTransversal s u = s

The two-element transversal sends every nontrivial coset to s.

@[simp]

theorem Subgroup.indexTwoTransversal_mk {G : Type u_1} [Group G] {U : Subgroup G} (hU : U.index = 2) {s : G} (hs : s ∉ U) (u : G ⧸ U) : ↑(U.indexTwoTransversal s u) = u

For a subgroup of index two and s ∉ U, U.indexTwoTransversal s is a transversal.

@[simp]

theorem TauCeti.lWord_indexTwoTransversal_mk_one_of_mem {G : Type u_1} [Group G] {U : Subgroup G} (s : G) {γ : G} (hγ : γ ∈ U) : lWord U (U.indexTwoTransversal s) (↑1) γ = γ

At the trivial coset, the transversal word of U.indexTwoTransversal s on an element of U is that element.

@[simp]

theorem TauCeti.lWord_indexTwoTransversal_mk_of_mem {G : Type u_1} [Group G] {U : Subgroup G} (hU : U.index = 2) {s : G} (hs : s ∉ U) {γ : G} (hγ : γ ∈ U) : lWord U (U.indexTwoTransversal s) (↑s) γ = s⁻¹ * γ * s

At the coset of s, the transversal word of U.indexTwoTransversal s on an element γ of a subgroup U of index two is the conjugate s⁻¹ * γ * s.

@[simp]

theorem TauCeti.lWord_indexTwoTransversal_mk_one_of_notMem {G : Type u_1} [Group G] {U : Subgroup G} (hU : U.index = 2) {s : G} (hs : s ∉ U) {γ : G} (hγ : γ ∉ U) : lWord U (U.indexTwoTransversal s) (↑1) γ = γ * s

At the trivial coset, the transversal word of U.indexTwoTransversal s on an element γ outside a subgroup U of index two is γ * s.

@[simp]

theorem TauCeti.lWord_indexTwoTransversal_mk_of_notMem {G : Type u_1} [Group G] {U : Subgroup G} (hU : U.index = 2) {s : G} (hs : s ∉ U) {γ : G} (hγ : γ ∉ U) : lWord U (U.indexTwoTransversal s) (↑s) γ = s⁻¹ * γ

At the coset of s, the transversal word of U.indexTwoTransversal s on an element γ outside a subgroup U of index two is s⁻¹ * γ.