Multiplicative bases

MultiplicativeBasisDeformations.Foundations.PeriodicComponents

Periodic components and the reduction of D_m to them #

Proposition 5.1 (prop:periodic-localization) and the first paragraph of Appendix A.2 (periodic-mesh-calculations.tex): the cokernel of D_m is computed on the periodic components.

T is the set of τ-periodic vertices. A periodic component is a class of the equivalence relation on T generated by the arrows between vertices of T and by v ~ τ v (the translation edges of the complex K of Subsection 4.1). Each component is closed under τ and τ⁻¹ (isTauClosed_component), and a path with all vertices in T stays in one component.

meshDerivativeSurjective_of_components: if D_m is surjective on every periodic component, it is surjective on C(Q, c).

source
def MultiplicativeBasisDeformations.TranslationQuiver.periodic {V : Type v} [Quiver V] (Q : TranslationQuiver V) :
Set V

The τ-periodic vertices.

Instances For
    source
    theorem MultiplicativeBasisDeformations.TranslationQuiver.isTauPeriodic_iff {V : Type v} [Quiver V] {Q : TranslationQuiver V} (v : V) :
    Q.IsTauPeriodic v ↔ ∃ (h : v ∈ Q.nonprojective), Q.IsTauPeriodic ↑(Q.tau ⟨v, h⟩)
    source
    def MultiplicativeBasisDeformations.TranslationQuiver.PeriodicAdj {V : Type v} [Quiver V] (Q : TranslationQuiver V) (u v : V) :
    Prop

    Adjacency in the periodic part: an arrow, or a translation edge.

    Instances For
      source
      def MultiplicativeBasisDeformations.TranslationQuiver.component {V : Type v} [Quiver V] (Q : TranslationQuiver V) (x : V) :
      Set V

      The periodic component of a vertex.

      Instances For
        source
        theorem MultiplicativeBasisDeformations.TranslationQuiver.mem_component_self {V : Type v} [Quiver V] {Q : TranslationQuiver V} {x : V} (hx : x ∈ Q.periodic) :
        x ∈ Q.component x
        source
        theorem MultiplicativeBasisDeformations.TranslationQuiver.component_subset_periodic {V : Type v} [Quiver V] {Q : TranslationQuiver V} (x : V) :
        Q.component x ⊆ Q.periodic
        source
        theorem MultiplicativeBasisDeformations.TranslationQuiver.isTauClosed_component {V : Type v} [Quiver V] {Q : TranslationQuiver V} (x : V) :
        Q.IsTauClosed (Q.component x)

        Periodic components are closed under τ and τ⁻¹.

        source
        theorem MultiplicativeBasisDeformations.TranslationQuiver.vertices_mem_component {V : Type v} [Quiver V] {Q : TranslationQuiver V} {x a : V} (ha : a ∈ Q.component x) {b : V} (p : Quiver.Path a b) :
        (∀ v ∈ p.vertices, v ∈ Q.periodic) → ∀ v ∈ p.vertices, v ∈ Q.component x

        A path whose vertices are periodic and which starts in a component stays in it.

        source
        theorem MultiplicativeBasisDeformations.meshDerivativeSurjective_of_components {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [DecidablePred fun (x : V) => x ∈ Q.nonprojective] [Fintype V] (m : ℕ) (H : ∀ x ∈ Q.periodic, ScalarMeshCategory.MeshDerivativeSurjective (MeshCoefficients.restrict ⋯ c) m) :
        ScalarMeshCategory.MeshDerivativeSurjective c m

        Proposition 5.1 (prop:periodic-localization), in the form used for the vanishing (Appendix A.2): if D_m is surjective on the scalar mesh category of every periodic component, it is surjective on C(Q, c).