English
In NonemptyFinLinOrd, epi is equivalent to surjective.
Русский
В категории NonemptyFinLinOrd эпиморфизм эквивалентен сюръективности.
LaTeX
$$$\mathrm{Epi}(f) \iff \mathrm{Surjective}(f)$$$
Lean4
theorem epi_iff_surjective {A B : NonemptyFinLinOrd.{u}} (f : A ⟶ B) : Epi f ↔ Function.Surjective f :=
by
constructor
· intro
dsimp only [Function.Surjective]
by_contra! hf'
rcases hf' with ⟨m, hm⟩
let Y := of (ULift (Fin 2))
let p₁ : B ⟶ Y :=
ofHom
⟨fun b => if b < m then ULift.up 0 else ULift.up 1, fun x₁ x₂ h =>
by
simp only
split_ifs with h₁ h₂ h₂
any_goals apply Fin.zero_le
· exfalso
exact h₁ (lt_of_le_of_lt h h₂)
· rfl⟩
let p₂ : B ⟶ Y :=
ofHom
⟨fun b => if b ≤ m then ULift.up 0 else ULift.up 1, fun x₁ x₂ h =>
by
simp only
split_ifs with h₁ h₂ h₂
any_goals apply Fin.zero_le
· exfalso
exact h₁ (h.trans h₂)
· rfl⟩
have h : p₁ m = p₂ m := by
congr
rw [← cancel_epi f]
ext a : 3
simp only [p₁, p₂, hom_comp, OrderHom.comp_coe, Function.comp_apply, hom_ofHom]
change ite _ _ _ = ite _ _ _
split_ifs with h₁ h₂ h₂
any_goals rfl
· exfalso
exact h₂ (le_of_lt h₁)
· exfalso
exact hm a (eq_of_le_of_not_lt h₂ h₁)
simp [Y, p₁, p₂, ConcreteCategory.hom_ofHom] at h
· intro h
exact ConcreteCategory.epi_of_surjective f h
