Grace/Cumulus/Algebra/Group/Pow.g17

Open in Workbench Download source

Imports

Subgroup · Power

Declarations

• groupPow def
• groupPow.value theorem derivation
• pow_zero theorem derivation
• pow_succ_left theorem derivation
• pow_succ theorem derivation
• pow_one theorem derivation
• Group.pow_mem instance derivation
• pow_add theorem derivation
• pow_mul theorem derivation
• one_pow theorem derivation
• pow_mul_comm theorem derivation
• pow_mul_self_comm theorem derivation
• inv_pow theorem derivation
• pow_eq_inv_pow_of_pow_add theorem derivation
• Subgroup.pow_mem instance derivation

Source

1-- Natural powers in a bundled group, written x ^ n: the recursion laws,2-- additivity and multiplicativity of exponents, powers of the unit and of3-- inverses, and closure of subgroups under powers4-- Part of Cumulus, the Grace17 mathematics library.5-- Copyright (c) 2026 Grant Passmore.6-- Released under the Apache License 2.0. See LICENSE in the repository root.7-- Authors: Grant Passmore89module Grace.Cumulus.Algebra.Group.Pow10import Subgroup11import Power1213-- The n-th power of x in G, the monoid power under the operation and unit14-- of G; written x ^ n wherever a hypothesis supplies the group.15def groupPow (G x : Set, n : Nat) : Set := monoidPow(G.mul, G.one, x, n)1617notation infixr 80 "^" => groupPow(G, _, _) via hypothesis Group(G) for G.carrier18notation infixr 80 "^" => groupPow(G, _, _) via hypothesis AbelianGroup(G) for G.carrier19notation infixr 80 "^" => groupPow(G, _, _) via hypothesis Subgroup(H, G) for H2021theorem groupPow.value (G x : Set, n : Nat)22  shows groupPow(G, x, n) = monoidPow(G.mul, G.one, x, n)23proof24  simp [groupPow]2526section PowerLaws27variable (G : Set)28hypothesis group : Group(G)2930theorem pow_zero (x : G)31  shows x ^ 0 = G.one32proof33  simp [groupPow, monoidPow.zero]3435theorem pow_succ_left (x : G) (n : Nat)36  shows x ^ (n + 1) = x * x ^ n37proof38  have monoid := IsGroup.monoid with (Group.parts with group)39  have step := monoidPow.succ_left at G.carrier, G.mul, G.one, x, n with monoid, *40  simp [groupPow, step]4142theorem pow_succ (x : G) (n : Nat)43  shows x ^ (n + 1) = x ^ n * x44proof45  have monoid := IsGroup.monoid with (Group.parts with group)46  have step := monoidPow.succ_right at G.carrier, G.mul, G.one, x, n with monoid, *47  simp [groupPow, step]4849theorem pow_one (x : G)50  shows x ^ 1 = x51proof52  have monoid := IsGroup.monoid with (Group.parts with group)53  have one := monoidPow.one with monoid, *54  simp [groupPow, one]5556instance Group.pow_mem (x : G) (n : Nat)57  shows x ^ n ∈ G58proof59  have monoid := IsGroup.monoid with (Group.parts with group)60  have closed := monoidPow.closed at G.carrier, G.mul, G.one, x, n with monoid, *61  simp [groupPow, closed]6263theorem pow_add (x : G) (m n : Nat)64  shows x ^ (m + n) = x ^ m * x ^ n65proof66  have monoid := IsGroup.monoid with (Group.parts with group)67  have split := monoidPow.add at G.carrier, G.mul, G.one, x, m, n with monoid, *68  simp [groupPow, split]6970theorem pow_mul (x : G) (m n : Nat)71  shows x ^ (m * n) = (x ^ m) ^ n72proof73  have monoid := IsGroup.monoid with (Group.parts with group)74  have split := monoidPow.mul at G.carrier, G.mul, G.one, x, m, n with monoid, *75  simp [groupPow, split]7677theorem one_pow (n : Nat)78  shows G.one ^ n = G.one79proof80  have monoid := IsGroup.monoid with (Group.parts with group)81  have power := monoidPow.unit at G.carrier, G.mul, G.one, n with monoid82  simp [groupPow, power]8384theorem pow_mul_comm (x : G) (m n : Nat)85  shows x ^ m * x ^ n = x ^ n * x ^ m86proof87  have monoid := IsGroup.monoid with (Group.parts with group)88  have swap := monoidPow.add_commute at G.carrier, G.mul, G.one, x, m, n with monoid, *89  simp [groupPow, swap]9091theorem pow_mul_self_comm (x : G) (n : Nat)92  shows x * x ^ n = x ^ n * x93proof94  have monoid := IsGroup.monoid with (Group.parts with group)95  have swap := monoidPow.commute at G.carrier, G.mul, G.one, x, n with monoid, *96  simp [groupPow, swap]9798theorem inv_pow (x : G) (n : Nat)99  shows x⁻¹ ^ n = (x ^ n)⁻¹100proof101  induction n102  | zero =>103    rw [pow_zero, pow_zero, inv_one]104    rfl105  | succ(k) using ih =>106    have step : x⁻¹ ^ (k + 1) = x⁻¹ ^ k * x⁻¹ := pow_succ with *107    have stepX : x ^ (k + 1) = x * x ^ k := pow_succ_left with *108    rw [← add.right_one, step, stepX, ih, mul_inv_rev]109    rfl110111-- The power that completes a vanishing product is the inverse power.112theorem pow_eq_inv_pow_of_pow_add (x : G) (m n : Nat)113  requires vanishes : x ^ (m + n) = G.one114  shows x ^ n = (x ^ m)⁻¹115proof116  have split : x ^ (m + n) = x ^ m * x ^ n := pow_add with *117  have product : x ^ m * x ^ n = G.one by cc118  exact eq_inv_of_mul_eq_one_right with *119120end PowerLaws121122section SubgroupPowers123variable (G H : Set)124hypothesis subgroup : Subgroup(H, G)125126instance Subgroup.pow_mem (h : H) (n : Nat)127  shows h ^ n ∈ H128proof129  have group := Subgroup.group with subgroup130  induction n131  | zero =>132    have zero : h ^ 0 = G.one := pow_zero with *133    rw zero134    exact Subgroup.one_mem with *135  | succ(k) using ih =>136    have step : h ^ (k + 1) = h ^ k * h := pow_succ with *137    rw [← add.right_one, step]138    exact Subgroup.mul_mem with *139140end SubgroupPowers141