docs(qft): add Feynman diagram and topological field theory API maps

Physlib/QFT/PerturbationTheory/FeynmanDiagrams/API-map.yaml

@@ -0,0 +1,68 @@
+version: v0.1
+
+Title: "Feynman diagrams"
+
+Overview: |
+  The key data structure is a Feynman diagram, understood here as a partition of a
+  multiset of field operators into disjoint pairs. This is the multiset counterpart of
+  a Wick contraction, which is a finite set of disjoint pairs of positions in a list
+  of field operators; the intended relation is that the permissible Wick contractions,
+  those contributing a non-zero amount to the vacuum expectation value, embed into
+  Feynman diagrams. Passing from lists to multisets makes a diagram independent of the
+  order in which the operators were written, and it is the resulting many-to-one map
+  from contractions to diagrams that a symmetry factor must account for.
+
+  The API is to be built on top of the perturbation-theory material already in the
+  library. A `FieldSpecification` fixes the fields of a theory, their bosonic or
+  fermionic statistics, and the labels from which the field operators and their
+  creation and annihilation parts are built; `FieldOpFreeAlgebra` and `WickAlgebra`
+  supply the operator algebra in which the value of a diagram is to be computed;
+  `WickContraction` supplies the pairings of a list together with their signs, time
+  contractions and the machinery used by Wick's theorem. A position field operator
+  carries a point of `SpaceTime`, which is a Lorentz vector carrying an action of the
+  Lorentz group, so the Lorentz group is a parent of this API as well, reached through
+  `FieldSpecification`.
+
+  This is a tracking map for issue #882. The directory currently holds a single Lean
+  file, `Basic.lean`, which states the intended design in its module documentation and
+  contains no declarations. Every requirement below is therefore recorded as not done
+  with location N/A. The directory is marked in that file as a work in progress.
+
+ParentAPIs:
+  - "Field specification (Physlib/QFT/PerturbationTheory/FieldSpecification)"
+  - "Field operator free algebra (Physlib/QFT/PerturbationTheory/FieldOpFreeAlgebra)"
+  - "Wick algebra (Physlib/QFT/PerturbationTheory/WickAlgebra)"
+  - "Wick contractions (Physlib/QFT/PerturbationTheory/WickContraction)"
+  - "Koszul signs (Physlib/QFT/PerturbationTheory/Koszul)"
+  - "Field statistics (Physlib/QFT/PerturbationTheory/FieldStatistics)"
+  - "Lorentz group (Physlib/Relativity/LorentzGroup)"
+
+References:
+  - "https://en.wikipedia.org/wiki/Feynman_diagram"
+  - "M. E. Peskin and D. V. Schroeder, An Introduction to Quantum Field Theory, chapter 4."
+
+Requirements:
+
+  - description: "The key data structure of a Feynman diagram, a partition of a multiset of field operators into disjoint pairs, shall be defined."
+    done: false
+    location: N/A
+
+  - description: "The definition shall be general enough to accept any Feynman diagram from any theory."
+    done: false
+    location: N/A
+
+  - description: "The API shall contain a definition to provably generate all Feynman diagrams up to a given order for a given amplitude."
+    done: false
+    location: N/A
+
+  - description: "The API shall contain a computable definition of the symmetry factor of a Feynman diagram."
+    done: false
+    location: N/A
+
+  - description: "The API shall contain a definition permitting the conversion of a Feynman diagram into its underlying algebraic expression."
+    done: false
+    location: N/A
+
+  - description: "The API shall contain the embedding of permissible Wick contractions, those which do not contribute zero to the vacuum expectation value, into Feynman diagrams."
+    done: false
+    location: N/A

Physlib/QFT/TopologicalFieldTheory/API-map.yaml

@@ -0,0 +1,105 @@
+version: v0.1
+
+Title: "Topological field theory"
+
+Overview: |
+  A topological field theory assigns algebraic data to manifolds in a way that
+  depends only on their topology. In the Atiyah-Segal formulation a theory in
+  dimension `d` is a symmetric monoidal functor from a category of cobordisms,
+  whose objects are closed oriented `(d-1)`-manifolds and whose morphisms are
+  oriented `d`-dimensional cobordisms between them, to the category of modules
+  over a fixed commutative ring. The state space of a closed `(d-1)`-manifold is
+  the value of the functor on that object, and the partition function of a closed
+  `d`-manifold is the value of the functor on it read as a cobordism from the
+  empty manifold to itself. No metric on the world-volume enters the construction,
+  so every number and every space produced this way is an invariant of the
+  underlying manifold.
+
+  This is a tracking map for issue #877. No part of it is formalized in the
+  current library: there is no category of cobordisms, no monoidal functor into
+  modules, and no example theory such as Chern-Simons theory or BF theory. The one
+  adjacent piece is the time manifold `TimeMan`
+  (Physlib/SpaceAndTime/Time/TimeMan.lean), time carrying an orientation but no
+  metric, which is the one-dimensional world-volume on which such a theory would
+  be placed. Every requirement below is therefore recorded as not done with
+  location N/A.
+
+ParentAPIs:
+  - "Time (Physlib/SpaceAndTime/Time)"
+
+References:
+  - "M. F. Atiyah, Topological quantum field theories, Publications Mathematiques de l'IHES 68 (1988), 175-186"
+  - "G. Segal, The definition of conformal field theory, in Differential Geometrical Methods in Theoretical Physics (1988), 165-171"
+  - "E. Witten, Quantum field theory and the Jones polynomial, Communications in Mathematical Physics 121 (1989), 351-399"
+  - "J. Kock, Frobenius Algebras and 2D Topological Quantum Field Theories, Cambridge University Press (2003)"
+  - "J. Lurie, On the classification of topological field theories, Current Developments in Mathematics 2008 (2009), 129-280"
+
+Requirements:
+
+  - description: "The API shall contain the category of cobordisms in dimension `d`, with closed oriented `(d-1)`-manifolds as objects and oriented cobordisms taken up to boundary-preserving diffeomorphism as morphisms, composed by gluing along a common boundary."
+    done: false
+    location: "N/A"
+
+  - description: "The API shall contain the symmetric monoidal structure on the cobordism category given by disjoint union, with the empty `(d-1)`-manifold as the unit object."
+    done: false
+    location: "N/A"
+
+  - description: "The key data structure, a topological field theory in dimension `d`, shall be defined as a symmetric monoidal functor from the cobordism category to the category of modules over a fixed commutative ring."
+    done: false
+    location: "N/A"
+
+  - description: "The API shall contain the state space assigned to a closed oriented `(d-1)`-manifold, together with the finiteness condition that it is finitely generated (finite dimensional when the ground ring is a field)."
+    done: false
+    location: "N/A"
+
+  - description: "The API shall contain the multiplicativity axiom, that the state space of a disjoint union is the tensor product of the state spaces, and the normalisation assigning the ground ring to the empty manifold."
+    done: false
+    location: "N/A"
+
+  - description: "The API shall contain the gluing axiom, that the map assigned to a cobordism cut along a closed `(d-1)`-manifold is the composite of the maps assigned to the two pieces."
+    done: false
+    location: "N/A"
+
+  - description: "The API shall contain the partition function of a closed oriented `d`-manifold as an element of the ground ring, and its invariance under orientation-preserving diffeomorphism."
+    done: false
+    location: "N/A"
+
+  - description: "The API shall contain the behaviour under orientation reversal, that the state space of a manifold with reversed orientation is dual to the original one, and that the pairing between them coming from the cylinder is nondegenerate."
+    done: false
+    location: "N/A"
+
+  - description: "The API shall show that a cylinder induces the identity map on the state space, so that a topological theory has no time evolution on a fixed spatial slice."
+    done: false
+    location: "N/A"
+
+  - description: "The API shall contain the trace formula, that the partition function of the product of a closed `(d-1)`-manifold with a circle equals the rank of the state space of that manifold."
+    done: false
+    location: "N/A"
+
+  - description: "The API shall contain the classification in dimension two, an equivalence between topological field theories valued in vector spaces over a field and commutative Frobenius algebras."
+    done: false
+    location: "N/A"
+
+  - description: "The API shall contain the classification in dimension one, an equivalence between topological field theories and finitely generated projective modules."
+    done: false
+    location: "N/A"
+
+  - description: "The API shall contain topological quantum mechanics on the time manifold `TimeMan`, the one-dimensional case in which the world-volume carries an orientation but no metric."
+    done: false
+    location: "N/A"
+
+  - description: "The API shall contain the Chern-Simons action of a connection on a principal bundle over a closed oriented three-manifold, its independence of any metric, its gauge invariance up to a shift by an integer multiple of the level, and the identification of its critical points with flat connections."
+    done: false
+    location: "N/A"
+
+  - description: "The API shall contain the BF action in general dimension, its independence of any metric, and its field equations stating that the connection is flat and the field `B` is covariantly constant."
+    done: false
+    location: "N/A"
+
+  - description: "The API shall contain Wilson-loop observables of a topological gauge theory, their invariance under gauge transformation, and the link invariants obtained from their expectation values."
+    done: false
+    location: "N/A"
+
+  - description: "The API shall contain the finite gauge group (Dijkgraaf-Witten) theory as a worked example, with a partition function counting principal bundles over the manifold weighted by a group cocycle."
+    done: false
+    location: "N/A"