Magnitude conjecture

MagnitudeConjecture.CategoryTheory.AlmostSplitLocalFunctor

Almost-split morphisms under locally closed functors #

For preservation of a right almost-split map, essential surjectivity is needed only for objects carrying a nonzero nonsplit map to its endpoint. The left statement is dual. These local conditions isolate the role of the first Hom neighborhoods in the covering-control argument, while minimality of either map is preserved by full faithfulness alone.

source
def MagnitudeConjecture.IsLocallyRightObjectClosedAt {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) (Y : C) :
Prop

Every object relevant to testing right almost-splitness at F.obj Y lies in the essential image. The zero map is excluded because it factors trivially and needs no object lift.

Instances For
    source
    def MagnitudeConjecture.IsLocallyLeftObjectClosedAt {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) (X : C) :
    Prop

    Every object relevant to testing left almost-splitness at F.obj X lies in the essential image.

    Instances For
      source
      theorem MagnitudeConjecture.rightAlmostSplit_map_of_full_faithful_of_locallyRightObjectClosed {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.Full] [F.Faithful] [F.PreservesZeroMorphisms] {X Y : C} {f : X ⟶ Y} (hf : QuotientSubmoduleEquidistribution.IsRightAlmostSplit f) (hclosed : IsLocallyRightObjectClosedAt F Y) :
      QuotientSubmoduleEquidistribution.IsRightAlmostSplit (F.map f)

      Full faithfulness and local source-object closure preserve a right almost-split morphism.

      source
      theorem MagnitudeConjecture.leftAlmostSplit_map_of_full_faithful_of_locallyLeftObjectClosed {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.Full] [F.Faithful] [F.PreservesZeroMorphisms] {X Y : C} {f : X ⟶ Y} (hf : QuotientSubmoduleEquidistribution.IsLeftAlmostSplit f) (hclosed : IsLocallyLeftObjectClosedAt F X) :
      QuotientSubmoduleEquidistribution.IsLeftAlmostSplit (F.map f)

      Full faithfulness and local target-object closure preserve a left almost-split morphism.

      source
      theorem MagnitudeConjecture.rightAlmostSplit_of_map_full_faithful {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.Full] [F.Faithful] [F.PreservesZeroMorphisms] {X Y : C} {f : X ⟶ Y} (hf : QuotientSubmoduleEquidistribution.IsRightAlmostSplit (F.map f)) :
      QuotientSubmoduleEquidistribution.IsRightAlmostSplit f

      Full faithfulness reflects right almost-splitness. This is the restriction direction used for a full control window containing both terms of an ambient sink map.

      source
      theorem MagnitudeConjecture.leftAlmostSplit_of_map_full_faithful {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.Full] [F.Faithful] [F.PreservesZeroMorphisms] {X Y : C} {f : X ⟶ Y} (hf : QuotientSubmoduleEquidistribution.IsLeftAlmostSplit (F.map f)) :
      QuotientSubmoduleEquidistribution.IsLeftAlmostSplit f

      Full faithfulness reflects left almost-splitness.

      source
      theorem MagnitudeConjecture.rightMinimal_map_of_full_faithful {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor C D) [F.Full] [F.Faithful] {X Y : C} {f : X ⟶ Y} (hf : QuotientSubmoduleEquidistribution.IsRightMinimal f) :
      QuotientSubmoduleEquidistribution.IsRightMinimal (F.map f)

      Full faithfulness preserves right minimality.

      source
      theorem MagnitudeConjecture.rightMinimal_of_map_full_faithful {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor C D) [F.Full] [F.Faithful] {X Y : C} {f : X ⟶ Y} (hf : QuotientSubmoduleEquidistribution.IsRightMinimal (F.map f)) :
      QuotientSubmoduleEquidistribution.IsRightMinimal f

      Full faithfulness reflects right minimality.

      source
      theorem MagnitudeConjecture.leftMinimal_map_of_full_faithful {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor C D) [F.Full] [F.Faithful] {X Y : C} {f : X ⟶ Y} (hf : QuotientSubmoduleEquidistribution.IsLeftMinimal f) :
      QuotientSubmoduleEquidistribution.IsLeftMinimal (F.map f)

      Full faithfulness preserves left minimality.