PhysLean Documentation

PhysLean.QFT.QED.AnomalyCancellation.BasisLinear

Basis of LinSols #

We give a basis of vector space LinSols, and find the rank thereof.

The basis elements as charges, defined to have a 1 in the jth position and a -1 in the last position.

Equations
Instances For

    The basis elements as LinSols.

    Equations
    Instances For
      theorem PureU1.BasisLinear.sum_of_vectors {k n : } (f : Fin k(PureU1 n).LinSols) (j : Fin n) :
      (∑ i : Fin k, f i).val j = i : Fin k, (f i).val j

      The coordinate map for the basis.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        The basis of LinSols.

        Equations
        Instances For

          The module over defined by linear solutions to the pure U(1) ACCs is finite.

          The module of solutions to the linear pure-U(1) acc has rank equal to n.