English
For groups M,N,P and commuting images f,g, the range of the noncommCoprod f g equals the join (sup) of the ranges of f and g.
Русский
Для групп M,N,P и коммутирующих образов f,g, образ копродукта равен объединению (объединению по надмножество) образов f и g.
LaTeX
$$$\\mathrm{range}(f.noncommCoprod g comm) = f\\text{range} \\vee g\\text{range}.$$$
Lean4
theorem noncommCoprod_range {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)) : (noncommCoprod f g comm).range = f.range ⊔ g.range :=
by
apply le_antisymm
· rintro - ⟨a, rfl⟩
exact mul_mem (mem_sup_left ⟨a.1, rfl⟩) (mem_sup_right ⟨a.2, rfl⟩)
· rw [sup_le_iff]
constructor
· rintro - ⟨a, rfl⟩
exact ⟨(a, 1), by rw [noncommCoprod_apply, map_one, mul_one]⟩
· rintro - ⟨a, rfl⟩
exact ⟨(1, a), by rw [noncommCoprod_apply, map_one, one_mul]⟩
