English
IsApproximateSubgroup 1 A is equivalent to A being a subgroup.
Русский
IsApproximateSubgroup 1 A эквивалентно тому, что A является подпгруппой.
LaTeX
$$$\\IsApproximateSubgroup 1 \\; A \\iff \\exists H: Subgroup G, H = (A).$$$
Lean4
/-- A `1`-approximate subgroup is the same thing as a subgroup. -/
@[to_additive (attr := simp) /-- A `1`-approximate subgroup is the same thing as a subgroup. -/
]
theorem isApproximateSubgroup_one {A : Set G} : IsApproximateSubgroup 1 (A : Set G) ↔ ∃ H : Subgroup G, H = A
where
mp
hA :=
by
suffices A * A ⊆ A from
let H : Subgroup G :=
{ carrier := A
one_mem' := hA.one_mem
inv_mem' hx := by rwa [← hA.inv_eq_self, inv_mem_inv]
mul_mem' hx hy := this (mul_mem_mul hx hy) }
⟨H, rfl⟩
obtain ⟨x, hx⟩ : ∃ x : G, A * A ⊆ x • A :=
by
obtain ⟨K, hK, hKA⟩ := hA.sq_covBySMul
simp only [Nat.cast_le_one, Finset.card_le_one_iff_subset_singleton, Finset.subset_singleton_iff] at hK
obtain ⟨x, rfl | rfl⟩ := hK
· simp [hA.nonempty.ne_empty] at hKA
· rw [Finset.coe_singleton, singleton_smul, sq] at hKA
use x
have hx' : x⁻¹ • (A * A) ⊆ A := by rwa [← subset_smul_set_iff]
have hx_inv : x⁻¹ ∈ A := by simpa using hx' (smul_mem_smul_set (mul_mem_mul hA.one_mem hA.one_mem))
have hx_sq : x * x ∈ A := by
rw [← hA.inv_eq_self]
simpa using hx' (smul_mem_smul_set (mul_mem_mul hx_inv hA.one_mem))
calc
A * A ⊆ x • A := by assumption
_ = x⁻¹ • (x * x) • A := by simp [smul_smul]
_ ⊆ x⁻¹ • (A • A) := (smul_set_mono (smul_set_subset_smul hx_sq))
_ ⊆ A := hx'
mpr := by rintro ⟨H, rfl⟩; exact .subgroup
