English
The 0-th iterated wreath product equals the singleton PUnit: IteratedWreathProduct G 0 = PUnit.
Русский
0-е итерированное вентовое произведение равно одиночному PUnit: IteratedWreathProduct G 0 = PUnit.
LaTeX
$$$ IteratedWreathProduct(G,0) = PUnit $$$
Lean4
theorem closure_mul_image_mul_eq_top (hR : IsComplement H R) (hR1 : (1 : G) ∈ R) (hS : closure S = ⊤) :
(closure ((R * S).image fun g => g * (hR.toRightFun g : G)⁻¹)) * R = ⊤ :=
by
let f : G → R := hR.toRightFun
let U : Set G := (R * S).image fun g => g * (f g : G)⁻¹
change (closure U : Set G) * R = ⊤
refine top_le_iff.mp fun g _ => ?_
refine closure_induction_right ?_ ?_ ?_ (eq_top_iff.mp hS (mem_top g))
· exact ⟨1, (closure U).one_mem, 1, hR1, one_mul 1⟩
· rintro - - s hs ⟨u, hu, r, hr, rfl⟩
rw [show u * r * s = u * (r * s * (f (r * s) : G)⁻¹) * f (r * s) by group]
refine Set.mul_mem_mul ((closure U).mul_mem hu ?_) (f (r * s)).coe_prop
exact subset_closure ⟨r * s, Set.mul_mem_mul hr hs, rfl⟩
· rintro - - s hs ⟨u, hu, r, hr, rfl⟩
rw [show u * r * s⁻¹ = u * (f (r * s⁻¹) * s * r⁻¹)⁻¹ * f (r * s⁻¹) by group]
refine Set.mul_mem_mul ((closure U).mul_mem hu ((closure U).inv_mem ?_)) (f (r * s⁻¹)).2
refine subset_closure ⟨f (r * s⁻¹) * s, Set.mul_mem_mul (f (r * s⁻¹)).2 hs, ?_⟩
rw [mul_right_inj, inv_inj, ← Subtype.coe_mk r hr, ← Subtype.ext_iff, Subtype.coe_mk]
apply
(isComplement_iff_existsUnique_mul_inv_mem.mp hR (f (r * s⁻¹) * s)).unique
(hR.mul_inv_toRightFun_mem (f (r * s⁻¹) * s))
rw [mul_assoc, ← inv_inv s, ← mul_inv_rev, inv_inv]
exact hR.toRightFun_mul_inv_mem (r * s⁻¹)
