Group extensions built from a factor set

A factor set of a group G with values in a G-module M (written multiplicatively: M is a commutative group carrying a MulDistribMulAction of G) is a normalized multiplicative 2-cocycle α : G × G → M. This file builds the group extension 1 → M → E_α → G → 1 it determines: the underlying set is M × G, and the multiplication is the one of a semidirect product twisted by α,

⟨a, g⟩ * ⟨b, h⟩ = ⟨a * g • b * α (g, h), g * h⟩.

The cocycle identity is exactly associativity of this product, and the normalization is exactly what makes ⟨1, 1⟩ its identity, so both are carried as fields of FactorSet rather than as hypotheses of the results below.

Two facts identify α as the factor set of the extension it builds. The set-theoretic section g ↦ ⟨1, g⟩ fails to be a homomorphism by exactly α (TauCeti.FactorSet.canonicalSection_mul), and conjugating the copy of M inside the extension is the given action of G on M (TauCeti.FactorSet.mul_inl). When G acts trivially the latter says the copy of M is central, so the extension is a central extension; that is the case M = kˣ in which a projective representation of G with factor set α becomes a linear representation of E_α.

A factor set is a multiplicative 2-cocycle by definition, so no conversion is needed to reach group cohomology: groupCohomology.cocyclesOfIsMulCocycle₂ α.isMulCocycle₂ reads α as a 2-cocycle for the ℤ-linear representation of G on Additive M, the input to groupCohomology.H2.

Main definitions

• TauCeti.FactorSet G M: a normalized multiplicative 2-cocycle G × G → M, bundled with its cocycle and normalization proofs.
• TauCeti.FactorSet.Extension: the twisted product M × G carrying the group structure above.
• TauCeti.FactorSet.groupExtension: that group as a GroupExtension M _ G, i.e. together with the inclusion of M, the projection to G, and the exactness proofs.
• TauCeti.FactorSet.canonicalSection: the section g ↦ ⟨1, g⟩ of the projection.
• TauCeti.FactorSet.rescaleEquiv: the equivalence of extensions obtained by rescaling that section.
• TauCeti.FactorSet.trivial: the factor set that is constantly 1.
• TauCeti.FactorSet.map: the pushforward of a factor set along a G-equivariant homomorphism of coefficient modules.

Main results

• TauCeti.FactorSet.canonicalSection_mul: σ g * σ h = inl (α (g, h)) * σ (g * h), so α measures the failure of the canonical section to be a homomorphism, and TauCeti.FactorSet.inl_mul_canonicalSection: every element of the extension is its M-component times the section at its G-component, so the two together determine a homomorphism out of the extension.
• TauCeti.FactorSet.mul_inl: conjugation moves the copy of M by the action of the image in G.
• TauCeti.FactorSet.inl_range_le_center: when G acts trivially the extension is central.
• TauCeti.FactorSet.nonempty_groupExtensionEquiv: cohomologous factor sets build equivalent extensions.
• TauCeti.FactorSet.trivialMulEquiv: the extension attached to the trivial factor set is the semidirect product, and TauCeti.FactorSet.trivialSplitting splits it.

References

G. Karpilovsky, Projective Representations of Finite Groups, Marcel Dekker (1985), Ch. 1, and I. M. Isaacs, Character Theory of Finite Groups, AMS Chelsea (1976), Ch. 11.

structure TauCeti.FactorSet (G : Type u) (M : Type v) [Group G] [CommGroup M] [MulDistribMulAction G M] : Type (max u v)

A factor set of G with values in the G-module M: a multiplicative 2-cocycle α : G × G → M normalized by α (1, 1) = 1. The cocycle identity is Mathlib's groupCohomology.IsMulCocycle₂; it gives associativity of TauCeti.FactorSet.Extension, while the normalization makes ⟨1, 1⟩ the identity there.

• toFun : G × G → M

  The underlying function of a factor set.

• isMulCocycle₂' : groupCohomology.IsMulCocycle₂ self.toFun

  A factor set satisfies the multiplicative 2-cocycle identity.

• map_one_one' : self.toFun (1, 1) = 1

  A factor set is normalized. Together with the cocycle identity this forces α (1, g) = α (g, 1) = 1 for every g.

@[instance_reducible]

instance TauCeti.FactorSet.instFunLike {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] : FunLike (FactorSet G M) (G × G) M

Equations

• TauCeti.FactorSet.instFunLike = { coe := TauCeti.FactorSet.toFun, coe_injective := ⋯ }

@[simp]

theorem TauCeti.FactorSet.coe_mk {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] (f : G × G → M) (hf : groupCohomology.IsMulCocycle₂ f) (hf₁ : f (1, 1) = 1) : ⇑{ toFun := f, isMulCocycle₂' := hf, map_one_one' := hf₁ } = f

theorem TauCeti.FactorSet.ext {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] {α β : FactorSet G M} (h : ∀ (p : G × G), α p = β p) : α = β

theorem TauCeti.FactorSet.ext_iff {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] {α β : FactorSet G M} : α = β ↔ ∀ (p : G × G), α p = β p

instance TauCeti.FactorSet.instFinite {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] [Finite G] [Finite M] : Finite (FactorSet G M)

theorem TauCeti.FactorSet.isMulCocycle₂ {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] (α : FactorSet G M) : groupCohomology.IsMulCocycle₂ ⇑α

The cocycle identity of a factor set, restated for the coercion ⇑α rather than for the field toFun, so that it rewrites in the goals the rest of the API produces.

theorem TauCeti.FactorSet.map_one_one {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] (α : FactorSet G M) : α (1, 1) = 1

The normalization of a factor set, restated for the coercion ⇑α rather than for the field toFun, so that it rewrites in the goals the rest of the API produces. Not @[simp]: the two lemmas below subsume it.

@[simp]

theorem TauCeti.FactorSet.map_one_fst {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] (α : FactorSet G M) (g : G) : α (1, g) = 1

@[simp]

theorem TauCeti.FactorSet.map_one_snd {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] (α : FactorSet G M) (g : G) : α (g, 1) = 1

theorem TauCeti.FactorSet.smul_apply_inv_left {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] (α : FactorSet G M) (g : G) : g • α (g⁻¹, g) = α (g, g⁻¹)

The two values of a factor set on an element and its inverse agree up to the action. This is what makes the inverse of TauCeti.FactorSet.Extension a two-sided inverse.

Pushforward along a coefficient map

def TauCeti.FactorSet.map {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] {N : Type u_1} [CommGroup N] [MulDistribMulAction G N] (α : FactorSet G M) (f : M →*[G] N) : FactorSet G N

Pushforward of a factor set along an equivariant homomorphism of coefficient modules: the factor set (g, h) ↦ f (α (g, h)) of G with values in N.

Equations

• α.map f = { toFun := fun (p : G × G) => f (α p), isMulCocycle₂' := ⋯, map_one_one' := ⋯ }

@[simp]

theorem TauCeti.FactorSet.map_apply {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] {N : Type u_1} [CommGroup N] [MulDistribMulAction G N] (α : FactorSet G M) (f : M →*[G] N) (p : G × G) : (α.map f) p = f (α p)

structure TauCeti.FactorSet.Extension {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] (α : FactorSet G M) : Type (max u v)

The twisted product M × G attached to a factor set α: the underlying set of the group extension of G by M that α determines, with multiplication ⟨a, g⟩ * ⟨b, h⟩ = ⟨a * g • b * α (g, h), g * h⟩. For the trivial factor set this is the semidirect product M ⋊ G (TauCeti.FactorSet.trivialMulEquiv).

• left : M

  The M-component of an element of the twisted product.

• right : G

  The G-component of an element of the twisted product.

theorem TauCeti.FactorSet.Extension.ext {G : Type u} {M : Type v} {inst✝ : Group G} {inst✝¹ : CommGroup M} {inst✝² : MulDistribMulAction G M} {α : FactorSet G M} {x y : α.Extension} (left : x.left = y.left) (right : x.right = y.right) : x = y

theorem TauCeti.FactorSet.Extension.ext_iff {G : Type u} {M : Type v} {inst✝ : Group G} {inst✝¹ : CommGroup M} {inst✝² : MulDistribMulAction G M} {α : FactorSet G M} {x y : α.Extension} : x = y ↔ x.left = y.left ∧ x.right = y.right

def TauCeti.FactorSet.Extension.equivProd {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] (α : FactorSet G M) : α.Extension ≃ M × G

The twisted product is M × G as a type. It is the multiplication that the factor set twists, not the underlying set.

Equations

• TauCeti.FactorSet.Extension.equivProd α = { toFun := fun (x : α.Extension) => (x.left, x.right), invFun := fun (p : M × G) => { left := p.1, right := p.2 }, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem TauCeti.FactorSet.Extension.equivProd_apply {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] {α : FactorSet G M} (x : α.Extension) : (equivProd α) x = (x.left, x.right)

@[simp]

theorem TauCeti.FactorSet.Extension.equivProd_symm_apply {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] {α : FactorSet G M} (p : M × G) : (equivProd α).symm p = { left := p.1, right := p.2 }

instance TauCeti.FactorSet.Extension.instFinite {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] {α : FactorSet G M} [Finite G] [Finite M] : Finite α.Extension

@[instance_reducible]

instance TauCeti.FactorSet.Extension.instMul {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] {α : FactorSet G M} : Mul α.Extension

Equations

• TauCeti.FactorSet.Extension.instMul = { mul := fun (x y : α.Extension) => { left := x.left * x.right • y.left * α (x.right, y.right), right := x.right * y.right } }

@[simp]

theorem TauCeti.FactorSet.Extension.mul_left {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] {α : FactorSet G M} (x y : α.Extension) : (x * y).left = x.left * x.right • y.left * α (x.right, y.right)

@[simp]

theorem TauCeti.FactorSet.Extension.mul_right {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] {α : FactorSet G M} (x y : α.Extension) : (x * y).right = x.right * y.right

@[instance_reducible]

instance TauCeti.FactorSet.Extension.instOne {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] {α : FactorSet G M} : One α.Extension

Equations

• TauCeti.FactorSet.Extension.instOne = { one := { left := 1, right := 1 } }

@[simp]

theorem TauCeti.FactorSet.Extension.one_left {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] {α : FactorSet G M} : left 1 = 1

@[simp]

theorem TauCeti.FactorSet.Extension.one_right {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] {α : FactorSet G M} : right 1 = 1

@[instance_reducible]

instance TauCeti.FactorSet.Extension.instInv {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] {α : FactorSet G M} : Inv α.Extension

Equations

• TauCeti.FactorSet.Extension.instInv = { inv := fun (x : α.Extension) => { left := x.right⁻¹ • (x.left * α (x.right, x.right⁻¹))⁻¹, right := x.right⁻¹ } }

@[simp]

theorem TauCeti.FactorSet.Extension.inv_left {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] {α : FactorSet G M} (x : α.Extension) : x⁻¹.left = x.right⁻¹ • (x.left * α (x.right, x.right⁻¹))⁻¹

@[simp]

theorem TauCeti.FactorSet.Extension.inv_right {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] {α : FactorSet G M} (x : α.Extension) : x⁻¹.right = x.right⁻¹

@[instance_reducible]

instance TauCeti.FactorSet.Extension.instGroup {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] {α : FactorSet G M} : Group α.Extension

Equations

• One or more equations did not get rendered due to their size.

def TauCeti.FactorSet.mapExtension {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] {N : Type u_1} [CommGroup N] [MulDistribMulAction G N] (α : FactorSet G M) (f : M →*[G] N) : α.Extension →* (α.map f).Extension

The homomorphism of twisted products induced by an equivariant coefficient homomorphism.

Equations

• α.mapExtension f = { toFun := fun (x : α.Extension) => { left := f x.left, right := x.right }, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem TauCeti.FactorSet.mapExtension_left {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] {N : Type u_1} [CommGroup N] [MulDistribMulAction G N] (α : FactorSet G M) (f : M →*[G] N) (x : α.Extension) : ((α.mapExtension f) x).left = f x.left

@[simp]

theorem TauCeti.FactorSet.mapExtension_right {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] {N : Type u_1} [CommGroup N] [MulDistribMulAction G N] (α : FactorSet G M) (f : M →*[G] N) (x : α.Extension) : ((α.mapExtension f) x).right = x.right

def TauCeti.FactorSet.inl {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] (α : FactorSet G M) : M →* α.Extension

The inclusion of M into the twisted product, as a ↦ ⟨a, 1⟩.

Equations

• α.inl = { toFun := fun (a : M) => { left := a, right := 1 }, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem TauCeti.FactorSet.inl_left {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] (α : FactorSet G M) (a : M) : (α.inl a).left = a

@[simp]

theorem TauCeti.FactorSet.inl_right {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] (α : FactorSet G M) (a : M) : (α.inl a).right = 1

def TauCeti.FactorSet.rightHom {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] (α : FactorSet G M) : α.Extension →* G

The projection of the twisted product onto G.

Equations

• α.rightHom = { toFun := TauCeti.FactorSet.Extension.right, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem TauCeti.FactorSet.rightHom_apply {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] (α : FactorSet G M) (x : α.Extension) : α.rightHom x = x.right

@[simp]

theorem TauCeti.FactorSet.mapExtension_comp_inl {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] (α : FactorSet G M) {N : Type u_1} [CommGroup N] [MulDistribMulAction G N] (f : M →*[G] N) : (α.mapExtension f).comp α.inl = (α.map f).inl.comp f.toMonoidHom

The induced map of extensions commutes with the coefficient inclusions.

@[simp]

theorem TauCeti.FactorSet.rightHom_comp_mapExtension {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] (α : FactorSet G M) {N : Type u_1} [CommGroup N] [MulDistribMulAction G N] (f : M →*[G] N) : (α.map f).rightHom.comp (α.mapExtension f) = α.rightHom

The induced map of extensions preserves the projection to the quotient group.

theorem TauCeti.FactorSet.inl_injective {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] (α : FactorSet G M) : Function.Injective ⇑α.inl

theorem TauCeti.FactorSet.range_inl_eq_ker_rightHom {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] (α : FactorSet G M) : α.inl.range = α.rightHom.ker

theorem TauCeti.FactorSet.rightHom_surjective {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] (α : FactorSet G M) : Function.Surjective ⇑α.rightHom

def TauCeti.FactorSet.groupExtension {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] (α : FactorSet G M) : GroupExtension M α.Extension G

The group extension 1 → M → E_α → G → 1 determined by a factor set.

Equations

• α.groupExtension = { inl := α.inl, rightHom := α.rightHom, inl_injective := ⋯, range_inl_eq_ker_rightHom := ⋯, rightHom_surjective := ⋯ }

@[simp]

theorem TauCeti.FactorSet.groupExtension_inl {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] (α : FactorSet G M) : α.groupExtension.inl = α.inl

@[simp]

theorem TauCeti.FactorSet.groupExtension_rightHom {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] (α : FactorSet G M) : α.groupExtension.rightHom = α.rightHom

def TauCeti.FactorSet.canonicalSection {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] (α : FactorSet G M) : α.groupExtension.Section

The canonical set-theoretic section g ↦ ⟨1, g⟩ of the projection. It fails to be a homomorphism by exactly α; see TauCeti.FactorSet.canonicalSection_mul.

Equations

• α.canonicalSection = { toFun := fun (g : G) => { left := 1, right := g }, rightInverse_rightHom := ⋯ }

@[simp]

theorem TauCeti.FactorSet.canonicalSection_apply {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] (α : FactorSet G M) (g : G) : α.canonicalSection g = { left := 1, right := g }

theorem TauCeti.FactorSet.canonicalSection_one {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] (α : FactorSet G M) : α.canonicalSection 1 = 1

The canonical section is normalized. Not @[simp]: canonicalSection_apply already rewrites the left-hand side, to ⟨1, 1⟩.

theorem TauCeti.FactorSet.canonicalSection_mul {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] (α : FactorSet G M) (g h : G) : α.canonicalSection g * α.canonicalSection h = α.inl (α (g, h)) * α.canonicalSection (g * h)

A factor set is the factor set of the extension it builds: the canonical section fails to be a homomorphism by exactly α.

theorem TauCeti.FactorSet.inl_mul_canonicalSection {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] (α : FactorSet G M) (x : α.Extension) : α.inl x.left * α.canonicalSection x.right = x

Every element of the twisted product factors through the canonical section, as its M-component times the section at its G-component. Together with TauCeti.FactorSet.canonicalSection_mul this reduces any statement about a homomorphism out of the extension to its values on the copy of M and on the section.

theorem TauCeti.FactorSet.mul_inl {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] (α : FactorSet G M) (x : α.Extension) (a : M) : x * α.inl a = α.inl (x.right • a) * x

Conjugation in the twisted product moves the copy of M by the action of the image in G. The copy of M is normal for a second reason: it is a kernel, by TauCeti.FactorSet.range_inl_eq_ker_rightHom.

theorem TauCeti.FactorSet.inl_range_le_center {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] (α : FactorSet G M) (h : ∀ (g : G) (a : M), g • a = a) : α.inl.range ≤ Subgroup.center α.Extension

The extension is central when G acts trivially on M. This is the case M = kˣ with the trivial action, in which a projective representation of G with factor set α is a linear representation of the extension.

theorem TauCeti.FactorSet.rescale_one {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] (α β : FactorSet G M) (x : G → M) (hx : ∀ (g h : G), α (g, h) * x (g * h) = β (g, h) * (g • x h * x g)) : x 1 = 1

A rescaling turning one factor set into another is normalized.

def TauCeti.FactorSet.rescaleEquiv {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] (α β : FactorSet G M) (x : G → M) (hx : ∀ (g h : G), α (g, h) * x (g * h) = β (g, h) * (g • x h * x g)) : α.groupExtension.Equiv β.groupExtension

Rescaling the canonical section by x turns the extension built from α into the one built from β. The hypothesis says that α and β differ by the coboundary of x; see TauCeti.FactorSet.nonempty_groupExtensionEquiv.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.FactorSet.rescaleEquiv_apply {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] (α β : FactorSet G M) (x : G → M) (hx : ∀ (g h : G), α (g, h) * x (g * h) = β (g, h) * (g • x h * x g)) (y : α.Extension) : (α.rescaleEquiv β x hx) y = { left := y.left * x y.right, right := y.right }

@[simp]

theorem TauCeti.FactorSet.rescaleEquiv_symm_apply {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] (α β : FactorSet G M) (x : G → M) (hx : ∀ (g h : G), α (g, h) * x (g * h) = β (g, h) * (g • x h * x g)) (y : β.Extension) : (α.rescaleEquiv β x hx).symm y = { left := y.left * (x y.right)⁻¹, right := y.right }

theorem TauCeti.FactorSet.nonempty_groupExtensionEquiv {G : Type u} {M : Type v} [Group G] [CommGroup M] [MulDistribMulAction G M] (α β : FactorSet G M) (h : groupCohomology.IsMulCoboundary₂ fun (p : G × G) => α p / β p) : Nonempty (α.groupExtension.Equiv β.groupExtension)

Cohomologous factor sets build equivalent extensions. Two factor sets whose quotient is a multiplicative 2-coboundary give equivalent group extensions of G by M, the equivalence rescaling the canonical section by the function the coboundary comes from.

def TauCeti.FactorSet.trivial (G : Type u) (M : Type v) [Group G] [CommGroup M] [MulDistribMulAction G M] : FactorSet G M

The trivial factor set, constantly 1. Its extension is the semidirect product (TauCeti.FactorSet.trivialMulEquiv) and is split (TauCeti.FactorSet.trivialSplitting).

Equations

• TauCeti.FactorSet.trivial G M = { toFun := fun (x : G × G) => 1, isMulCocycle₂' := ⋯, map_one_one' := ⋯ }

@[simp]

theorem TauCeti.FactorSet.trivial_apply (G : Type u) (M : Type v) [Group G] [CommGroup M] [MulDistribMulAction G M] (p : G × G) : (trivial G M) p = 1

def TauCeti.FactorSet.trivialMulEquiv (G : Type u) (M : Type v) [Group G] [CommGroup M] [MulDistribMulAction G M] : (trivial G M).Extension ≃* M ⋊[MulDistribMulAction.toMulAut G M] G

The extension attached to the trivial factor set is the semidirect product of M by G.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.FactorSet.trivialMulEquiv_apply (G : Type u) (M : Type v) [Group G] [CommGroup M] [MulDistribMulAction G M] (x : (trivial G M).Extension) : (trivialMulEquiv G M) x = ⟨x.left, x.right⟩

@[simp]

theorem TauCeti.FactorSet.trivialMulEquiv_symm_apply (G : Type u) (M : Type v) [Group G] [CommGroup M] [MulDistribMulAction G M] (x : M ⋊[MulDistribMulAction.toMulAut G M] G) : (trivialMulEquiv G M).symm x = { left := x.left, right := x.right }

def TauCeti.FactorSet.trivialSplitting (G : Type u) (M : Type v) [Group G] [CommGroup M] [MulDistribMulAction G M] : (trivial G M).groupExtension.Splitting

The extension attached to the trivial factor set is split: there the canonical section is a homomorphism.

Equations

• TauCeti.FactorSet.trivialSplitting G M = { toFun := fun (g : G) => { left := 1, right := g }, map_one' := ⋯, map_mul' := ⋯, rightInverse_rightHom := ⋯ }

@[simp]

theorem TauCeti.FactorSet.trivialSplitting_apply (G : Type u) (M : Type v) [Group G] [CommGroup M] [MulDistribMulAction G M] (g : G) : (trivialSplitting G M) g = { left := 1, right := g }