OnePlusIndex110.lean

1 import Mathlib.GroupTheory.Index
2 import Mathlib.RingTheory.Ideal.Basic
3 import Mathlib.Logic.Equiv.Defs
4 import Mathlib.Tactic.NoncommRing
5 
6 /-! Exact multiplicative/additive coset comparison. The named unit subgroup K
7 must really consist of all units 1+x for x in L. This does not pretend that
8 an arbitrary full lattice contained in a radical automatically is a group. -/
9 set_option autoImplicit false
10 noncomputable section
11 namespace PaperXI.OnePlusIndex110
12 
13 variable {R : Type*} [Ring R]
14 
15 def congruence (I : Ideal R) (K : Subgroup Rˣ) : Subgroup K where
16   carrier := {g | ((g : Rˣ) : R) - 1 ∈ I}
17   one_mem' := by simp
18   mul_mem' := by
19     intro a b ha hb
20     change (((a : Rˣ) : R) * ((b : Rˣ) : R)) - 1 ∈ I
21     have he : (((a : Rˣ) : R) * ((b : Rˣ) : R)) - 1 =
22         ((a : Rˣ) : R) * (((b : Rˣ) : R) - 1) + (((a : Rˣ) : R) - 1) := by noncomm_ring
23     rw [he]
24     exact I.add_mem (I.mul_mem_left _ hb) ha
25   inv_mem' := by
26     intro a ha
27     change (((a : Rˣ)⁻¹ : Rˣ) : R) - 1 ∈ I
28     have he : (((a : Rˣ)⁻¹ : Rˣ) : R) - 1 =
29         -((((a : Rˣ)⁻¹ : Rˣ) : R) * (((a : Rˣ) : R) - 1)) := by
30       rw [mul_sub, Units.inv_mul, mul_one]
31       abel
32     rw [he]
33     exact I.neg_mem (I.mul_mem_left _ ha)
34 
35 def offsetEquiv (L : AddSubgroup R) (K : Subgroup Rˣ)
36     (hK : ∀ g : K, ((g : Rˣ) : R) - 1 ∈ L)
37     (hL : ∀ x : L, ∃ g : K, ((g : Rˣ) : R) = 1 + (x : R)) : K ≃ L :=
38   Equiv.ofBijective (fun g => ⟨((g : Rˣ) : R) - 1, hK g⟩) (by
39     constructor
40     · intro a b hab
41       apply Subtype.ext
42       apply Units.ext
43       have he := congrArg (fun x : L => (x : R)) hab
44       exact sub_left_injective he
45     · intro x
46       obtain ⟨g, hg⟩ := hL x
47       refine ⟨g, Subtype.ext ?_⟩
48       change ((g : Rˣ) : R) - 1 = (x : R)
49       rw [hg]
50       abel)
51 
52 theorem inv_mul_sub_one_mem_iff (I : Ideal R) (a b : Rˣ) :
53     (((a⁻¹ * b : Rˣ) : R) - 1 ∈ I) ↔ ((b : R) - (a : R) ∈ I) := by
54   have hleft : ((a⁻¹ * b : Rˣ) : R) - 1 = (↑a⁻¹ : R) * ((b : R) - (a : R)) := by
55     rw [mul_sub, Units.inv_mul]
56     rfl
57   have hright : (b : R) - (a : R) = (a : R) * (((a⁻¹ * b : Rˣ) : R) - 1) := by
58     rw [mul_sub, Units.val_mul, ← mul_assoc, Units.mul_inv, one_mul, mul_one]
59   constructor
60   · intro h
61     rw [hright]
62     exact I.mul_mem_left _ h
63   · intro h
64     rw [hleft]
65     exact I.mul_mem_left _ h
66 
67 def cosetEquiv (I : Ideal R) (L : AddSubgroup R) (K : Subgroup Rˣ)
68     (hK : ∀ g : K, ((g : Rˣ) : R) - 1 ∈ L)
69     (hL : ∀ x : L, ∃ g : K, ((g : Rˣ) : R) = 1 + (x : R)) :
70     (K ⧸ congruence I K) ≃ (L ⧸ I.toAddSubgroup.addSubgroupOf L) :=
71   Quotient.congr (offsetEquiv L K hK hL) (by
72     intro a b
73     rw [QuotientGroup.leftRel_apply, QuotientAddGroup.leftRel_apply]
74     change (((((a : Rˣ)⁻¹) * (b : Rˣ)) : R) - 1 ∈ I) ↔
75       (-(((a : Rˣ) : R) - 1) + (((b : Rˣ) : R) - 1) ∈ I)
76     have he : -(((a : Rˣ) : R) - 1) + (((b : Rˣ) : R) - 1) =
77         ((b : Rˣ) : R) - ((a : Rˣ) : R) := by abel
78     rw [he]
79     exact inv_mul_sub_one_mem_iff I (a : Rˣ) (b : Rˣ))
80 
81 theorem index_eq_additive_relIndex (I : Ideal R) (L : AddSubgroup R) (K : Subgroup Rˣ)
82     (hK : ∀ g : K, ((g : Rˣ) : R) - 1 ∈ L)
83     (hL : ∀ x : L, ∃ g : K, ((g : Rˣ) : R) = 1 + (x : R)) :
84     (congruence I K).index = I.toAddSubgroup.relIndex L :=
85   Nat.card_congr (cosetEquiv I L K hK hL)
86 
87 end PaperXI.OnePlusIndex110

Back to source controls