fullyFaithful_reflectsLimits — Mathlib

English

A fully faithful functor reflects limits: if F is full and faithful, then F reflects limits of any shape.

Русский

Полнофункциональный функтор отражает пределы: если F полно и точно, то F отражает пределы любой формы.

LaTeX

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

Lean4

/-- A fully faithful functor reflects limits. -/
instance fullyFaithful_reflectsLimits [F.Full] [F.Faithful] : ReflectsLimitsOfSize.{w, w'} F where
  reflectsLimitsOfShape {J}
    𝒥₁ :=
    {
      reflectsLimit := fun {K} =>
        {
          reflects := fun {c} t =>
            ⟨(IsLimit.mkConeMorphism fun _ => (Cones.functoriality K F).preimage (t.liftConeMorphism _)) <|
                by
                apply fun s m => (Cones.functoriality K F).map_injective _
                intro s m
                rw [Functor.map_preimage]
                apply t.uniq_cone_morphism⟩ } }

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