fullyFaithful_reflectsColimits — Mathlib

English

A fully faithful functor reflects colimits.

Русский

Полнофункциональный функтор отражает колимиты.

LaTeX

$$$\\text{If } F \\text{ is full and faithful, then } ReflectsColimitsOfSize F$.$$

Lean4

/-- A fully faithful functor reflects colimits. -/
instance fullyFaithful_reflectsColimits [F.Full] [F.Faithful] : ReflectsColimitsOfSize.{w, w'} F where
  reflectsColimitsOfShape {J}
    𝒥₁ :=
    {
      reflectsColimit := fun {K} =>
        {
          reflects := fun {c} t =>
            ⟨(IsColimit.mkCoconeMorphism fun _ => (Cocones.functoriality K F).preimage (t.descCoconeMorphism _)) <|
                by
                apply fun s m => (Cocones.functoriality K F).map_injective _
                intro s m
                rw [Functor.map_preimage]
                apply t.uniq_cocone_morphism⟩ } }

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