English
If a finite index family of subgroups K_i is independent (iSupIndep) and elements f_i lie in K_i, then the finite noncommProd equals 1 implies each f_i = 1.
Русский
Если семейство подгрупп K_i взаимно независимо и элементы f_i лежат в K_i, то равенство непроизвольной неперсуперпродукции к единице влечёт, что каждый f_i равен 1.
LaTeX
$$$\\forall i \\in s,\\ f_i = 1$ from $s.noncommProd f comm = 1$ under iSupIndep K.$$
Lean4
/-- `Finset.noncommProd` is “injective” in `f` if `f` maps into independent subgroups. This
generalizes (one direction of) `Subgroup.disjoint_iff_mul_eq_one`. -/
@[to_additive /-- `Finset.noncommSum` is “injective” in `f` if `f` maps into independent subgroups.
This generalizes (one direction of) `AddSubgroup.disjoint_iff_add_eq_zero`. -/
]
theorem eq_one_of_noncommProd_eq_one_of_iSupIndep {ι : Type*} (s : Finset ι) (f : ι → G) (comm) (K : ι → Subgroup G)
(hind : iSupIndep K) (hmem : ∀ x ∈ s, f x ∈ K x) (heq1 : s.noncommProd f comm = 1) : ∀ i ∈ s, f i = 1 := by
classical
revert heq1
induction s using Finset.induction_on with
| empty => simp
| insert i s hnotMem
ih =>
have hcomm := comm.mono (Finset.coe_subset.2 <| Finset.subset_insert _ _)
simp only [Finset.forall_mem_insert] at hmem
have hmem_bsupr : s.noncommProd f hcomm ∈ ⨆ i ∈ (s : Set ι), K i :=
by
refine Subgroup.noncommProd_mem _ _ ?_
intro x hx
have : K x ≤ ⨆ i ∈ (s : Set ι), K i := le_iSup₂ (f := fun i _ => K i) x hx
exact this (hmem.2 x hx)
intro heq1
rw [Finset.noncommProd_insert_of_notMem _ _ _ _ hnotMem] at heq1
have hnotMem' : i ∉ (s : Set ι) := by simpa
obtain ⟨heq1i : f i = 1, heq1S : s.noncommProd f _ = 1⟩ :=
Subgroup.disjoint_iff_mul_eq_one.mp (hind.disjoint_biSup hnotMem') hmem.1 hmem_bsupr heq1
intro i h
simp only [Finset.mem_insert] at h
rcases h with (rfl | h)
· exact heq1i
· refine ih hcomm hmem.2 heq1S _ h
