Systems of units

This file develops linearly independent systems of units in cyclotomic modules.

structure systemOfUnits (p : ℕ) (G : Type u_1) [AddCommGroup G] [Module (CyclotomicIntegers p) G] (s : ℕ) : Type u_1

A system of s units represented by a linearly independent family over cyclotomic integers.

• units : Fin s → G

  The family of units in the system.

• linearIndependent : LinearIndependent (CyclotomicIntegers p) self.units

  The linear independence of the family over cyclotomic integers.

theorem systemOfUnits.existence0 (p : ℕ) (G : Type u_1) [AddCommGroup G] [Module (CyclotomicIntegers p) G] : Nonempty (systemOfUnits p G 0)

theorem systemOfUnits.finrank_spanA (p : ℕ) (hp : Nat.Prime p) (G : Type u_1) [AddCommGroup G] [Module (CyclotomicIntegers p) G] {R : ℕ} (f : Fin R → G) (hf : LinearIndependent (CyclotomicIntegers p) f) : Module.finrank ℤ ↥(Submodule.span (CyclotomicIntegers p) (Set.range f)) = (p - 1) * R

theorem systemOfUnits.ex_not_mem (p : ℕ) (hp : Nat.Prime p) (G : Type u_1) [AddCommGroup G] (s : ℕ) (hf : Module.finrank ℤ G = s * (p - 1)) [Module (CyclotomicIntegers p) G] [Module.Free ℤ G] {R : ℕ} (S : systemOfUnits p G R) (hR : R < s) : ∃ (g : G), ∀ (k : ℤ), k ≠ 0 → k • g ∉ Submodule.span (CyclotomicIntegers p) (Set.range S.units)

theorem systemOfUnits.existence' (p : ℕ) (hp : Nat.Prime p) (G : Type u_1) [AddCommGroup G] (s : ℕ) (hf : Module.finrank ℤ G = s * (p - 1)) [Module.Free ℤ G] [Module (CyclotomicIntegers p) G] {R : ℕ} (S : systemOfUnits p G R) (hR : R < s) : Nonempty (systemOfUnits p G (R + 1))

theorem systemOfUnits.existence'' (p : ℕ) (hp : Nat.Prime p) (G : Type u_1) [AddCommGroup G] (s : ℕ) (hf : Module.finrank ℤ G = s * (p - 1)) [Module.Free ℤ G] [Module (CyclotomicIntegers p) G] {R : ℕ} (hR : R ≤ s) : Nonempty (systemOfUnits p G R)

theorem systemOfUnits.existence (p : ℕ) (hp : Nat.Prime p) (G : Type u_1) [AddCommGroup G] (s : ℕ) (hf : Module.finrank ℤ G = s * (p - 1)) [Module.Free ℤ G] [Module (CyclotomicIntegers p) G] : Nonempty (systemOfUnits p G s)