English
Given an equivalence e: G1 ≃ G2 between Klein four structures with e(1) = 1 and with G2 of exponent 2, there exists a multiplicative equivalence G1 ≃* G2.
Русский
С учётом эквивалентности e между двумя группами Klein Four с e(1)=1 и pодпорядком G2 равной 2, существует мультипликативное эквивалентное отображение G1 ≃* G2.
LaTeX
$$e: G1 ≃ G2,\; e(1)=1,\; \operatorname{exponent}(G2)=2 \Rightarrow G1 \simeq_{\mathrm{Mul}} G2$$
Lean4
/-- An equivalence between an `IsKleinFour` group `G₁` and a group `G₂` of exponent two which sends
`1 : G₁` to `1 : G₂` is in fact an isomorphism. -/
@[to_additive /-- An equivalence between an `IsAddKleinFour` group `G₁` and a group `G₂` of exponent
two which sends `0 : G₁` to `0 : G₂` is in fact an isomorphism. -/
]
def mulEquiv' (e : G₁ ≃ G₂) (he : e 1 = 1) (h : Monoid.exponent G₂ = 2) : G₁ ≃* G₂
where
toEquiv := e
map_mul' := by
let _inst₁ := Fintype.ofFinite G₁
let _inst₂ := Fintype.ofEquiv G₁ e
intro x y
by_cases hx : x = 1 <;> by_cases hy : y = 1
all_goals try simp only [hx, hy, mul_one, one_mul, Equiv.toFun_as_coe, he]
by_cases hxy : x = y
· simp [hxy, mul_self, ← pow_two (e y), h ▸ Monoid.pow_exponent_eq_one (e y), he]
·
classical
have univ₂ : {e (x * y), e x, e y, (1 : G₂)} = Finset.univ := by
simpa [map_univ_equiv e, map_insert, he] using congr(Finset.map e.toEmbedding $(eq_finset_univ hx hy hxy))
rw [← Ne, ← e.injective.ne_iff] at hx hy hxy
rw [he] at hx hy
symm
apply eq_of_mem_insert_of_notMem <| univ₂.symm ▸ mem_univ _
simpa using mul_notMem_of_exponent_two h hx hy hxy
