English
There is a MulAction instance on the left transversal by F acting on G, compatible with the quotient structure.
Русский
Существует действие по умножению на левый трансверсал, совместимое с фактор-группой.
LaTeX
$$MulAction F H.LeftTransversal with smul defined componentwise via representatives.$$
Lean4
@[to_additive]
noncomputable instance : MulAction F H.LeftTransversal
where
smul f
T :=
⟨f • (T : Set G), by
refine isComplement_iff_existsUnique_inv_mul_mem.mpr fun g => ?_
obtain ⟨t, ht1, ht2⟩ := isComplement_iff_existsUnique_inv_mul_mem.mp T.2 (f⁻¹ • g)
refine ⟨⟨f • (t : G), Set.smul_mem_smul_set t.2⟩, ?_, ?_⟩
· exact smul_inv_smul f g ▸ QuotientAction.inv_mul_mem f ht1
· rintro ⟨-, t', ht', rfl⟩ h
replace h := QuotientAction.inv_mul_mem f⁻¹ h
simp only [Subtype.ext_iff, smul_left_cancel_iff, inv_smul_smul] at h ⊢
exact Subtype.ext_iff.mp (ht2 ⟨t', ht'⟩ h)⟩
one_smul T := Subtype.ext (one_smul F (T : Set G))
mul_smul f₁ f₂ T := Subtype.ext (mul_smul f₁ f₂ (T : Set G))
