The representable poset-space realization functor

This file formalizes the concrete functor in the frozen manuscript. Given a distinguished source P, projective objects P_t, and compatible maps P ⟶ P_t, an object X is sent to the poset space with total space Hom(P,X) and t-subspace the image of

Hom(P_t,X) ⟶ Hom(P,X).

The genuinely structural part of Iyama's theorem—fullness and essential surjectivity—is kept visible as data to be constructed from the primitive factor, rather than postulated in the public theorem.

structure MagnitudeConjecture.PosetSpace.RepresentableData (k T : Type u) (C : Type v) [Field k] [PartialOrder T] [CategoryTheory.Category.{u, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] : Type (max u v)

Categorical data needed to define the manuscript's representable poset-space functor. factor is the coherent form of the order relation: when s ≤ t, the chosen map to P_s factors through the chosen map to P_t.

• source : C
• projective : T → C
• unit (t : T) : self.source ⟶ self.projective t
• factor {s t : T} : s ≤ t → ∃ (v : self.projective t ⟶ self.projective s), CategoryTheory.CategoryStruct.comp (self.unit t) v = self.unit s
• homFinite (X : C) : Module.Finite k (self.source ⟶ X)

def MagnitudeConjecture.PosetSpace.RepresentableData.precomposition {k T : Type u} {C : Type v} [Field k] [PartialOrder T] [CategoryTheory.Category.{u, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (D : RepresentableData k T C) (t : T) (X : C) : (D.projective t ⟶ X) →ₗ[k] D.source ⟶ X

Precomposition with the chosen map P ⟶ P_t.

def MagnitudeConjecture.PosetSpace.RepresentableData.postcomposition {k T : Type u} {C : Type v} [Field k] [PartialOrder T] [CategoryTheory.Category.{u, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (D : RepresentableData k T C) {X Y : C} (f : X ⟶ Y) : (D.source ⟶ X) →ₗ[k] D.source ⟶ Y

Postcomposition with a categorical morphism.

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

The representable T-space attached to X.

def MagnitudeConjecture.PosetSpace.RepresentableData.map {k T : Type u} {C : Type v} [Field k] [PartialOrder T] [CategoryTheory.Category.{u, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (D : RepresentableData k T C) {X Y : C} (f : X ⟶ Y) : D.obj X ⟶ D.obj Y

Postcomposition defines a morphism of representable poset spaces.

@[simp]

theorem MagnitudeConjecture.PosetSpace.RepresentableData.map_linear {k T : Type u} {C : Type v} [Field k] [PartialOrder T] [CategoryTheory.Category.{u, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (D : RepresentableData k T C) {X Y : C} (f : X ⟶ Y) : (D.map f).linear = D.postcomposition f

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

The manuscript's objectwise construction is a literal functor.

@[simp]

theorem MagnitudeConjecture.PosetSpace.RepresentableData.functor_obj {k T : Type u} {C : Type v} [Field k] [PartialOrder T] [CategoryTheory.Category.{u, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (D : RepresentableData k T C) (X : C) : D.functor.obj X = D.obj X

@[simp]

theorem MagnitudeConjecture.PosetSpace.RepresentableData.functor_map {k T : Type u} {C : Type v} [Field k] [PartialOrder T] [CategoryTheory.Category.{u, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (D : RepresentableData k T C) {X Y : C} (f : X ⟶ Y) : D.functor.map f = D.map f

instance MagnitudeConjecture.PosetSpace.RepresentableData.instAdditiveObjFunctor {k T : Type u} {C : Type v} [Field k] [PartialOrder T] [CategoryTheory.Category.{u, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (D : RepresentableData k T C) : D.functor.Additive

instance MagnitudeConjecture.PosetSpace.RepresentableData.instLinearObjFunctor {k T : Type u} {C : Type v} [Field k] [PartialOrder T] [CategoryTheory.Category.{u, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (D : RepresentableData k T C) : CategoryTheory.Functor.Linear k D.functor

theorem MagnitudeConjecture.PosetSpace.RepresentableData.finrank_obj {k T : Type u} {C : Type v} [Field k] [PartialOrder T] [CategoryTheory.Category.{u, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (D : RepresentableData k T C) (X : C) : Module.finrank k (D.obj X).carrier = Module.finrank k (D.source ⟶ X)

The total dimension of the realized poset space is exactly the dimension of the represented Hom space.

theorem MagnitudeConjecture.PosetSpace.RepresentableData.obj_isSchur {k T : Type u} {C : Type v} [Field k] [PartialOrder T] [CategoryTheory.Category.{u, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (D : RepresentableData k T C) {X : C} (hnonzero : ∃ (h : D.source ⟶ X), h ≠ 0) (hfull : ∀ (f : D.obj X ⟶ D.obj X), ∃ (g : X ⟶ X), D.map g = f) (hscalar : ∀ (g : X ⟶ X), ∃ (a : k), g = a • CategoryTheory.CategoryStruct.id X) : IsSchur k T (D.obj X)

Fullness on one object and scalar endomorphisms in the source category make its representable poset space Schur.

theorem MagnitudeConjecture.PosetSpace.RepresentableData.map_injective {k T : Type u} {C : Type v} [Field k] [PartialOrder T] [CategoryTheory.Category.{u, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (D : RepresentableData k T C) (hfaithful : ∀ {X Y : C} (f g : X ⟶ Y), (∀ (h : D.source ⟶ X), CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp h g) → f = g) {X Y : C} : Function.Injective D.functor.map

Faithfulness of Hom(P,-) in elementwise form makes the representable poset-space functor faithful.

theorem MagnitudeConjecture.PosetSpace.RepresentableData.faithful {k T : Type u} {C : Type v} [Field k] [PartialOrder T] [CategoryTheory.Category.{u, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (D : RepresentableData k T C) (hfaithful : ∀ {X Y : C} (f g : X ⟶ Y), (∀ (h : D.source ⟶ X), CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp h g) → f = g) : D.functor.Faithful

The corresponding Functor.Faithful package.

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

Exact extra data needed to promote the concrete representable functor to Iyama's poset-space equivalence. Subsequent work constructs these fields from the literal primitive factor.

• full {X Y : C} (f : D.obj X ⟶ D.obj Y) : ∃ (g : X ⟶ Y), D.map g = f
• faithful {X Y : C} (f g : X ⟶ Y) : D.map f = D.map g → f = g
• essSurj (Y : Obj k T) : ∃ (X : C), Nonempty (D.obj X ≅ Y)

theorem MagnitudeConjecture.PosetSpace.RepresentableData.EquivalenceData.functorFull {k T : Type u} {C : Type v} [Field k] [PartialOrder T] [CategoryTheory.Category.{u, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {D : RepresentableData k T C} (R : D.EquivalenceData) : D.functor.Full

Fullness of the concrete functor.

theorem MagnitudeConjecture.PosetSpace.RepresentableData.EquivalenceData.functorFaithful {k T : Type u} {C : Type v} [Field k] [PartialOrder T] [CategoryTheory.Category.{u, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {D : RepresentableData k T C} (R : D.EquivalenceData) : D.functor.Faithful

Faithfulness of the concrete functor.

theorem MagnitudeConjecture.PosetSpace.RepresentableData.EquivalenceData.functorEssSurj {k T : Type u} {C : Type v} [Field k] [PartialOrder T] [CategoryTheory.Category.{u, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {D : RepresentableData k T C} (R : D.EquivalenceData) : D.functor.EssSurj

Essential surjectivity of the concrete functor.

theorem MagnitudeConjecture.PosetSpace.RepresentableData.EquivalenceData.obj_isSchur {k T : Type u} {C : Type v} [Field k] [PartialOrder T] [CategoryTheory.Category.{u, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {D : RepresentableData k T C} (R : D.EquivalenceData) {X : C} (hnonzero : ∃ (h : D.source ⟶ X), h ≠ 0) (hscalar : ∀ (g : X ⟶ X), ∃ (a : k), g = a • CategoryTheory.CategoryStruct.id X) : IsSchur k T (D.obj X)

A nonzero scalar-endomorphism object is sent to a Schur poset space by the completed realization.

noncomputable def MagnitudeConjecture.PosetSpace.RepresentableData.EquivalenceData.equivalence {k T : Type u} {C : Type v} [Field k] [PartialOrder T] [CategoryTheory.Category.{u, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {D : RepresentableData k T C} (R : D.EquivalenceData) : C ≌ Obj k T

The equivalence furnished by completed realization data.