Built with
doc-gen4 , running Lean4.
Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents.
Use
Ctrl+β Ctrl+β to navigate,
Ctrl+π±οΈ to focus.
On Mac, use
Cmd instead of
Ctrl .
import UnitConjecture.GardamGroup
import Mathlib.Algebra.GroupPower.Basic
/-!
## Torsion-freeness of `P`
This file contains a proof that the group `P` defined is in fact torsion-free.
Roughly, the steps are as follows (further details can be found in the corresponding `.md` file):
1. Define a function `sq : P -> K` taking a group element `(q, k)` to its square. This element lies in the kernel as the group `β€/2 Γ β€/2` has exponent `2`.
2. Show that elements in `K`, which are integer triples of the form `(a, b, c)`, do not have torsion. This requires the fact that the group `β€`, and hence `β€Β³`, is torsion-free.
3. Show that no element of `P` has order precisely `2`. This is an argument by cases on the `Q` part of a general element of `P`.
4. Finally, show that if an element `g : G` of a group `G` satisfies `g ^ n = (1 : G)`, then it also satisfies `(g ^ 2) ^ n = (1 : G)`.
5. Together, these statements show that `P` is torsion-free.
-/
section TorsionFree
/-!
### Torsion-free groups
-/
/-- The definition of a torsion-free group. -/
class TorsionFree ( G : Type _ ) [ Group G ] where
/-- A group is *torsion-free* if the only element with non-trivial torsion is the identity element. -/
torsionFree : β g : G , β n : β , g ^ n . succ = 1 β g = 1
/-- The definition of torsion-free additive groups. -/
class AddTorsionFree ( A : Type _ ) [ AddGroup A ] where
/-- An additive group is *torsion-free* if the only element with non-trivial torsion is the identity element. -/
torsionFree : β a : A , β n : β , n . succ β’ a = 0 β a = 0
/-- β€ is torsion-free, since it is an integral domain. -/
instance : AddTorsionFree β€ where
torsionFree := by
intro a n ( h : n . succ * a = 0 )
cases Int.mul_eq_zero . mp : β {a b : Prop }, (a β b a β b h with
| inl : β {a b : Prop }, a β a β¨ b hyp => injection hyp ; contradiction
| inr : β {a b : Prop }, b β a β¨ b _ => assumption
/-- The product of torsion-free additive groups is torsion-free. -/
instance { A B : Type _ } [ AddGroup A ] [ AddGroup B ] [ AddTorsionFree A ] [ AddTorsionFree B ] : AddTorsionFree ( A Γ B ) where
torsionFree := by
intro ( a , b ) n
rw [ show n . succ β’ ( a , b ) = ( n . succ β’ a , n . succ β’ b ) from rfl : β {Ξ± : Sort ?u.7161} {a : Ξ± }, a = a , Prod.ext_iff : β {Ξ± : Type ?u.7197} {Ξ² : Type ?u.7198} {p q : Ξ± Γ Ξ² p = q β p .fst= q .fstβ§ p .snd= q .snd , Prod.ext_iff : β {Ξ± : Type ?u.7223} {Ξ² : Type ?u.7224} {p q : Ξ± Γ Ξ² p = q β p .fst= q .fstβ§ p .snd= q .snd ]
intro β¨_, _β© (a , b ) .fst= 0 .fstβ§ (a , b ) .snd= 0 .snd; (a , b ) .fst= 0 .fstβ§ (a , b ) .snd= 0 .snd refine' β¨ _ , _ β© (a , b ) .fst= 0 .fstβ§ (a , b ) .snd= 0 .snd<;>
(a , b ) .fst= 0 .fst⧠(a , b ) .snd= 0 .snd( apply AddTorsionFree.torsionFree ; assumption )
end TorsionFree
/-! ### **Step 1:** Defining the square of an element of `P`. -/
/-- The function taking an element of `P` to its square, which lies in the kernel `K`. -/
@[ aesop norm unfold ( rule_sets [P]), reducible]
def P.sq : P β K
| (( p , q , r ), .e ) => ( p + p , q + q , r + r )
| ((_, q , _), .b ) => ( 0 , q + q + 1 , 0 )
| (( p , _, _), .a ) => ( p + p + 1 , 0 , 0 )
| ((_, _, r ), .c ) => ( 0 , 0 , r + r + 1 )
open P
/-- A proof that the function `sq` indeed takes an element of `P` to its square in `K`. -/
@[ aesop norm apply ( rule_sets [P]), simp ]
theorem sq_square : β g : P , g * g = ( P.sq g , .e )
| (( p , q , r ), x ) =>
match x with
| .e | .a | .b | .c => by
((p , q , r ) , Q.b ) * ((p , q , r ) , Q.b ) = (P.sq ((p , q , r ) , Q.b ) Q.e ) aesop ( rule_sets [P])
/-! ### **Step 2:** Proving that `K` (= `β€Β³`) is torsion-free. -/
/-- The kernel `β€Β³` is torsion-free. -/
instance K.torsionFree : AddTorsionFree K := inferInstance : {Ξ± : Sort ?u.213891} β [i : Ξ± ] β Ξ±
/-! ### **Step 3:** Showing that no element of `P` has order precisely two. -/
namespace Int
/-! Some basic lemmas about integers needed to prove facts about `P`. -/
lemma add_twice_eq_mul_two : β {a : β€ }, a + a = a * 2 add_twice_eq_mul_two { a : β€ } : a + a = a * 2 := by
rw [ show 2 = 1 + 1 by rfl , mul_add , mul_one ]
attribute [ local simp ] add_twice_eq_mul_two : β {a : β€ }, a + a = a * 2
/-- No odd integer is zero. -/
lemma odd_ne_zero : β (a : β€ ), Β¬ a + a + 1 = 0 odd_ne_zero : β a : β€ , Β¬( a + a + 1 = 0 ) := by
intro a h
have : ( a + a + 1 ) % 2 = 0 % 2 := congrArg : β {Ξ± : Sort ?u.215087} {Ξ² : Sort ?u.215086} {aβ aβ : Ξ± } (f : Ξ± β Ξ² aβ = aβ f aβ = f aβ (Β· % 2) h
simp [ Int.add_emod : β (a b n : β€ ), (a + b % n = (a % n + b % n % n ] at this : (a + a + 1 % 2 = 0 % 2 this
/-- If the sum of an integer with itself is zero, then the integer is itself zero. -/
lemma zero_of_twice_zero : β (a : β€ ), a + a = 0 a = 0 zero_of_twice_zero : β a : β€ , a + a = 0 β a = 0 := by
β (a : β€ ), a + a = 0 a = 0 simp
end Int
/-- The only element of `P` with order dividing `2` is the identity. -/
theorem square_free : β {g : P }, g * g = 1 g = 1 square_free : β { g : P }, g * g = ( 1 : P ) β g = ( 1 : P )
| (( p , q , r ), x ) => by
((p , q , r ) , x ) * ((p , q , r ) , x ) = 1 ((p , q , r ) , x ) = 1 match x with
((p , q , r ) , x ) * ((p , q , r ) , x ) = 1 ((p , q , r ) , x ) = 1 | .e => ((p , q , r ) , Q.e ) * ((p , q , r ) , Q.e ) = 1 ((p , q , r ) , Q.e ) = 1 ((p , q , r ) , x ) * ((p , q , r ) , x ) = 1 ((p , q , r ) , x ) = 1 aesop ( rule_sets [P]) ( add norm [Int.zero_of_twice_zero])
((p , q , r ) , x ) * ((p , q , r ) , x ) = 1 ((p , q , r ) , x ) = 1 | .a | .b | .c => ((p , q , r ) , Q.a ) * ((p , q , r ) , Q.a ) = 1 ((p , q , r ) , Q.a ) = 1 ((p , q , r ) , x ) * ((p , q , r ) , x ) = 1 ((p , q , r ) , x ) = 1 aesop ( rule_sets [P]) ( add norm [Int.odd_ne_zero])
/-! ### **Step 4:** Showing that if the `n`-th power of a group element is trivial, then so is that of its square. -/
/-- If `g` is a torsion element of a group, then so is `g ^ 2`. -/
lemma torsion_implies_square_torsion : β {G : Type u_1} [inst : Group G g : G ) (n : β ), g ^ n = 1 (g ^ 2 ^ n = 1 torsion_implies_square_torsion { G : Type _ : Type (?u.440141+1)} [ Group : Type ?u.440144 β Type ?u.440144 G ] ( g : G ) ( n : β ) ( g_tor : g ^ n = 1 ) : ( g ^ 2 ) ^ n = 1 :=
calc ( g ^ 2 ) ^ n = g ^ ( 2 * n ) := by (g ^ 2 ^ n = g ^ (2 * n rw [ (g ^ 2 ^ n = g ^ (2 * n β pow_mul : β {M : Type ?u.458456} [inst : Monoid M a : M ) (m n : β ), a ^ (m * n = (a ^ m ^ n g ^ (2 * n = g ^ (2 * n ]
_ = g ^ ( n * 2 ) := by g ^ (2 * n = g ^ (n * 2 rw [ g ^ (2 * n = g ^ (n * 2 mul_comm g ^ (n * 2 = g ^ (n * 2 ]
_ = ( g ^ n ) ^ 2 := by g ^ (n * 2 = (g ^ n ^ 2 rw [ g ^ (n * 2 = (g ^ n ^ 2 pow_mul : β {M : Type ?u.458753} [inst : Monoid M a : M ) (m n : β ), a ^ (m * n = (a ^ m ^ n (g ^ n ^ 2 = (g ^ n ^ 2 ]
_ = ( 1 : G ) ^ 2 := by rw [ β g_tor (g ^ n ^ 2 = (g ^ n ^ 2 ]
_ = ( 1 : G ) := by rw [ one_pow ]
/-! ### **Step 5:** Putting the facts together. -/
/-- `P` is torsion-free. -/
instance P.torsionFree : TorsionFree P where
torsionFree := by
intros g n g_tor -- assume `g` is a torsion element
-- then `g ^ 2` is also a torsion element
have square_tor : ( g ^ 2 ) ^ n . succ = (( 0 , 0 , 0 ), Q.e ) := torsion_implies_square_torsion : β {G : Type ?u.462165} [inst : Group G g : G ) (n : β ), g ^ n = 1 (g ^ 2 ^ n = 1 g n . succ g_tor
erw [ pow_two : β {M : Type ?u.462608} [inst : Monoid M a : M ), a ^ 2 = a * a , sq_square : β (g : P ), g * g = (sq g Q.e ) , MetabelianGroup.kernel_pow , Prod.mk.injEq : β {Ξ± : Type ?u.468262} {Ξ² : Type ?u.468261} (fst : Ξ± ) (snd : Ξ² ) (fst_1 : Ξ± ) (snd_1 : Ξ² ),
((fst , snd ) = (fst_1 , snd_1 ) = (fst = fst_1 β§ snd = snd_1 ] at square_tor
-- since `g ^ 2 = s g`, we have that `s g` is a torsion element
have s_tor : n . succ β’ ( sq g ) = 0 := square_tor . left : β {a b : Prop }, a β§ b a
-- since `s g` lies in the kernel and the kernel is torsion-free, `s g = 0`
have square_zero : ( sq g , Q.e ) = ( 0 , Q.e ) := congrArg : β {Ξ± : Sort ?u.468529} {Ξ² : Sort ?u.468528} {aβ aβ : Ξ± } (f : Ξ± β Ξ² aβ = aβ f aβ = f aβ (Β·, Q.e ) ( K.torsionFree . torsionFree ( sq g ) n s_tor )
rw [ β sq_square : β (g : P ), g * g = (sq g Q.e ) ] at square_zero
-- this means `g ^ 2 = e`, and also `g = e` because `P` has no order 2 elements
exact square_free : β {g : P }, g * g = 1 g = 1 square_zero : g * g = (0 , Q.e ) square_zero