functorialSurjectiveInjectiveFactorizationData

Lean4
/-- In the category of types, any map can be functorially factored as a surjective
map followed by an injective map. -/
def functorialSurjectiveInjectiveFactorizationData : FunctorialSurjectiveInjectiveFactorizationData (Type u)
    where
  Z :=
    { obj := fun f => Subtype (Set.range f.hom)
      map := fun φ y =>
        ⟨φ.right y.1, by
          obtain ⟨_, x, rfl⟩ := y
          exact ⟨φ.left x, congr_fun φ.w x⟩⟩ }
  i :=
    { app := fun f x => ⟨f.hom x, ⟨x, rfl⟩⟩
      naturality := fun f g φ => by
        ext x
        exact congr_fun φ.w x }
  p :=
    { app := fun _ y => y.1
      naturality := by intros; rfl; }
  fac := rfl
  hi := by
    rintro f ⟨_, x, rfl⟩
    exact ⟨x, rfl⟩
  hp f x₁ x₂
    h := by
    rw [Subtype.ext_iff]
    exact h
Похожие утверждения