English
For groups M,N,P and homomorphisms f,g with commuting images, the induced noncommCoprod map is injective iff f and g are injective and f.range ∩ g.range = {1}.
Русский
Для групп M,N,P и гомоморфизмов f,g c коммутирующими образами, отображение noncommCoprod инъективно тогда и только тогда, когда f и g инъективны и пересечение образов тривиально.
LaTeX
$$$\\mathrm{Injective}(\\mathrm{noncommCoprod}\\ f\\ g\\ comm) \\iff (\\mathrm{Injective}(f) \\wedge \\mathrm{Injective}(g) \\wedge \\mathrm{Disjoint}(f\\text{-range}, g\\text{-range})).$$$
Lean4
theorem noncommCoprod_injective {M N P : Type*} [Group M] [Group N] [Group P] (f : M →* P) (g : N →* P)
(comm : ∀ (m : M) (n : N), Commute (f m) (g n)) :
Function.Injective (noncommCoprod f g comm) ↔
(Function.Injective f ∧ Function.Injective g ∧ _root_.Disjoint f.range g.range) :=
by
simp only [injective_iff_map_eq_one, disjoint_iff_inf_le, noncommCoprod_apply, Prod.forall, Prod.mk_eq_one]
refine ⟨fun h ↦ ⟨fun x ↦ ?_, fun x ↦ ?_, ?_⟩, ?_⟩
· simpa using h x 1
· simpa using h 1 x
· intro x ⟨⟨y, hy⟩, z, hz⟩
rwa [(h y z⁻¹ (by rw [map_inv, hy, hz, mul_inv_cancel])).1, map_one, eq_comm] at hy
· intro ⟨hf, hg, hp⟩ a b h
have key := hp ⟨⟨a⁻¹, by rwa [map_inv, inv_eq_iff_mul_eq_one]⟩, b, rfl⟩
exact ⟨hf a (by rwa [key, mul_one] at h), hg b key⟩
