Module

CrossedDifferential.lean

Nyll.ProCGroups.FoxDifferential.Common.CrossedDifferential

62 declarations indexed from sourceView source ↗

Module documentation

Bundled crossed homomorphisms

This module defines crossed homomorphisms for an additive group action and their scalar-character specialization. It supplies the Fox product, inverse, conjugation, commutator, and power rules; restriction to coefficient-trivial subgroups; linear pushforward and group-homomorphism pullback; the standard semidirect-product representation; and the additive-group structure on the space of crossed homomorphisms.

CrossedHom and ScalarCrossedHom are the only crossed-differential representations exposed by this module. The former parallel raw-function predicate and its conversion layer have been removed, so downstream APIs operate on the bundled maps directly.

Imports7

Mathlib.Algebra.Group.Commutator
Mathlib.Algebra.Group.Units.Hom
Mathlib.Algebra.GroupWithZero.Action.Basic
Mathlib.Algebra.Group.Subgroup.Lattice
Mathlib.Algebra.Module.BigOperators
Mathlib.Algebra.Module.LinearMap.Basic
Mathlib.GroupTheory.SemidirectProduct

Imported by3

def

scalarCrossedAction

L37 ↗

FoxDifferential.scalarCrossedAction

Documentation

Scalar multiplication by a character coeff : G →* R, expressed as an additive action.

Because G is a group, every coeff g is automatically a unit; toHomUnits records that fact and produces actual additive automorphisms rather than mere additive endomorphisms.

Source context 2 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement

Lean source · statement

def scalarCrossedAction
    {R G A : Type*} [Semiring R] [Group G] [AddCommGroup A] [Module R A]
    (coeff : G →* R) : G →* Multiplicative (AddAut A)

theorem

scalarCrossedAction_apply

L44 ↗

FoxDifferential.scalarCrossedAction_apply

Documentation

The action induced by a scalar character evaluates as scalar multiplication.

Source context 2 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement

Lean source · statement

theorem scalarCrossedAction_apply
    {R G A : Type*} [Semiring R] [Group G] [AddCommGroup A] [Module R A]
    (coeff : G →* R) (g : G) (a : A) :
    scalarCrossedAction (A := A) coeff g a = coeff g • a

def

crossedSemidirectMulAction

L52 ↗

FoxDifferential.crossedSemidirectMulAction

Documentation

Convert an additive action to the multiplicative action used by Mathlib's standard SemidirectProduct.

Source context 2 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement

Lean source · statement

def crossedSemidirectMulAction
    {G A : Type*} [Group G] [AddCommGroup A]
    (action : G →* Multiplicative (AddAut A)) : G →* MulAut (Multiplicative A)

abbrev

CrossedSemidirectProduct

L58 ↗

FoxDifferential.CrossedSemidirectProduct

Documentation

The standard Mathlib semidirect product attached to an additive action.

Source context 2 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement

Lean source · statement

abbrev CrossedSemidirectProduct
    {G A : Type*} [Group G] [AddCommGroup A]
    (action : G →* Multiplicative (AddAut A))

theorem

crossedSemidirectMulAction_apply

L65 ↗

FoxDifferential.crossedSemidirectMulAction_apply

Documentation

The multiplicative form of an additive action agrees with the original action on elements.

Source context 2 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement

Lean source · statement

theorem crossedSemidirectMulAction_apply
    {G A : Type*} [Group G] [AddCommGroup A]
    (action : G →* Multiplicative (AddAut A)) (g : G) (a : A) :
    crossedSemidirectMulAction action g (Multiplicative.ofAdd a) =
      Multiplicative.ofAdd (action g a)

theorem

crossedSemidirectMulAction_toAdd

L74 ↗

FoxDifferential.crossedSemidirectMulAction_toAdd

Documentation

Read the multiplicative presentation of the action back in the original additive group.

Source context 2 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement

Lean source · statement

theorem crossedSemidirectMulAction_toAdd
    {G A : Type*} [Group G] [AddCommGroup A]
    (action : G →* Multiplicative (AddAut A)) (g : G) (a : Multiplicative A) :
    Multiplicative.toAdd (crossedSemidirectMulAction action g a) =
      action g (Multiplicative.toAdd a)

structure

CrossedHom

L82 ↗

FoxDifferential.CrossedHom

Documentation

A crossed homomorphism bundled with its acting representation and Fox--Leibniz law.

Source context 2 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement

Lean source · full declaration

structure CrossedHom
    {G A : Type*} [Group G] [AddCommGroup A]
    (action : G →* Multiplicative (AddAut A)) where
  /-- The function from the source group to the additive target. -/
  toFun : G → A
  /-- The crossed-homomorphism law with respect to the specified action. -/
  map_mul' : ∀ g h, toFun (g * h) = toFun g + action g (toFun h)

abbrev

ScalarCrossedHom

L92 ↗

FoxDifferential.ScalarCrossedHom

Documentation

Scalar-character crossed homomorphisms are a specialization of general crossed homomorphisms for the action scalarCrossedAction coeff.

Source context 2 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement

Lean source · statement

abbrev ScalarCrossedHom
    {R G : Type*} [Semiring R] [Group G]
    (coeff : G →* R) (A : Type*) [AddCommGroup A] [Module R A]

instance

instFunLike

L103 ↗

FoxDifferential.CrossedHom.instFunLike

Documentation

Crossed homomorphisms coerce to their underlying functions.

Source context 5 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement
namespace CrossedHom
variable {G A : Type*} [Group G] [AddCommGroup A]
variable {action : G →* Multiplicative (AddAut A)}

Lean source · full declaration

instance instFunLike : FunLike (CrossedHom action) G A where
  coe := CrossedHom.toFun
  coe_injective f g h := by
    cases f
    cases g
    simp_all

theorem

toFun_apply

L112 ↗

FoxDifferential.CrossedHom.toFun_apply

Documentation

The underlying function of a crossed homomorphism agrees with its coercion to a function.

Source context 5 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement
namespace CrossedHom
variable {G A : Type*} [Group G] [AddCommGroup A]
variable {action : G →* Multiplicative (AddAut A)}

Lean source · statement

theorem toFun_apply (d : CrossedHom action) (g : G) : d.toFun g = d g

theorem

ext

L116 ↗

FoxDifferential.CrossedHom.ext

Documentation

Equality of crossed homomorphisms is pointwise equality.

Source context 5 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement
namespace CrossedHom
variable {G A : Type*} [Group G] [AddCommGroup A]
variable {action : G →* Multiplicative (AddAut A)}

Lean source · statement

theorem ext {d e : CrossedHom action} (h : ∀ g, d g = e g) : d = e

theorem

map_mul

L122 ↗

FoxDifferential.CrossedHom.map_mul

Documentation

The bundled Fox--Leibniz rule for a general additive action.

Source context 5 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement
namespace CrossedHom
variable {G A : Type*} [Group G] [AddCommGroup A]
variable {action : G →* Multiplicative (AddAut A)}

Lean source · statement

theorem map_mul (d : CrossedHom action) (g h : G) :
    d (g * h) = d g + action g (d h)

theorem

map_one

L128 ↗

FoxDifferential.CrossedHom.map_one

Documentation

A crossed homomorphism vanishes at the identity.

Source context 5 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement
namespace CrossedHom
variable {G A : Type*} [Group G] [AddCommGroup A]
variable {action : G →* Multiplicative (AddAut A)}

Lean source · statement

theorem map_one (d : CrossedHom action) : d 1 = 0

theorem

map_inv

L138 ↗

FoxDifferential.CrossedHom.map_inv

Documentation

Inverse rule for a crossed homomorphism.

Source context 5 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement
namespace CrossedHom
variable {G A : Type*} [Group G] [AddCommGroup A]
variable {action : G →* Multiplicative (AddAut A)}

Lean source · statement

theorem map_inv (d : CrossedHom action) (g : G) :
    d g⁻¹ = -(action g⁻¹ (d g))

theorem

map_inv_mul

L146 ↗

FoxDifferential.CrossedHom.map_inv_mul

Documentation

Formula for multiplying by an inverse on the left.

Source context 5 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement
namespace CrossedHom
variable {G A : Type*} [Group G] [AddCommGroup A]
variable {action : G →* Multiplicative (AddAut A)}

Lean source · statement

theorem map_inv_mul (d : CrossedHom action) (g h : G) :
    d (g⁻¹ * h) = -(action g⁻¹ (d g)) + action g⁻¹ (d h)

theorem

map_mul_inv

L151 ↗

FoxDifferential.CrossedHom.map_mul_inv

Documentation

Formula for multiplying by an inverse on the right.

Source context 5 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement
namespace CrossedHom
variable {G A : Type*} [Group G] [AddCommGroup A]
variable {action : G →* Multiplicative (AddAut A)}

Lean source · statement

theorem map_mul_inv (d : CrossedHom action) (g h : G) :
    d (g * h⁻¹) = d g - action (g * h⁻¹) (d h)

theorem

map_div

L158 ↗

FoxDifferential.CrossedHom.map_div

Documentation

Division rule for a crossed homomorphism.

Source context 5 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement
namespace CrossedHom
variable {G A : Type*} [Group G] [AddCommGroup A]
variable {action : G →* Multiplicative (AddAut A)}

Lean source · statement

theorem map_div (d : CrossedHom action) (g h : G) :
    d (g / h) = d g - action (g / h) (d h)

theorem

map_conj

L163 ↗

FoxDifferential.CrossedHom.map_conj

Documentation

Conjugation rule for a crossed homomorphism.

Source context 5 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement
namespace CrossedHom
variable {G A : Type*} [Group G] [AddCommGroup A]
variable {action : G →* Multiplicative (AddAut A)}

Lean source · statement

theorem map_conj (d : CrossedHom action) (g h : G) :
    d (g * h * g⁻¹) =
      d g + action g (d h) - action (g * h * g⁻¹) (d g)

theorem

map_commutator

L169 ↗

FoxDifferential.CrossedHom.map_commutator

Documentation

Commutator rule for a crossed homomorphism.

Source context 5 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement
namespace CrossedHom
variable {G A : Type*} [Group G] [AddCommGroup A]
variable {action : G →* Multiplicative (AddAut A)}

Lean source · statement

theorem map_commutator (d : CrossedHom action) (g h : G) :
    d ⁅g, h⁆ =
      d g + action g (d h) - action (g * h * g⁻¹) (d g) -
        action ⁅g, h⁆ (d h)

theorem

map_pow

L176 ↗

FoxDifferential.CrossedHom.map_pow

Documentation

Positive-power rule for a crossed homomorphism.

Source context 5 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement
namespace CrossedHom
variable {G A : Type*} [Group G] [AddCommGroup A]
variable {action : G →* Multiplicative (AddAut A)}

Lean source · full declaration

theorem map_pow (d : CrossedHom action) (g : G) (n : ℕ) :
    d (g ^ n) = (Finset.range n).sum (fun k => action (g ^ k) (d g)) := by
  induction n with
  | zero => simp only [pow_zero, map_one, Finset.range_zero, Finset.sum_empty]
  | succ n ih =>
      rw [pow_succ, d.map_mul, ih, Finset.sum_range_succ]

def

toSemidirectMonoidHom

L185 ↗

FoxDifferential.CrossedHom.toSemidirectMonoidHom

Documentation

The graph of a crossed homomorphism is an ordinary homomorphism into the standard semidirect product.

Source context 5 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement
namespace CrossedHom
variable {G A : Type*} [Group G] [AddCommGroup A]
variable {action : G →* Multiplicative (AddAut A)}

Lean source · full declaration

def toSemidirectMonoidHom (d : CrossedHom action) :
    G →* CrossedSemidirectProduct action where
  toFun g := ⟨Multiplicative.ofAdd (d g), g⟩
  map_one' := by
    apply SemidirectProduct.ext
    · change d 1 = 0
      exact d.map_one
    · rfl
  map_mul' g h := by
    apply SemidirectProduct.ext
    · change d (g * h) = d g + action g (d h)
      exact d.map_mul g h
    · rfl

theorem

toSemidirectMonoidHom_left

L201 ↗

FoxDifferential.CrossedHom.toSemidirectMonoidHom_left

Documentation

The left component of the semidirect-product graph is the value of the crossed homomorphism.

Source context 5 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement
namespace CrossedHom
variable {G A : Type*} [Group G] [AddCommGroup A]
variable {action : G →* Multiplicative (AddAut A)}

Lean source · statement

theorem toSemidirectMonoidHom_left (d : CrossedHom action) (g : G) :
    Multiplicative.toAdd (d.toSemidirectMonoidHom g).left = d g

theorem

toSemidirectMonoidHom_right

L207 ↗

FoxDifferential.CrossedHom.toSemidirectMonoidHom_right

Documentation

The right component of the semidirect-product graph is the original group element.

Source context 5 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement
namespace CrossedHom
variable {G A : Type*} [Group G] [AddCommGroup A]
variable {action : G →* Multiplicative (AddAut A)}

Lean source · statement

theorem toSemidirectMonoidHom_right (d : CrossedHom action) (g : G) :
    (d.toSemidirectMonoidHom g).right = g

def

ofSemidirectMonoidHom

L213 ↗

FoxDifferential.CrossedHom.ofSemidirectMonoidHom

Documentation

Recover a crossed homomorphism from a semidirect-product homomorphism whose right component is the identity.

Source context 5 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement
namespace CrossedHom
variable {G A : Type*} [Group G] [AddCommGroup A]
variable {action : G →* Multiplicative (AddAut A)}

Lean source · full declaration

def ofSemidirectMonoidHom
    (f : G →* CrossedSemidirectProduct action)
    (hright : ∀ g, (f g).right = g) : CrossedHom action where
  toFun g := Multiplicative.toAdd (f g).left
  map_mul' := by
    intro g h
    have hleft := congrArg SemidirectProduct.left (f.map_mul g h)
    rw [SemidirectProduct.mul_left] at hleft
    have hleftAdd := congrArg Multiplicative.toAdd hleft
    simpa only [toAdd_mul, crossedSemidirectMulAction_toAdd, hright] using hleftAdd

theorem

ofSemidirectMonoidHom_apply

L226 ↗

FoxDifferential.CrossedHom.ofSemidirectMonoidHom_apply

Documentation

Recovering a crossed homomorphism takes the additive form of the graph's left component.

Source context 5 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement
namespace CrossedHom
variable {G A : Type*} [Group G] [AddCommGroup A]
variable {action : G →* Multiplicative (AddAut A)}

Lean source · statement

theorem ofSemidirectMonoidHom_apply
    (f : G →* CrossedSemidirectProduct action)
    (hright : ∀ g, (f g).right = g) (g : G) :
    ofSemidirectMonoidHom f hright g = Multiplicative.toAdd (f g).left

theorem

ofSemidirectMonoidHom_toSemidirectMonoidHom

L234 ↗

FoxDifferential.CrossedHom.ofSemidirectMonoidHom_toSemidirectMonoidHom

Documentation

Recovering a crossed homomorphism from its semidirect-product graph returns the original map.

Source context 5 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement
namespace CrossedHom
variable {G A : Type*} [Group G] [AddCommGroup A]
variable {action : G →* Multiplicative (AddAut A)}

Lean source · full declaration

theorem ofSemidirectMonoidHom_toSemidirectMonoidHom (d : CrossedHom action) :
    ofSemidirectMonoidHom d.toSemidirectMonoidHom
      (fun g => toSemidirectMonoidHom_right d g) = d := by
  apply CrossedHom.ext
  intro g
  rfl

theorem

toSemidirectMonoidHom_ofSemidirectMonoidHom

L243 ↗

FoxDifferential.CrossedHom.toSemidirectMonoidHom_ofSemidirectMonoidHom

Documentation

The graph construction loses no information: a semidirect-product homomorphism over the identity is exactly the graph of the crossed homomorphism obtained from its left component.

Source context 5 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement
namespace CrossedHom
variable {G A : Type*} [Group G] [AddCommGroup A]
variable {action : G →* Multiplicative (AddAut A)}

Lean source · statement

theorem toSemidirectMonoidHom_ofSemidirectMonoidHom
    (f : G →* CrossedSemidirectProduct action)
    (hright : ∀ g, (f g).right = g) :
    (ofSemidirectMonoidHom f hright).toSemidirectMonoidHom = f

def

compMonoidHom

L254 ↗

FoxDifferential.CrossedHom.compMonoidHom

Documentation

Pull back a crossed homomorphism along a group homomorphism.

Source context 5 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement
namespace CrossedHom
variable {G A : Type*} [Group G] [AddCommGroup A]
variable {action : G →* Multiplicative (AddAut A)}

Lean source · full declaration

def compMonoidHom {K : Type*} [Group K]
    (d : CrossedHom action) (φ : K →* G) : CrossedHom (action.comp φ) where
  toFun k := d (φ k)
  map_mul' := by
    intro g h
    change d (φ (g * h)) = d (φ g) + action (φ g) (d (φ h))
    rw [φ.map_mul]
    exact d.map_mul (φ g) (φ h)

theorem

compMonoidHom_apply

L265 ↗

FoxDifferential.CrossedHom.compMonoidHom_apply

Documentation

Pullback along a group homomorphism evaluates by precomposition.

Source context 5 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement
namespace CrossedHom
variable {G A : Type*} [Group G] [AddCommGroup A]
variable {action : G →* Multiplicative (AddAut A)}

Lean source · statement

theorem compMonoidHom_apply {K : Type*} [Group K]
    (d : CrossedHom action) (φ : K →* G) (k : K) :
    d.compMonoidHom φ k = d (φ k)

def

mapAddEquivariant

L271 ↗

FoxDifferential.CrossedHom.mapAddEquivariant

Documentation

Push a crossed homomorphism through an equivariant additive homomorphism.

Source context 5 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement
namespace CrossedHom
variable {G A : Type*} [Group G] [AddCommGroup A]
variable {action : G →* Multiplicative (AddAut A)}

Lean source · full declaration

def mapAddEquivariant (d : CrossedHom action) {B : Type*} [AddCommGroup B]
    (actionB : G →* Multiplicative (AddAut B)) (f : A →+ B)
    (hf : ∀ g a, f (action g a) = actionB g (f a))
    : CrossedHom actionB where
  toFun g := f (d g)
  map_mul' := by
    intro g h
    rw [d.map_mul g h, map_add, hf]

theorem

mapAddEquivariant_apply

L282 ↗

FoxDifferential.CrossedHom.mapAddEquivariant_apply

Documentation

Equivariant pushforward evaluates by applying the additive homomorphism to each value.

Source context 5 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement
namespace CrossedHom
variable {G A : Type*} [Group G] [AddCommGroup A]
variable {action : G →* Multiplicative (AddAut A)}

Lean source · statement

theorem mapAddEquivariant_apply {B : Type*} [AddCommGroup B]
    (actionB : G →* Multiplicative (AddAut B)) (f : A →+ B)
    (hf : ∀ g a, f (action g a) = actionB g (f a))
    (d : CrossedHom action) (g : G) :
    d.mapAddEquivariant actionB f hf g = f (d g)

theorem

eqOn_closure

L290 ↗

FoxDifferential.CrossedHom.eqOn_closure

Documentation

Crossed homomorphisms agreeing on a set agree on the subgroup it generates.

Source context 5 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement
namespace CrossedHom
variable {G A : Type*} [Group G] [AddCommGroup A]
variable {action : G →* Multiplicative (AddAut A)}

Lean source · statement

theorem eqOn_closure (d e : CrossedHom action) {s : Set G}
    (hs : Set.EqOn d e s) :
    Set.EqOn d e ((Subgroup.closure s : Subgroup G) : Set G)

theorem

eq_of_closure_eq_top

L305 ↗

FoxDifferential.CrossedHom.eq_of_closure_eq_top

Documentation

Crossed homomorphisms are determined by their values on a generating set.

Source context 5 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement
namespace CrossedHom
variable {G A : Type*} [Group G] [AddCommGroup A]
variable {action : G →* Multiplicative (AddAut A)}

Lean source · statement

theorem eq_of_closure_eq_top (d e : CrossedHom action) {s : Set G}
    (hsgen : Subgroup.closure s = ⊤) (hs : Set.EqOn d e s) : d = e

instance

instZero

L312 ↗

FoxDifferential.CrossedHom.instZero

Documentation

The zero crossed homomorphism.

Source context 5 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement
namespace CrossedHom
variable {G A : Type*} [Group G] [AddCommGroup A]
variable {action : G →* Multiplicative (AddAut A)}

Lean source · full declaration

instance instZero : Zero (CrossedHom action) where
  zero := ⟨fun _ => 0, by intro g h; simp only [map_zero, add_zero]⟩

instance

instAdd

L316 ↗

FoxDifferential.CrossedHom.instAdd

Documentation

Pointwise addition of crossed homomorphisms.

Source context 5 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement
namespace CrossedHom
variable {G A : Type*} [Group G] [AddCommGroup A]
variable {action : G →* Multiplicative (AddAut A)}

Lean source · full declaration

instance instAdd : Add (CrossedHom action) where
  add d e := ⟨fun g => d g + e g, by
    intro g h
    rw [d.map_mul g h, e.map_mul g h, map_add]
    ac_rfl⟩

theorem

zero_apply

L324 ↗

FoxDifferential.CrossedHom.zero_apply

Documentation

The zero crossed homomorphism vanishes at every group element.

Source context 5 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement
namespace CrossedHom
variable {G A : Type*} [Group G] [AddCommGroup A]
variable {action : G →* Multiplicative (AddAut A)}

Lean source · statement

theorem zero_apply (g : G) : (0 : CrossedHom action) g = 0

theorem

add_apply

L328 ↗

FoxDifferential.CrossedHom.add_apply

Documentation

Addition of crossed homomorphisms is computed pointwise.

Source context 5 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement
namespace CrossedHom
variable {G A : Type*} [Group G] [AddCommGroup A]
variable {action : G →* Multiplicative (AddAut A)}

Lean source · statement

theorem add_apply (d e : CrossedHom action) (g : G) : (d + e) g = d g + e g

instance

instSMulNat

L331 ↗

FoxDifferential.CrossedHom.instSMulNat

Documentation

Natural-number scalar multiplication of crossed homomorphisms is repeated pointwise addition.

Source context 5 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement
namespace CrossedHom
variable {G A : Type*} [Group G] [AddCommGroup A]
variable {action : G →* Multiplicative (AddAut A)}

Lean source · statement

instance instSMulNat : SMul ℕ (CrossedHom action)

theorem

nsmul_apply

L335 ↗

FoxDifferential.CrossedHom.nsmul_apply

Documentation

Natural-number scalar multiplication of crossed homomorphisms is computed pointwise.

Source context 5 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement
namespace CrossedHom
variable {G A : Type*} [Group G] [AddCommGroup A]
variable {action : G →* Multiplicative (AddAut A)}

Lean source · statement

theorem nsmul_apply (n : ℕ) (d : CrossedHom action) (g : G) :
    (n • d) g = n • d g

instance

instAddCommMonoid

L346 ↗

FoxDifferential.CrossedHom.instAddCommMonoid

Documentation

A temporary additive-monoid structure used while constructing the stronger additive group.

Source context 5 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement
namespace CrossedHom
variable {G A : Type*} [Group G] [AddCommGroup A]
variable {action : G →* Multiplicative (AddAut A)}

Lean source · statement

instance instAddCommMonoid : AddCommMonoid (CrossedHom action)

instance

instNeg

L353 ↗

FoxDifferential.CrossedHom.instNeg

Documentation

Negation of crossed homomorphisms is computed pointwise.

Source context 6 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement
namespace CrossedHom
variable {G A : Type*} [Group G] [AddCommGroup A]
variable {action : G →* Multiplicative (AddAut A)}
/-- A temporary additive-monoid structure used while constructing the stronger additive group. -/
local instance instAddCommMonoid : AddCommMonoid (CrossedHom action) :=
  Function.Injective.addCommMonoid
    (fun d : CrossedHom action => d.toFun)
    (by intro d e h; exact CrossedHom.ext (congrFun h))
    rfl (fun _ _ => rfl) (fun d n => by funext g; exact nsmul_apply n d g)

Lean source · full declaration

instance instNeg : Neg (CrossedHom action) where
  neg d := ⟨fun g => -d g, by
    intro g h
    rw [d.map_mul g h, map_neg]
    simp only [neg_add_rev, add_comm]⟩

instance

instSub

L360 ↗

FoxDifferential.CrossedHom.instSub

Documentation

Subtraction of crossed homomorphisms is computed pointwise.

Source context 6 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement
namespace CrossedHom
variable {G A : Type*} [Group G] [AddCommGroup A]
variable {action : G →* Multiplicative (AddAut A)}
/-- A temporary additive-monoid structure used while constructing the stronger additive group. -/
local instance instAddCommMonoid : AddCommMonoid (CrossedHom action) :=
  Function.Injective.addCommMonoid
    (fun d : CrossedHom action => d.toFun)
    (by intro d e h; exact CrossedHom.ext (congrFun h))
    rfl (fun _ _ => rfl) (fun d n => by funext g; exact nsmul_apply n d g)

Lean source · full declaration

instance instSub : Sub (CrossedHom action) where
  sub d e := ⟨fun g => d g - e g, by
    intro g h
    rw [d.map_mul g h, e.map_mul g h, map_sub]
    simp only [sub_eq_add_neg, neg_add_rev]
    ac_rfl⟩

theorem

neg_apply

L369 ↗

FoxDifferential.CrossedHom.neg_apply

Documentation

Evaluating a negated crossed homomorphism negates its value.

Source context 6 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement
namespace CrossedHom
variable {G A : Type*} [Group G] [AddCommGroup A]
variable {action : G →* Multiplicative (AddAut A)}
/-- A temporary additive-monoid structure used while constructing the stronger additive group. -/
local instance instAddCommMonoid : AddCommMonoid (CrossedHom action) :=
  Function.Injective.addCommMonoid
    (fun d : CrossedHom action => d.toFun)
    (by intro d e h; exact CrossedHom.ext (congrFun h))
    rfl (fun _ _ => rfl) (fun d n => by funext g; exact nsmul_apply n d g)

Lean source · statement

theorem neg_apply (d : CrossedHom action) (g : G) : (-d) g = -d g

theorem

sub_apply

L373 ↗

FoxDifferential.CrossedHom.sub_apply

Documentation

Evaluating a difference of crossed homomorphisms subtracts their values.

Source context 6 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement
namespace CrossedHom
variable {G A : Type*} [Group G] [AddCommGroup A]
variable {action : G →* Multiplicative (AddAut A)}
/-- A temporary additive-monoid structure used while constructing the stronger additive group. -/
local instance instAddCommMonoid : AddCommMonoid (CrossedHom action) :=
  Function.Injective.addCommMonoid
    (fun d : CrossedHom action => d.toFun)
    (by intro d e h; exact CrossedHom.ext (congrFun h))
    rfl (fun _ _ => rfl) (fun d n => by funext g; exact nsmul_apply n d g)

Lean source · statement

theorem sub_apply (d e : CrossedHom action) (g : G) : (d - e) g = d g - e g

instance

instSMulInt

L377 ↗

FoxDifferential.CrossedHom.instSMulInt

Documentation

Integer scalar multiplication of crossed homomorphisms is repeated pointwise addition or subtraction.

Source context 6 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement
namespace CrossedHom
variable {G A : Type*} [Group G] [AddCommGroup A]
variable {action : G →* Multiplicative (AddAut A)}
/-- A temporary additive-monoid structure used while constructing the stronger additive group. -/
local instance instAddCommMonoid : AddCommMonoid (CrossedHom action) :=
  Function.Injective.addCommMonoid
    (fun d : CrossedHom action => d.toFun)
    (by intro d e h; exact CrossedHom.ext (congrFun h))
    rfl (fun _ _ => rfl) (fun d n => by funext g; exact nsmul_apply n d g)

Lean source · statement

instance instSMulInt : SMul ℤ (CrossedHom action)

theorem

zsmul_apply

L382 ↗

FoxDifferential.CrossedHom.zsmul_apply

Documentation

Integer scalar multiplication of crossed homomorphisms is computed pointwise.

Source context 6 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement
namespace CrossedHom
variable {G A : Type*} [Group G] [AddCommGroup A]
variable {action : G →* Multiplicative (AddAut A)}
/-- A temporary additive-monoid structure used while constructing the stronger additive group. -/
local instance instAddCommMonoid : AddCommMonoid (CrossedHom action) :=
  Function.Injective.addCommMonoid
    (fun d : CrossedHom action => d.toFun)
    (by intro d e h; exact CrossedHom.ext (congrFun h))
    rfl (fun _ _ => rfl) (fun d n => by funext g; exact nsmul_apply n d g)

Lean source · statement

theorem zsmul_apply (z : ℤ) (d : CrossedHom action) (g : G) :
    (z • d) g = z • d g

instance

instAddCommGroup

L393 ↗

FoxDifferential.CrossedHom.instAddCommGroup

Documentation

Pointwise operations make crossed homomorphisms an additive commutative group.

Source context 6 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement
namespace CrossedHom
variable {G A : Type*} [Group G] [AddCommGroup A]
variable {action : G →* Multiplicative (AddAut A)}
/-- A temporary additive-monoid structure used while constructing the stronger additive group. -/
local instance instAddCommMonoid : AddCommMonoid (CrossedHom action) :=
  Function.Injective.addCommMonoid
    (fun d : CrossedHom action => d.toFun)
    (by intro d e h; exact CrossedHom.ext (congrFun h))
    rfl (fun _ _ => rfl) (fun d n => by funext g; exact nsmul_apply n d g)

Lean source · statement

instance instAddCommGroup : AddCommGroup (CrossedHom action)

theorem

map_mul

L410 ↗

FoxDifferential.ScalarCrossedHom.map_mul

Documentation

Scalar crossed homomorphisms satisfy the scalar Fox--Leibniz product rule.

Source context 5 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement
namespace ScalarCrossedHom
variable {R G A : Type*} [Semiring R] [Group G] [AddCommGroup A] [Module R A]
variable {coeff : G →* R}

Lean source · statement

theorem map_mul (d : ScalarCrossedHom coeff A) (g h : G) :
    d (g * h) = d g + coeff g • d h

theorem

map_one

L416 ↗

FoxDifferential.ScalarCrossedHom.map_one

Documentation

A scalar crossed homomorphism vanishes at the identity.

Source context 5 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement
namespace ScalarCrossedHom
variable {R G A : Type*} [Semiring R] [Group G] [AddCommGroup A] [Module R A]
variable {coeff : G →* R}

Lean source · statement

theorem map_one (d : ScalarCrossedHom coeff A) : d 1 = 0

theorem

map_inv

L420 ↗

FoxDifferential.ScalarCrossedHom.map_inv

Documentation

The value of a scalar crossed homomorphism at an inverse is the transported negative value.

Source context 5 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement
namespace ScalarCrossedHom
variable {R G A : Type*} [Semiring R] [Group G] [AddCommGroup A] [Module R A]
variable {coeff : G →* R}

Lean source · statement

theorem map_inv (d : ScalarCrossedHom coeff A) (g : G) :
    d g⁻¹ = -(coeff g⁻¹ • d g)

theorem

map_inv_mul

L425 ↗

FoxDifferential.ScalarCrossedHom.map_inv_mul

Documentation

Formula for a scalar crossed homomorphism on a product with an inverse on the left.

Source context 5 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement
namespace ScalarCrossedHom
variable {R G A : Type*} [Semiring R] [Group G] [AddCommGroup A] [Module R A]
variable {coeff : G →* R}

Lean source · statement

theorem map_inv_mul (d : ScalarCrossedHom coeff A) (g h : G) :
    d (g⁻¹ * h) = -(coeff g⁻¹ • d g) + coeff g⁻¹ • d h

theorem

map_mul_inv

L430 ↗

FoxDifferential.ScalarCrossedHom.map_mul_inv

Documentation

Formula for a scalar crossed homomorphism on a product with an inverse on the right.

Source context 5 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement
namespace ScalarCrossedHom
variable {R G A : Type*} [Semiring R] [Group G] [AddCommGroup A] [Module R A]
variable {coeff : G →* R}

Lean source · statement

theorem map_mul_inv (d : ScalarCrossedHom coeff A) (g h : G) :
    d (g * h⁻¹) = d g - coeff (g * h⁻¹) • d h

theorem

map_div

L435 ↗

FoxDifferential.ScalarCrossedHom.map_div

Documentation

The scalar Fox rule written for group division.

Source context 5 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement
namespace ScalarCrossedHom
variable {R G A : Type*} [Semiring R] [Group G] [AddCommGroup A] [Module R A]
variable {coeff : G →* R}

Lean source · statement

theorem map_div (d : ScalarCrossedHom coeff A) (g h : G) :
    d (g / h) = d g - coeff (g / h) • d h

theorem

map_conj

L440 ↗

FoxDifferential.ScalarCrossedHom.map_conj

Documentation

The scalar crossed-homomorphism formula for a conjugate.

Source context 5 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement
namespace ScalarCrossedHom
variable {R G A : Type*} [Semiring R] [Group G] [AddCommGroup A] [Module R A]
variable {coeff : G →* R}

Lean source · statement

theorem map_conj (d : ScalarCrossedHom coeff A) (g h : G) :
    d (g * h * g⁻¹) = d g + coeff g • d h - coeff (g * h * g⁻¹) • d g

theorem

map_commutator

L445 ↗

FoxDifferential.ScalarCrossedHom.map_commutator

Documentation

The scalar crossed-homomorphism formula for a commutator.

Source context 5 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement
namespace ScalarCrossedHom
variable {R G A : Type*} [Semiring R] [Group G] [AddCommGroup A] [Module R A]
variable {coeff : G →* R}

Lean source · statement

theorem map_commutator (d : ScalarCrossedHom coeff A) (g h : G) :
    d ⁅g, h⁆ = d g + coeff g • d h - coeff (g * h * g⁻¹) • d g -
      coeff ⁅g, h⁆ • d h

theorem

map_pow

L451 ↗

FoxDifferential.ScalarCrossedHom.map_pow

Documentation

The value on a positive power is the sum of the translates of the value on its base.

Source context 5 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement
namespace ScalarCrossedHom
variable {R G A : Type*} [Semiring R] [Group G] [AddCommGroup A] [Module R A]
variable {coeff : G →* R}

Lean source · full declaration

theorem map_pow (d : ScalarCrossedHom coeff A) (g : G) (n : ℕ) :
    d (g ^ n) = (Finset.range n).sum (fun k => coeff (g ^ k) • d g) := by
  simpa only [scalarCrossedAction_apply] using CrossedHom.map_pow d g n

def

restrictTrivialSubgroupAddMonoidHom

L456 ↗

FoxDifferential.ScalarCrossedHom.restrictTrivialSubgroupAddMonoidHom

Documentation

Restrict a scalar crossed homomorphism to a subgroup on which its coefficient is trivial.

Source context 5 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement
namespace ScalarCrossedHom
variable {R G A : Type*} [Semiring R] [Group G] [AddCommGroup A] [Module R A]
variable {coeff : G →* R}

Lean source · full declaration

def restrictTrivialSubgroupAddMonoidHom
    (d : ScalarCrossedHom coeff A) (N : Subgroup G)
    (hN : ∀ n : N, coeff n = 1) :
    Additive N →+ A where
  toFun n := d ((Additive.toMul n : N) : G)
  map_zero' := by
    change d (1 : G) = 0
    exact map_one d
  map_add' g h := by
    change d (((Additive.toMul g : N) * (Additive.toMul h : N) : N) : G) =
      d ((Additive.toMul g : N) : G) + d ((Additive.toMul h : N) : G)
    have hmul :=
      d.map_mul ((Additive.toMul g : N) : G) ((Additive.toMul h : N) : G)
    simpa only [Subgroup.coe_mul, hN (Additive.toMul g), one_smul] using hmul

theorem

restrictTrivialSubgroupAddMonoidHom_apply

L473 ↗

FoxDifferential.ScalarCrossedHom.restrictTrivialSubgroupAddMonoidHom_apply

Documentation

Restriction to a coefficient-trivial subgroup evaluates as the original crossed homomorphism.

Source context 5 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement
namespace ScalarCrossedHom
variable {R G A : Type*} [Semiring R] [Group G] [AddCommGroup A] [Module R A]
variable {coeff : G →* R}

Lean source · statement

theorem restrictTrivialSubgroupAddMonoidHom_apply
    (d : ScalarCrossedHom coeff A) (N : Subgroup G)
    (hN : ∀ n : N, coeff n = 1) (g : N) :
    restrictTrivialSubgroupAddMonoidHom d N hN (Additive.ofMul g) = d g

def

mapLinear

L481 ↗

FoxDifferential.ScalarCrossedHom.mapLinear

Documentation

A linear map is equivariant for scalar crossed actions and hence maps scalar crossed homomorphisms to scalar crossed homomorphisms.

Source context 5 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement
namespace ScalarCrossedHom
variable {R G A : Type*} [Semiring R] [Group G] [AddCommGroup A] [Module R A]
variable {coeff : G →* R}

Lean source · statement

def mapLinear (d : ScalarCrossedHom coeff A) {B : Type*} [AddCommGroup B] [Module R B]
    (f : A →ₗ[R] B) : ScalarCrossedHom coeff B

theorem

mapLinear_apply

L491 ↗

FoxDifferential.ScalarCrossedHom.mapLinear_apply

Documentation

Linear pushforward evaluates by applying the linear map to each crossed-homomorphism value.

Source context 5 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement
namespace ScalarCrossedHom
variable {R G A : Type*} [Semiring R] [Group G] [AddCommGroup A] [Module R A]
variable {coeff : G →* R}

Lean source · statement

theorem mapLinear_apply {B : Type*} [AddCommGroup B] [Module R B]
    (d : ScalarCrossedHom coeff A) (f : A →ₗ[R] B) (g : G) :
    d.mapLinear f g = f (d g)

def

compMonoidHom

L497 ↗

FoxDifferential.ScalarCrossedHom.compMonoidHom

Documentation

Pull back a scalar crossed homomorphism while retaining its scalar specialization.

Source context 5 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement
namespace ScalarCrossedHom
variable {R G A : Type*} [Semiring R] [Group G] [AddCommGroup A] [Module R A]
variable {coeff : G →* R}

Lean source · full declaration

def compMonoidHom {K : Type*} [Group K]
    (d : ScalarCrossedHom coeff A) (φ : K →* G) : ScalarCrossedHom (coeff.comp φ) A where
  toFun k := d (φ k)
  map_mul' := by
    intro g h
    change d (φ (g * h)) = d (φ g) + coeff (φ g) • d (φ h)
    rw [φ.map_mul]
    exact d.map_mul (φ g) (φ h)

theorem

compMonoidHom_apply

L508 ↗

FoxDifferential.ScalarCrossedHom.compMonoidHom_apply

Documentation

Pullback of a scalar crossed homomorphism evaluates by precomposition.

Source context 5 commands

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

namespace FoxDifferential
open scoped BigOperators commutatorElement
namespace ScalarCrossedHom
variable {R G A : Type*} [Semiring R] [Group G] [AddCommGroup A] [Module R A]
variable {coeff : G →* R}

Lean source · statement

theorem compMonoidHom_apply {K : Type*} [Group K]
    (d : ScalarCrossedHom coeff A) (φ : K →* G) (k : K) :
    d.compMonoidHom φ k = d (φ k)

Module documentation

Bundled crossed homomorphisms

Declarations