English
If a monoid homomorphism f: A →* B has the property that for all u,v: B →* B ⧸ f.range, u ∘ f = v ∘ f implies u = v, then f.range = ⊤ (the range is all of B).
Русский
Если для гомоморфизма f: A →* B верно, что для всех u,v: B →* B ⧸ f.range, u ∘ f = v ∘ f ⇒ u = v, тогда f.range = ⊤ (образ равен всему B).
LaTeX
$$$ f.\mathrm{range} = \top \quad\text{при условии } \forall u,v:\, u \circ f = v \circ f \Rightarrow u = v $$$
Lean4
@[to_additive]
theorem range_eq_top_of_cancel {f : A →* B} (h : ∀ u v : B →* B ⧸ f.range, u.comp f = v.comp f → u = v) : f.range = ⊤ :=
by
specialize h 1 (QuotientGroup.mk' _) _
· ext1 x
simp only [one_apply, coe_comp, coe_mk', Function.comp_apply]
rw [show (1 : B ⧸ f.range) = (1 : B) from QuotientGroup.mk_one _, QuotientGroup.eq, inv_one, one_mul]
exact ⟨x, rfl⟩
replace h : (QuotientGroup.mk' f.range).ker = (1 : B →* B ⧸ f.range).ker := by rw [h]
rwa [ker_one, QuotientGroup.ker_mk'] at h
