Magnitude conjecture

MagnitudeConjecture.CategoryTheory.ExtendSupportedIso

Extending a natural isomorphism between functors that vanish off a full image #

source
noncomputable def MagnitudeConjecture.supportedExtensionIsoAt {D : Type u₁} {C : Type u₂} {E : Type u₃} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.Category.{v₂, u₂} C] [CategoryTheory.Category.{v₃, u₃} E] (I : CategoryTheory.Functor D C) (F G : CategoryTheory.Functor C E) (α : I.comp F ≅ I.comp G) (hF : ∀ c ∉ Set.range I.obj, CategoryTheory.Limits.IsZero (F.obj c)) (hG : ∀ c ∉ Set.range I.obj, CategoryTheory.Limits.IsZero (G.obj c)) (c : C) :
F.obj c ≅ G.obj c

Use the prescribed comparison on the image and the unique zero comparison elsewhere.

Instances For
    source
    theorem MagnitudeConjecture.supportedExtensionIsoAt_image {D : Type u₁} {C : Type u₂} {E : Type u₃} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.Category.{v₂, u₂} C] [CategoryTheory.Category.{v₃, u₃} E] (I : CategoryTheory.Functor D C) (hI : Function.Injective I.obj) (F G : CategoryTheory.Functor C E) (α : I.comp F ≅ I.comp G) (hF : ∀ c ∉ Set.range I.obj, CategoryTheory.Limits.IsZero (F.obj c)) (hG : ∀ c ∉ Set.range I.obj, CategoryTheory.Limits.IsZero (G.obj c)) (d : D) :
    supportedExtensionIsoAt I F G α hF hG (I.obj d) = α.app d
    source
    noncomputable def MagnitudeConjecture.extendSupportedIso {D : Type u₁} {C : Type u₂} {E : Type u₃} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.Category.{v₂, u₂} C] [CategoryTheory.Category.{v₃, u₃} E] (I : CategoryTheory.Functor D C) (hI : Function.Injective I.obj) (F G : CategoryTheory.Functor C E) (α : I.comp F ≅ I.comp G) (hF : ∀ c ∉ Set.range I.obj, CategoryTheory.Limits.IsZero (F.obj c)) (hG : ∀ c ∉ Set.range I.obj, CategoryTheory.Limits.IsZero (G.obj c)) [I.Full] :
    F ≅ G

    A comparison on a full injective image extends when both functors vanish elsewhere.

    Instances For