Evaluation of a detector-generated string summand #
The coherent trajectory construction gives an objectwise module morphism
S_C(F_C(N)) → N. This file begins the reconstruction argument by computing
the matching detector of that morphism.
def
MagnitudeConjecture.BoundQuiver.StringWord.Word.coefficientPointMap
{k : Type u}
[Field k]
(V : ModuleCat k)
(v : ↑V)
:
ModuleCat.of k k ⟶ V
The linear map from the ground field selecting one coefficient vector.
Instances For
@[simp]
theorem
MagnitudeConjecture.BoundQuiver.StringWord.Word.coefficientPointMap_apply
{k : Type u}
[Field k]
(V : ModuleCat k)
(v : ↑V)
(c : k)
:
(CategoryTheory.ConcreteCategory.hom (coefficientPointMap V v)) c = c • v
noncomputable def
MagnitudeConjecture.BoundQuiver.StringWord.Word.coefficientRightModuleMap
{k Q : Type u}
[Field k]
[Quiver Q]
{R : RelationFamily k Q}
(C : Word R)
(hmono : IsMonomial R)
(V : ModuleCat k)
(v : ↑V)
:
C.rightModule hmono ⟶ C.scalarRightModule hmono V
Insert one coefficient vector uniformly along a literal string module.
Instances For
@[simp]
theorem
MagnitudeConjecture.BoundQuiver.StringWord.Word.coefficientRightModuleMap_app_obj_apply
{k Q : Type u}
[Field k]
[Quiver Q]
{R : RelationFamily k Q}
(C : Word R)
(hmono : IsMonomial R)
(V : ModuleCat k)
(v : ↑V)
(x : Q)
(w : C.Space x)
:
(CategoryTheory.ConcreteCategory.hom ((C.coefficientRightModuleMap hmono V v).app (Opposite.op (obj R x)))) w = w ⊗ₜ[k] v
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.detectorLinearMap_comp_apply
{k Q : Type u}
[Field k]
[Quiver Q]
{A : Type u}
[Ring A]
[Algebra k A]
[Fintype Q]
[(x y : Q) → Fintype (x ⟶ y)]
{P : StringPresentation k A Q}
{S : P.ArrowPolarization}
{u₀ : Q}
{t : Bool}
{L M N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)}
(f : L ⟶ M)
(g : M ⟶ N)
(C : EndpointWord S u₀ t)
(q : DetectorSpace L C)
:
(detectorLinearMap (CategoryTheory.CategoryStruct.comp f g) C) q = (detectorLinearMap g C) ((detectorLinearMap f C) q)
Detector maps respect composition, stated on individual detector classes.
noncomputable def
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.coherentDetectorEvaluationSourceClass
{k Q : Type u}
[Field k]
[Quiver Q]
{A : Type u}
[Ring A]
[Algebra k A]
[Fintype Q]
[(x y : Q) → Fintype (x ⟶ y)]
{P : StringPresentation k A Q}
{S : P.ArrowPolarization}
{u₀ : Q}
{t : Bool}
(N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k))
(C : EndpointWord S u₀ t)
(q : DetectorSpace N C)
:
DetectorSpace (C.word.scalarRightModule ⋯ (ModuleCat.of k (DetectorSpace N C))) C
The detector class in F_C(S_C(F_C(N))) obtained by inserting q into
the distinguished target class of the literal string module.
Instances For
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.coherentDetectorPositionMap_targetPosition
{k Q : Type u}
[Field k]
[Quiver Q]
{A : Type u}
[Ring A]
[Algebra k A]
[Fintype Q]
[(x y : Q) → Fintype (x ⟶ y)]
{P : StringPresentation k A Q}
{S : P.ArrowPolarization}
{u₀ : Q}
{t : Bool}
(N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k))
(C : EndpointWord S u₀ t)
(q : DetectorSpace N C)
:
(coherentDetectorPositionMap N C C.word.targetPosition) q = ↑((detectorRepresentative N C) q)
At the target position, coherent detector evaluation is the chosen numerator representative of the detector class.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.coefficientRightModuleMap_comp_coherentDetectorModuleMap_targetBasis
{k Q : Type u}
[Field k]
[Quiver Q]
{A : Type u}
[Ring A]
[Algebra k A]
[Fintype Q]
[(x y : Q) → Fintype (x ⟶ y)]
{P : StringPresentation k A Q}
{S : P.ArrowPolarization}
{u₀ : Q}
{t : Bool}
(N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k))
[N.Additive]
[CategoryTheory.Functor.Linear k N]
(C : EndpointWord S u₀ t)
(q : DetectorSpace N C)
:
(CategoryTheory.ConcreteCategory.hom
((CategoryTheory.CategoryStruct.comp (C.word.coefficientRightModuleMap ⋯ (ModuleCat.of k (DetectorSpace N C)) q)
(coherentDetectorModuleMap N C ⋯)).app
(Opposite.op (obj P.relations u₀))))
(Finsupp.single C.word.targetPosition 1) = ↑((detectorRepresentative N C) q)
Inserting a detector class in the literal target basis and then applying coherent evaluation recovers its chosen numerator representative.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.detectorLinearMap_coefficientRightModuleMap_comp_evaluation
{k Q : Type u}
[Field k]
[Quiver Q]
{A : Type u}
[Ring A]
[Algebra k A]
[Fintype Q]
[(x y : Q) → Fintype (x ⟶ y)]
{P : StringPresentation k A Q}
{S : P.ArrowPolarization}
{u₀ : Q}
{t : Bool}
(N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k))
[N.Additive]
[CategoryTheory.Functor.Linear k N]
(C : EndpointWord S u₀ t)
(q : DetectorSpace N C)
:
(detectorLinearMap
(CategoryTheory.CategoryStruct.comp (C.word.coefficientRightModuleMap ⋯ (ModuleCat.of k (DetectorSpace N C)) q)
(coherentDetectorModuleMap N C ⋯))
C)
C.targetDetectorClass = q
The matching detector sends the composite from the literal string module
through the q coefficient line and coherent evaluation to q itself.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.detectorLinearMap_coherentDetectorModuleMap_sourceClass
{k Q : Type u}
[Field k]
[Quiver Q]
{A : Type u}
[Ring A]
[Algebra k A]
[Fintype Q]
[(x y : Q) → Fintype (x ⟶ y)]
{P : StringPresentation k A Q}
{S : P.ArrowPolarization}
{u₀ : Q}
{t : Bool}
(N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k))
[N.Additive]
[CategoryTheory.Functor.Linear k N]
(C : EndpointWord S u₀ t)
(q : DetectorSpace N C)
:
(detectorLinearMap (coherentDetectorModuleMap N C ⋯) C) (coherentDetectorEvaluationSourceClass N C q) = q
Applying the matching detector to coherent evaluation is onto. The
explicit preimage of q is the distinguished literal target class with
coefficient q.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.detectorLinearMap_coherentDetectorModuleMap_surjective
{k Q : Type u}
[Field k]
[Quiver Q]
{A : Type u}
[Ring A]
[Algebra k A]
[Fintype Q]
[(x y : Q) → Fintype (x ⟶ y)]
{P : StringPresentation k A Q}
{S : P.ArrowPolarization}
{u₀ : Q}
{t : Bool}
(N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k))
[N.Additive]
[CategoryTheory.Functor.Linear k N]
(C : EndpointWord S u₀ t)
:
Function.Surjective ⇑(detectorLinearMap (coherentDetectorModuleMap N C ⋯) C)
noncomputable def
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.coherentFiniteDetectorEvaluation
{k Q : Type u}
[Field k]
[Quiver Q]
{A : Type u}
[Ring A]
[Algebra k A]
[Fintype Q]
[(x y : Q) → Fintype (x ⟶ y)]
{P : StringPresentation k A Q}
{S : P.ArrowPolarization}
{u₀ : Q}
{t : Bool}
(N : CoveringHom.FiniteDimensionalModuleCategory k)
(C : EndpointWord S u₀ t)
:
(C.word.finiteStringEmbeddingFunctor ⋯).obj (C.finiteDetectorFunctor.obj N) ⟶ N
Coherent detector evaluation bundled in the finite-dimensional module category.
Instances For
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.finiteDetectorFunctor_map_coherentFiniteDetectorEvaluation_hom
{k Q : Type u}
[Field k]
[Quiver Q]
{A : Type u}
[Ring A]
[Algebra k A]
[Fintype Q]
[(x y : Q) → Fintype (x ⟶ y)]
{P : StringPresentation k A Q}
{S : P.ArrowPolarization}
{u₀ : Q}
{t : Bool}
(N : CoveringHom.FiniteDimensionalModuleCategory k)
(C : EndpointWord S u₀ t)
:
ModuleCat.Hom.hom (C.finiteDetectorFunctor.map (coherentFiniteDetectorEvaluation N C)).hom = detectorLinearMap (coherentDetectorModuleMap N.obj.obj C ⋯) C
The underlying linear map obtained by applying the matching finite detector to coherent evaluation is the detector quotient map computed above.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.finiteDetectorFunctor_map_coherentFiniteDetectorEvaluation_surjective
{k Q : Type u}
[Field k]
[Quiver Q]
{A : Type u}
[Ring A]
[Algebra k A]
[Fintype Q]
[(x y : Q) → Fintype (x ⟶ y)]
{P : StringPresentation k A Q}
{S : P.ArrowPolarization}
{u₀ : Q}
{t : Bool}
(N : CoveringHom.FiniteDimensionalModuleCategory k)
(C : EndpointWord S u₀ t)
:
Function.Surjective ⇑(ModuleCat.Hom.hom (C.finiteDetectorFunctor.map (coherentFiniteDetectorEvaluation N C)).hom)
The matching finite detector sends coherent evaluation onto the original detector coefficient space.
noncomputable def
MagnitudeConjecture.BoundQuiver.StringWord.DetectorIndex.coherentFiniteDetectorEvaluation
{k Q : Type u}
[Field k]
[Quiver Q]
{A : Type u}
[Ring A]
[Algebra k A]
[Fintype Q]
[(x y : Q) → Fintype (x ⟶ y)]
{P : StringPresentation k A Q}
{S : P.ArrowPolarization}
(N : CoveringHom.FiniteDimensionalModuleCategory k)
(i : DetectorIndex S)
:
i.finiteStringEmbeddingFunctor.obj (i.finiteDetectorFunctor.obj N) ⟶ N
Coherent evaluation for the chosen representative of one detector inversion class.
Instances For
theorem
MagnitudeConjecture.BoundQuiver.StringWord.DetectorIndex.isIso_finiteDetectorFunctor_map_coherentFiniteDetectorEvaluation
{k Q : Type u}
[Field k]
[Quiver Q]
{A : Type u}
[Ring A]
[Algebra k A]
[Fintype Q]
[(x y : Q) → Fintype (x ⟶ y)]
{P : StringPresentation k A Q}
{S : P.ArrowPolarization}
(N : CoveringHom.FiniteDimensionalModuleCategory k)
(i : DetectorIndex S)
:
CategoryTheory.IsIso (i.finiteDetectorFunctor.map (coherentFiniteDetectorEvaluation N i))
The matching detector of coherent evaluation is an isomorphism. Its
surjectivity is the explicit trajectory computation; injectivity follows
because F_i S_i ≅ id makes source and target finite-dimensional spaces have
the same dimension.