Incidence boundary evaluations of a finite poset space

For t in a finite poset, the projective boundary line P_t is supported on the principal filter Set.Ici t. Its complementary boundary line Q_t is supported on the complement of the principal ideal Set.Iic t.

This file proves the two concrete evaluations used in the frozen manuscript:

• maps P_t ⟶ X are the vectors in the distinguished subspace X_t;
• maps X ⟶ Q_t are the linear functionals on X / X_t.

For a one-dimensional total space these evaluations are complementary: the first Hom space is nonzero exactly when the second Hom space vanishes.

def MagnitudeConjecture.PosetSpace.coPrincipalSupport {T : Type u} [PartialOrder T] (t : T) : Set T

The complement of the principal ideal generated by t.

theorem MagnitudeConjecture.PosetSpace.coPrincipalSupport_isUpperSet {T : Type u} [PartialOrder T] (t : T) : IsUpperSet (coPrincipalSupport t)

The complement of a principal ideal is an upper set.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.PosetSpace.coPrincipalLine {k T : Type u} [Field k] [PartialOrder T] (t : T) : Obj k T

The complementary one-dimensional boundary object Q_t.

noncomputable def MagnitudeConjecture.PosetSpace.principalLineEvaluation {k T : Type u} [Field k] [PartialOrder T] (t : T) (X : Obj k T) : (line k T (Set.Ici t) ⋯ ⟶ X) →ₗ[k] ↥(X.subspace t)

Evaluation at 1 sends a map from P_t to its value in X_t.

def MagnitudeConjecture.PosetSpace.principalLineMapOfVector {k T : Type u} [Field k] [PartialOrder T] (t : T) (X : Obj k T) (x : ↥(X.subspace t)) : line k T (Set.Ici t) ⋯ ⟶ X

A vector of X_t defines a map from the principal-filter line.

noncomputable def MagnitudeConjecture.PosetSpace.homFromPrincipalLineEquiv {k T : Type u} [Field k] [PartialOrder T] (t : T) (X : Obj k T) : (line k T (Set.Ici t) ⋯ ⟶ X) ≃ₗ[k] ↥(X.subspace t)

The projective incidence evaluation Hom(P_t,X) ≃ X_t.

theorem MagnitudeConjecture.PosetSpace.homToCoPrincipalLine_vanishes {k T : Type u} [Field k] [PartialOrder T] (t : T) (X : Obj k T) (f : X ⟶ coPrincipalLine t) : X.subspace t ≤ f.linear.ker

Every map X ⟶ Q_t vanishes on the distinguished subspace X_t.

def MagnitudeConjecture.PosetSpace.coPrincipalQuotientEvaluation {k T : Type u} [Field k] [PartialOrder T] (t : T) (X : Obj k T) : (X ⟶ coPrincipalLine t) →ₗ[k] Module.Dual k (X.carrier ⧸ X.subspace t)

A map to Q_t descends to a functional on X / X_t.

def MagnitudeConjecture.PosetSpace.coPrincipalLineMapOfQuotientDual {k T : Type u} [Field k] [PartialOrder T] (t : T) (X : Obj k T) (f : Module.Dual k (X.carrier ⧸ X.subspace t)) : X ⟶ coPrincipalLine t

A functional on X / X_t defines a morphism X ⟶ Q_t.

noncomputable def MagnitudeConjecture.PosetSpace.homToCoPrincipalLineEquiv {k T : Type u} [Field k] [PartialOrder T] (t : T) (X : Obj k T) : (X ⟶ coPrincipalLine t) ≃ₗ[k] Module.Dual k (X.carrier ⧸ X.subspace t)

The quotient-dual incidence evaluation Hom(X,Q_t) ≃ D(X/X_t).

noncomputable def MagnitudeConjecture.PosetSpace.quotientEquivDualHomToCoPrincipalLine {k T : Type u} [Field k] [PartialOrder T] [Fintype T] (t : T) (X : Obj k T) : (X.carrier ⧸ X.subspace t) ≃ₗ[k] Module.Dual k (X ⟶ coPrincipalLine t)

Reflexivity of finite-dimensional vector spaces turns quotient evaluation into the dual of the Q_t-corepresentable.

noncomputable def MagnitudeConjecture.PosetSpace.incidenceBoundaryEvaluation {k T : Type u} [Field k] [PartialOrder T] [Fintype T] (t : T) (X : Obj k T) : X.carrier →ₗ[k] Module.Dual k (X ⟶ coPrincipalLine t)

The pointwise boundary map in the incidence exact sequence. It is the quotient map X ⟶ X/X_t, followed by the canonical identification of the quotient with D Hom(X,Q_t).

@[simp]

theorem MagnitudeConjecture.PosetSpace.incidenceBoundaryEvaluation_apply {k T : Type u} [Field k] [PartialOrder T] [Fintype T] (t : T) (X : Obj k T) (x : X.carrier) (f : X ⟶ coPrincipalLine t) : ((incidenceBoundaryEvaluation t X) x) f = f.linear x

The incidence boundary functional evaluates a map X ⟶ Q_t on the chosen vector of X.

theorem MagnitudeConjecture.PosetSpace.incidenceBoundaryEvaluation_ker {k T : Type u} [Field k] [PartialOrder T] [Fintype T] (t : T) (X : Obj k T) : (incidenceBoundaryEvaluation t X).ker = X.subspace t

The kernel of the boundary evaluation is exactly the distinguished subspace X_t.

theorem MagnitudeConjecture.PosetSpace.incidenceBoundaryEvaluation_surjective {k T : Type u} [Field k] [PartialOrder T] [Fintype T] (t : T) (X : Obj k T) : Function.Surjective ⇑(incidenceBoundaryEvaluation t X)

The boundary evaluation is onto.

noncomputable def MagnitudeConjecture.PosetSpace.homToCoPrincipalLinePrecomposition {k T : Type u} [Field k] [PartialOrder T] (t : T) {X Y : Obj k T} (f : X ⟶ Y) : (Y ⟶ coPrincipalLine t) →ₗ[k] X ⟶ coPrincipalLine t

Precomposition on morphisms into Q_t.

theorem MagnitudeConjecture.PosetSpace.incidenceBoundaryEvaluation_natural {k T : Type u} [Field k] [PartialOrder T] [Fintype T] (t : T) {X Y : Obj k T} (f : X ⟶ Y) (x : X.carrier) : (incidenceBoundaryEvaluation t Y) (f.linear x) = (homToCoPrincipalLinePrecomposition t f).dualMap ((incidenceBoundaryEvaluation t X) x)

Naturality of the incidence boundary evaluation. Postcomposition on the total spaces agrees with the dual of precomposition into Q_t.

theorem MagnitudeConjecture.PosetSpace.principalSubspace_incidenceBoundaryEvaluation_exact {k T : Type u} [Field k] [PartialOrder T] [Fintype T] (t : T) (X : Obj k T) : Function.Exact ⇑(X.subspace t).subtype ⇑(incidenceBoundaryEvaluation t X)

Pointwise exactness of the manuscript's incidence sequence

0 → X_t → X → D Hom(X,Q_t) → 0.

The first map is the literal subspace inclusion and the second is incidenceBoundaryEvaluation.

theorem MagnitudeConjecture.PosetSpace.homFromPrincipalLine_nonzero_iff_homToCoPrincipalLine_eq_zero {k T : Type u} [Field k] [PartialOrder T] [Fintype T] (t : T) (X : Obj k T) (hX : Module.finrank k X.carrier = 1) : (∃ (f : line k T (Set.Ici t) ⋯ ⟶ X), f ≠ 0) ↔ ∀ (g : X ⟶ coPrincipalLine t), g = 0

For a one-dimensional total space, the two incidence evaluations are complementary.