Magnitude conjecture

MagnitudeConjecture.Combinatorics.PosetSpaceFullSupport

Full-support envelopes of finite poset spaces #

Every finite poset space embeds canonically into the poset space on the same ambient vector space whose distinguished subspaces are all full. This is the elementary envelope used to reduce Iyama essential surjectivity to closure of the restricted-Yoneda image under subobjects.

source
@[reducible, inline]
abbrev MagnitudeConjecture.PosetSpace.fullSupport {k T : Type u} [Field k] [PartialOrder T] (Y : Obj k T) :
Obj k T

The poset space on the same ambient vector space as Y with every distinguished subspace equal to the full space.

Instances For
    source
    def MagnitudeConjecture.PosetSpace.toFullSupport {k T : Type u} [Field k] [PartialOrder T] (Y : Obj k T) :
    Y ⟶ fullSupport Y

    Every poset space embeds into its full-support envelope by the identity map on the ambient vector space.

    Instances For
      source
      @[simp]
      theorem MagnitudeConjecture.PosetSpace.toFullSupport_linear {k T : Type u} [Field k] [PartialOrder T] (Y : Obj k T) :
      (toFullSupport Y).linear = LinearMap.id
      source
      theorem MagnitudeConjecture.PosetSpace.mono_of_linear_injective {k T : Type u} [Field k] [PartialOrder T] {X Y : Obj k T} (f : X ⟶ Y) (hf : Function.Injective ⇑f.linear) :
      CategoryTheory.Mono f

      An injective underlying linear map is a monomorphism of poset spaces.

      source
      theorem MagnitudeConjecture.PosetSpace.epi_of_linear_surjective {k T : Type u} [Field k] [PartialOrder T] {X Y : Obj k T} (f : X ⟶ Y) (hf : Function.Surjective ⇑f.linear) :
      CategoryTheory.Epi f

      A surjective underlying linear map is an epimorphism of poset spaces.

      source
      theorem MagnitudeConjecture.PosetSpace.toFullSupport_mono {k T : Type u} [Field k] [PartialOrder T] (Y : Obj k T) :
      CategoryTheory.Mono (toFullSupport Y)

      The canonical map into the full-support envelope is monic.

      source
      def MagnitudeConjecture.PosetSpace.RepresentableData.EssentialImageClosedUnderSubobjects {k T : Type u} [Field k] [PartialOrder T] {C : Type v} [CategoryTheory.Category.{u, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (D : RepresentableData k T C) :
      Prop

      The essential image of a representable poset-space functor is closed under subobjects if every monomorphism into a represented object has a represented domain, up to isomorphism.

      Instances For
        source
        theorem MagnitudeConjecture.PosetSpace.RepresentableData.essSurj_of_fullSupport_of_closedUnderSubobjects {k T : Type u} [Field k] [PartialOrder T] {C : Type v} [CategoryTheory.Category.{u, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (D : RepresentableData k T C) (hfull : ∀ (Y : Obj k T), ∃ (X : C), Nonempty (D.obj X ≅ fullSupport Y)) (hclosed : D.EssentialImageClosedUnderSubobjects) (Y : Obj k T) :
        ∃ (X : C), Nonempty (D.obj X ≅ Y)

        Once all full-support envelopes are represented, closure of the essential image under subobjects implies essential surjectivity.