Module

FiniteOrbitProduct.lean

Nyll.GaloisCohomology.GroupTheory.FiniteOrbitProduct

3 declarations indexed from sourceView source ↗

Module documentation

Products over finite automorphism orbits

The product of all translates is fixed by the acting finite group. If a commuting automorphism changes the original element by a fixed factor, it changes the orbit product by that factor raised to the group's cardinality.

Imports4

Mathlib.Algebra.Group.End
Mathlib.Algebra.Group.Commute.Defs
Mathlib.Algebra.BigOperators.Group.Finset.Basic
Mathlib.Data.Fintype.Card

Imported by2

def

finiteOrbitProduct

L25 ↗

GroupTheory.finiteOrbitProduct

Documentation

The product of all translates, indexed by the acting finite monoid.

Source context 2 commands

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

namespace GroupTheory
open scoped BigOperators

Lean source · statement

def finiteOrbitProduct {G A : Type*} [Monoid G] [Fintype G] [CommMonoid A]
    (ρ : G →* MulAut A) (C : A) : A

theorem

finiteOrbitProduct_invariant

L30 ↗

GroupTheory.finiteOrbitProduct_invariant

Documentation

Reindexing by left multiplication makes the orbit product invariant.

Source context 2 commands

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

namespace GroupTheory
open scoped BigOperators

Lean source · statement

theorem finiteOrbitProduct_invariant
    {G A : Type*} [Group G] [Fintype G] [CommMonoid A]
    (ρ : G →* MulAut A) (C : A) (g : G) :
    ρ g (finiteOrbitProduct ρ C) = finiteOrbitProduct ρ C

theorem

finiteOrbitProduct_map_div

L44 ↗

GroupTheory.finiteOrbitProduct_map_div

Documentation

A fixed multiplicative difference accumulates once for each translate.

Source context 2 commands

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

namespace GroupTheory
open scoped BigOperators

Lean source · statement

theorem finiteOrbitProduct_map_div
    {G A : Type*} [Monoid G] [Fintype G] [CommGroup A]
    (ρ : G →* MulAut A) (α : MulAut A) (C D : A)
    (hcomm : ∀ g : G, Commute α (ρ g))
    (hdiff : α C / C = D) (hD : ∀ g : G, ρ g D = D) :
    α (finiteOrbitProduct ρ C) / finiteOrbitProduct ρ C = D ^ Fintype.card G

Module documentation

Products over finite automorphism orbits

Declarations

finiteOrbitProduct

finiteOrbitProduct_invariant

finiteOrbitProduct_map_div