Documentation

EpsilonEridani.Particles.Parton.Species

Parton species and their charge conjugation #

For a hadron whose quarks come in the flavours of a type Flavor, the parton species are the quark and the antiquark of each flavour and the gluon. This file names that index type, Species Flavor, so that the quark, antiquark and gluon distributions of a hadron (collinear densities, TMDs, fragmentation functions) are indexed by one type, and a species sum such as the momentum sum rule ∑ₛ ∫₀¹ x fₛ(x) dx = 1 runs over all of them, the gluon included.

Charge conjugation exchanges the quark and the antiquark of each flavour and fixes the gluon (Species.conj); it is an involution.

Main definitions #

Main statements #

References #

source
inductive EpsilonEridani.Particles.Parton.Species (Flavor : Type) :
Type

A parton species over the quark-flavour type Flavor: the quark of a flavour, the antiquark of a flavour, or the gluon.

  • quark {Flavor : Type} (i : Flavor) : Species Flavor

    The quark of flavour i.

  • antiquark {Flavor : Type} (i : Flavor) : Species Flavor

    The antiquark of flavour i.

  • gluon {Flavor : Type} : Species Flavor

    The gluon.

Instances For
    source
    @[instance_reducible]
    instance EpsilonEridani.Particles.Parton.instDecidableEqSpecies {Flavor✝ : Type} [DecidableEq Flavor✝] :
    DecidableEq (Species Flavor✝)
    Equations
    source
    def EpsilonEridani.Particles.Parton.instDecidableEqSpecies.decEq {Flavor✝ : Type} [DecidableEq Flavor✝] (x✝ x✝¹ : Species Flavor✝) :
    Decidable (x✝ = x✝¹)
    Equations
    Instances For
      source
      def EpsilonEridani.Particles.Parton.Species.equivSum {Flavor : Type} :
      Species Flavor ≃ (Flavor ⊕ Flavor) ⊕ Unit

      The species over Flavor are equivalent to (Flavor ⊕ Flavor) ⊕ Unit: the quark of flavour i goes to .inl (.inl i), the antiquark of flavour i to .inl (.inr i), and the gluon to .inr (). It carries the Fintype instance on species and sum_univ.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem EpsilonEridani.Particles.Parton.Species.equivSum_quark {Flavor : Type} (i : Flavor) :
        equivSum (quark i) = Sum.inl (Sum.inl i)
        source
        @[simp]
        theorem EpsilonEridani.Particles.Parton.Species.equivSum_antiquark {Flavor : Type} (i : Flavor) :
        equivSum (antiquark i) = Sum.inl (Sum.inr i)
        source
        @[simp]
        theorem EpsilonEridani.Particles.Parton.Species.equivSum_gluon {Flavor : Type} :
        equivSum gluon = Sum.inr ()
        source
        @[simp]
        theorem EpsilonEridani.Particles.Parton.Species.equivSum_symm_inl_inl {Flavor : Type} (i : Flavor) :
        equivSum.symm (Sum.inl (Sum.inl i)) = quark i
        source
        @[simp]
        theorem EpsilonEridani.Particles.Parton.Species.equivSum_symm_inl_inr {Flavor : Type} (i : Flavor) :
        equivSum.symm (Sum.inl (Sum.inr i)) = antiquark i
        source
        @[simp]
        theorem EpsilonEridani.Particles.Parton.Species.equivSum_symm_inr {Flavor : Type} (u : Unit) :
        equivSum.symm (Sum.inr u) = gluon
        source
        @[instance_reducible]
        instance EpsilonEridani.Particles.Parton.Species.instFintype {Flavor : Type} [Fintype Flavor] :
        Fintype (Species Flavor)
        Equations
        source
        @[simp]
        theorem EpsilonEridani.Particles.Parton.Species.card {Flavor : Type} [Fintype Flavor] :
        Fintype.card (Species Flavor) = 2 * Fintype.card Flavor + 1

        There are two species, a quark and an antiquark, for each flavour, and the gluon.

        source
        theorem EpsilonEridani.Particles.Parton.Species.sum_univ {Flavor : Type} [Fintype Flavor] {M : Type u_1} [AddCommMonoid M] (g : Species Flavor → M) :
        ∑ s : Species Flavor, g s = ∑ i : Flavor, g (quark i) + ∑ i : Flavor, g (antiquark i) + g gluon

        A sum over all parton species is the sum over the quarks, the sum over the antiquarks, and the gluon term.

        source
        def EpsilonEridani.Particles.Parton.Species.conj {Flavor : Type} :
        Species Flavor → Species Flavor

        Charge conjugation of parton species: the quark and the antiquark of each flavour are exchanged, and the gluon is its own antiparticle.

        Equations
        Instances For
          source
          @[simp]
          theorem EpsilonEridani.Particles.Parton.Species.conj_quark {Flavor : Type} (i : Flavor) :
          (quark i).conj = antiquark i
          source
          @[simp]
          theorem EpsilonEridani.Particles.Parton.Species.conj_antiquark {Flavor : Type} (i : Flavor) :
          (antiquark i).conj = quark i
          source
          @[simp]
          theorem EpsilonEridani.Particles.Parton.Species.conj_gluon {Flavor : Type} :
          gluon.conj = gluon
          source
          @[simp]
          theorem EpsilonEridani.Particles.Parton.Species.conj_conj {Flavor : Type} (s : Species Flavor) :
          s.conj.conj = s
          source
          theorem EpsilonEridani.Particles.Parton.Species.conj_involutive {Flavor : Type} :
          Function.Involutive conj