ProCGroups.FoxDifferential.Common.CrossedDifferential
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.
imports
- 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
def scalarCrossedAction
{R G A : Type*} [Semiring R] [Group G] [AddCommGroup A] [Module R A]
(coeff : G →* R) : G →* Multiplicative (AddAut A) :=
(DistribMulAction.toAddAut Rˣ A).comp coeff.toHomUnitsScalar 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.
@[simp]
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 • aThe action induced by a scalar character evaluates as scalar multiplication.
Show Lean proof
rfldef crossedSemidirectMulAction
{G A : Type*} [Group G] [AddCommGroup A]
(action : G →* Multiplicative (AddAut A)) : G →* MulAut (Multiplicative A) :=
(MulAutMultiplicative A).symm.toMonoidHom.comp actionConvert an additive action to the multiplicative action used by Mathlib's standard SemidirectProduct.
abbrev CrossedSemidirectProduct
{G A : Type*} [Group G] [AddCommGroup A]
(action : G →* Multiplicative (AddAut A)) :=
SemidirectProduct (Multiplicative A) G (crossedSemidirectMulAction action)The standard Mathlib semidirect product attached to an additive action.
@[simp]
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)The multiplicative form of an additive action agrees with the original action on elements.
Show Lean proof
rfl@[simp]
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)Read the multiplicative presentation of the action back in the original additive group.
Show Lean proof
rflstructure 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)A crossed homomorphism bundled with its acting representation and Fox--Leibniz law.
abbrev ScalarCrossedHom
{R G : Type*} [Semiring R] [Group G]
(coeff : G →* R) (A : Type*) [AddCommGroup A] [Module R A] :=
CrossedHom (scalarCrossedAction (A := A) coeff)Scalar-character crossed homomorphisms are a specialization of general crossed homomorphisms for the action scalarCrossedAction coeff.
instance instFunLike : FunLike (CrossedHom action) G A where
coe := CrossedHom.toFun
coe_injective f g h := by
cases f
cases g
simp_allCrossed homomorphisms coerce to their underlying functions.
@[simp]
theorem toFun_apply (d : CrossedHom action) (g : G) : d.toFun g = d gThe underlying function of a crossed homomorphism agrees with its coercion to a function.
Show Lean proof
rfl@[ext]
theorem ext {d e : CrossedHom action} (h : ∀ g, d g = e g) : d = eEquality of crossed homomorphisms is pointwise equality.
Show Lean proof
by
apply DFunLike.ext d e
exact h@[simp]
theorem map_mul (d : CrossedHom action) (g h : G) :
d (g * h) = d g + action g (d h)The bundled Fox--Leibniz rule for a general additive action.
Show Lean proof
d.map_mul' g h@[simp]
theorem map_one (d : CrossedHom action) : d 1 = 0A crossed homomorphism vanishes at the identity.
Show Lean proof
by
have h := d.map_mul 1 1
have hmul : d 1 = d 1 + d 1 := by
simpa only [one_mul, action.map_one, toAdd_one, AddAut.zero_apply] using h
have h' := congrArg (fun z : A => z - d 1) hmul
have hzero : 0 = d 1 := by
simpa [sub_eq_add_neg, add_assoc, add_left_comm, add_comm] using h'
exact hzero.symmtheorem map_inv (d : CrossedHom action) (g : G) :
d g⁻¹ = -(action g⁻¹ (d g))Inverse rule for a crossed homomorphism.
Show Lean proof
by
have h := d.map_mul g⁻¹ g
rw [inv_mul_cancel, map_one] at h
rw [eq_neg_iff_add_eq_zero]
exact h.symmtheorem map_inv_mul (d : CrossedHom action) (g h : G) :
d (g⁻¹ * h) = -(action g⁻¹ (d g)) + action g⁻¹ (d h)Formula for multiplying by an inverse on the left.
Show Lean proof
by
rw [d.map_mul, d.map_inv]theorem map_mul_inv (d : CrossedHom action) (g h : G) :
d (g * h⁻¹) = d g - action (g * h⁻¹) (d h)Formula for multiplying by an inverse on the right.
Show Lean proof
by
rw [d.map_mul, d.map_inv]
simp only [map_neg, sub_eq_add_neg, ← AddAut.add_apply]
rw [← toAdd_mul, ← action.map_mul]theorem map_div (d : CrossedHom action) (g h : G) :
d (g / h) = d g - action (g / h) (d h)Division rule for a crossed homomorphism.
Show Lean proof
by
simpa [div_eq_mul_inv] using d.map_mul_inv g htheorem map_conj (d : CrossedHom action) (g h : G) :
d (g * h * g⁻¹) =
d g + action g (d h) - action (g * h * g⁻¹) (d g)Conjugation rule for a crossed homomorphism.
Show Lean proof
by
rw [d.map_mul_inv (g * h) g, d.map_mul g h]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)Commutator rule for a crossed homomorphism.
Show Lean proof
by
rw [commutatorElement_def, d.map_mul_inv (g * h * g⁻¹) h, d.map_conj g h]theorem map_pow (d : CrossedHom action) (g : G) (n : ℕ) :
d (g ^ n) = (Finset.range n).sum (fun k => action (g ^ k) (d g))Positive-power rule for a crossed homomorphism.
Show Lean proof
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 (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
· rflThe graph of a crossed homomorphism is an ordinary homomorphism into the standard semidirect product.
@[simp]
theorem toSemidirectMonoidHom_left (d : CrossedHom action) (g : G) :
Multiplicative.toAdd (d.toSemidirectMonoidHom g).left = d gThe left component of the semidirect-product graph is the value of the crossed homomorphism.
Show Lean proof
rfl@[simp]
theorem toSemidirectMonoidHom_right (d : CrossedHom action) (g : G) :
(d.toSemidirectMonoidHom g).right = gThe right component of the semidirect-product graph is the original group element.
Show Lean proof
rfldef 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 hleftAddRecover a crossed homomorphism from a semidirect-product homomorphism whose right component is the identity.
@[simp]
theorem ofSemidirectMonoidHom_apply
(f : G →* CrossedSemidirectProduct action)
(hright : ∀ g, (f g).right = g) (g : G) :
ofSemidirectMonoidHom f hright g = Multiplicative.toAdd (f g).leftRecovering a crossed homomorphism takes the additive form of the graph's left component.
Show Lean proof
rfl@[simp]
theorem ofSemidirectMonoidHom_toSemidirectMonoidHom (d : CrossedHom action) :
ofSemidirectMonoidHom d.toSemidirectMonoidHom
(fun g => toSemidirectMonoidHom_right d g) = dRecovering a crossed homomorphism from its semidirect-product graph returns the original map.
Show Lean proof
by
apply CrossedHom.ext
intro g
rfltheorem toSemidirectMonoidHom_ofSemidirectMonoidHom
(f : G →* CrossedSemidirectProduct action)
(hright : ∀ g, (f g).right = g) :
(ofSemidirectMonoidHom f hright).toSemidirectMonoidHom = fThe 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.
Show Lean proof
by
apply MonoidHom.ext
intro g
apply SemidirectProduct.ext
· rfl
· exact (hright g).symmdef 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)Pull back a crossed homomorphism along a group homomorphism.
@[simp]
theorem compMonoidHom_apply {K : Type*} [Group K]
(d : CrossedHom action) (φ : K →* G) (k : K) :
d.compMonoidHom φ k = d (φ k)Pullback along a group homomorphism evaluates by precomposition.
Show Lean proof
rfldef 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]Push a crossed homomorphism through an equivariant additive homomorphism.
@[simp]
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)Equivariant pushforward evaluates by applying the additive homomorphism to each value.
Show Lean proof
rfltheorem 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)Crossed homomorphisms agreeing on a set agree on the subgroup it generates.
Show Lean proof
by
intro g hg
exact Subgroup.closure_induction
(p := fun g _ => d g = e g)
(fun x hx => hs hx)
(by
rw [d.map_one, e.map_one])
(fun x y _ _ hx hy => by
rw [d.map_mul x y, e.map_mul x y, hx, hy])
(fun x _ hx => by
rw [d.map_inv x, e.map_inv x, hx]) hgtheorem eq_of_closure_eq_top (d e : CrossedHom action) {s : Set G}
(hsgen : Subgroup.closure s = ⊤) (hs : Set.EqOn d e s) : d = eCrossed homomorphisms are determined by their values on a generating set.
Show Lean proof
by
apply CrossedHom.ext
intro g
exact d.eqOn_closure e hs (by simp only [hsgen, Subgroup.coe_top, Set.mem_univ])instance instZero : Zero (CrossedHom action) where
zero := ⟨fun _ => 0, by intro g h; simp only [map_zero, add_zero]⟩The zero crossed homomorphism.
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⟩Pointwise addition of crossed homomorphisms.
@[simp]
theorem zero_apply (g : G) : (0 : CrossedHom action) g = 0The zero crossed homomorphism vanishes at every group element.
Show Lean proof
rfl@[simp]
theorem add_apply (d e : CrossedHom action) (g : G) : (d + e) g = d g + e gAddition of crossed homomorphisms is computed pointwise.
Show Lean proof
rflinstance instSMulNat : SMul ℕ (CrossedHom action) := ⟨nsmulRec⟩Natural-number scalar multiplication of crossed homomorphisms is repeated pointwise addition.
@[simp]
theorem nsmul_apply (n : ℕ) (d : CrossedHom action) (g : G) :
(n • d) g = n • d gNatural-number scalar multiplication of crossed homomorphisms is computed pointwise.
Show Lean proof
by
change (nsmulRec n d).toFun g = n • d g
induction n with
| zero => simp only [zero_nsmul]; rfl
| succ n ih =>
rw [nsmulRec, succ_nsmul]
change (nsmulRec n d).toFun g + d.toFun g = n • d.toFun g + d.toFun g
simpa only [toFun_apply] using congrArg (fun x : A => x + d.toFun g) ihinstance 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]⟩Negation of crossed homomorphisms is computed pointwise.
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⟩Subtraction of crossed homomorphisms is computed pointwise.
@[simp]
theorem neg_apply (d : CrossedHom action) (g : G) : (-d) g = -d gEvaluating a negated crossed homomorphism negates its value.
Show Lean proof
rfl@[simp]
theorem sub_apply (d e : CrossedHom action) (g : G) : (d - e) g = d g - e gEvaluating a difference of crossed homomorphisms subtracts their values.
Show Lean proof
rflinstance instSMulInt : SMul ℤ (CrossedHom action) :=
⟨zsmulRec (nsmul := nsmulRec)⟩Integer scalar multiplication of crossed homomorphisms is repeated pointwise addition or subtraction.
@[simp]
theorem zsmul_apply (z : ℤ) (d : CrossedHom action) (g : G) :
(z • d) g = z • d gInteger scalar multiplication of crossed homomorphisms is computed pointwise.
Show Lean proof
by
change (zsmulRec (nsmul := nsmulRec) z d).toFun g = z • d g
cases z with
| ofNat n => rw [zsmulRec]; change (n • d) g = (n : ℤ) • d g; rw [nsmul_apply, natCast_zsmul]
| negSucc n =>
rw [zsmulRec]
change (-(n.succ • d)) g = Int.negSucc n • d g
rw [neg_apply, nsmul_apply, negSucc_zsmul]instance instAddCommGroup : AddCommGroup (CrossedHom action) :=
Function.Injective.addCommGroup
(fun d : CrossedHom action => d.toFun)
(by intro d e h; exact CrossedHom.ext (congrFun h))
rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl)
(fun d n => by funext g; exact nsmul_apply n d g)
(fun d z => by funext g; exact zsmul_apply z d g)Pointwise operations make crossed homomorphisms an additive commutative group.
@[simp]
theorem map_mul (d : ScalarCrossedHom coeff A) (g h : G) :
d (g * h) = d g + coeff g • d hScalar crossed homomorphisms satisfy the scalar Fox--Leibniz product rule.
Show Lean proof
by
simpa only [scalarCrossedAction_apply] using CrossedHom.map_mul d g h@[simp]
theorem map_one (d : ScalarCrossedHom coeff A) : d 1 = 0A scalar crossed homomorphism vanishes at the identity.
Show Lean proof
CrossedHom.map_one dtheorem map_inv (d : ScalarCrossedHom coeff A) (g : G) :
d g⁻¹ = -(coeff g⁻¹ • d g)The value of a scalar crossed homomorphism at an inverse is the transported negative value.
Show Lean proof
by
simpa only [scalarCrossedAction_apply] using CrossedHom.map_inv d gtheorem map_inv_mul (d : ScalarCrossedHom coeff A) (g h : G) :
d (g⁻¹ * h) = -(coeff g⁻¹ • d g) + coeff g⁻¹ • d hFormula for a scalar crossed homomorphism on a product with an inverse on the left.
Show Lean proof
by
simpa only [scalarCrossedAction_apply] using CrossedHom.map_inv_mul d g htheorem map_mul_inv (d : ScalarCrossedHom coeff A) (g h : G) :
d (g * h⁻¹) = d g - coeff (g * h⁻¹) • d hFormula for a scalar crossed homomorphism on a product with an inverse on the right.
Show Lean proof
by
simpa only [scalarCrossedAction_apply] using CrossedHom.map_mul_inv d g htheorem map_div (d : ScalarCrossedHom coeff A) (g h : G) :
d (g / h) = d g - coeff (g / h) • d hThe scalar Fox rule written for group division.
Show Lean proof
by
simpa only [scalarCrossedAction_apply] using CrossedHom.map_div d g htheorem map_conj (d : ScalarCrossedHom coeff A) (g h : G) :
d (g * h * g⁻¹) = d g + coeff g • d h - coeff (g * h * g⁻¹) • d gThe scalar crossed-homomorphism formula for a conjugate.
Show Lean proof
by
simpa only [scalarCrossedAction_apply] using CrossedHom.map_conj d g htheorem 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 hThe scalar crossed-homomorphism formula for a commutator.
Show Lean proof
by
simpa only [scalarCrossedAction_apply] using CrossedHom.map_commutator d g htheorem map_pow (d : ScalarCrossedHom coeff A) (g : G) (n : ℕ) :
d (g ^ n) = (Finset.range n).sum (fun k => coeff (g ^ k) • d g)The value on a positive power is the sum of the translates of the value on its base.
Show Lean proof
by
simpa only [scalarCrossedAction_apply] using CrossedHom.map_pow d g ndef 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 hmulRestrict a scalar crossed homomorphism to a subgroup on which its coefficient is trivial.
@[simp]
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 gRestriction to a coefficient-trivial subgroup evaluates as the original crossed homomorphism.
Show Lean proof
rfldef mapLinear (d : ScalarCrossedHom coeff A) {B : Type*} [AddCommGroup B] [Module R B]
(f : A →ₗ[R] B) : ScalarCrossedHom coeff B :=
d.mapAddEquivariant (scalarCrossedAction (A := B) coeff) f.toAddMonoidHom
(by
intro g a
change f (coeff g • a) = coeff g • f a
exact f.map_smul (coeff g) a)A linear map is equivariant for scalar crossed actions and hence maps scalar crossed homomorphisms to scalar crossed homomorphisms.
@[simp]
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)Linear pushforward evaluates by applying the linear map to each crossed-homomorphism value.
Show Lean proof
rfldef 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)Pull back a scalar crossed homomorphism while retaining its scalar specialization.
@[simp]
theorem compMonoidHom_apply {K : Type*} [Group K]
(d : ScalarCrossedHom coeff A) (φ : K →* G) (k : K) :
d.compMonoidHom φ k = d (φ k)Pullback of a scalar crossed homomorphism evaluates by precomposition.
Show Lean proof
rfl