instHasStrongEpiMonoFactorisations

English

There exists a canonical factorisation of any morphism into a strong epi followed by a mono.

Русский

Существует каноническое разложение любого морфизма на сильный эпиморфизм, за которым следует мономорфизм.

LaTeX

$$$\exists I\, (e:X\to I),\ (m:I\to Y)\; (\text{StrongEpi}(e)),\ (\text{Mono}(m)),\ f = m \circ e.$$$

Lean4

instance : HasStrongEpiMonoFactorisations NonemptyFinLinOrd.{u} :=
  ⟨fun {X Y} f => by
    let I := of (Set.image f ⊤)
    let e : X ⟶ I := ofHom ⟨fun x => ⟨f x, ⟨x, by tauto⟩⟩, fun x₁ x₂ h => f.hom.monotone h⟩
    let m : I ⟶ Y := ofHom ⟨fun y => y.1, by tauto⟩
    haveI : Epi e := by
      rw [epi_iff_surjective]
      rintro ⟨_, y, h, rfl⟩
      exact ⟨y, rfl⟩
    haveI : StrongEpi e := strongEpi_of_epi e
    haveI : Mono m := ConcreteCategory.mono_of_injective _ (fun x y h => Subtype.ext h)
    exact ⟨⟨I, m, e, rfl⟩⟩⟩

Похожие утверждения