Multiplicative bases

MultiplicativeBasisDeformations.Foundations.MeshWeightsConn

Connectedness of the Auslander–Reiten quiver in Lemma 7.4 and Proposition 7.5 #

weights-and-parameters.tex, scalar-normalization.tex: "we assume that A is connected. Then Γ_A is connected by [ARS, Theorem VII.2.1]." The generic statements of Lemma 7.4 and Proposition 7.5 (exists_meshWt_lift, res_eq_zero_iff, eq_zero_of_diff, chars_part_of_basis) assume that every vertex is reached from a base projective by a lifted walk (hK), and Proposition 7.2(1) assumes that the projectives of A₀ are connected (A0Conn). Both follow from the connectedness of the quiver (QConn): walks lift to the cover (aconn_of_walk, hK_of_QConn), and lifted projectives in one component of the lifted quiver are connected in L (conn_of_aconn), hence by nonzero pieces of A₀ (A0Conn_of_QConn).

source
def MultiplicativeBasisDeformations.MeshWalk.QConn (V : Type) [Quiver V] :
Prop

The quiver is connected: any two vertices are joined by a walk of arrows.

Instances For
    source
    theorem MultiplicativeBasisDeformations.MeshWalk.aconn_of_walk {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {v₀ : V} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {X Y : V} (h : Relation.EqvGen (fun (X Y : V) => Nonempty (X ⟶ Y)) X Y) (g : Deck Q v₀) :
    ∃ (g' : Deck Q v₀), aconn Q v₀ (X, g) (Y, g')

    Walks lift to the cover from any sheet.

    source
    theorem MultiplicativeBasisDeformations.MeshWalk.hK_of_QConn {k : Type u} [Field k] [IsAlgClosed k] [Infinite k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {v₀ : V} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (hQ : QConn V) (x₀ : D.PV) (X : V) :
    ∃ (g : Deck Q v₀), aconn Q v₀ (↑x₀, 1) (X, g)

    Every vertex is reached from the base projective by a lifted walk.

    source
    theorem MultiplicativeBasisDeformations.MeshWalk.A0Conn_of_QConn {k : Type u} [Field k] [IsAlgClosed k] [Infinite k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {v₀ : V} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (hQ : QConn V) (x₀ : D.PV) :
    A0Conn Q c v₀ D x₀

    The projectives of A₀ are connected by nonzero pieces.

    From connectedness of A₀ #

    source
    theorem MultiplicativeBasisDeformations.MeshWalk.exists_path_of_mem {k : Type u} [Field k] [IsAlgClosed k] [Infinite k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {v₀ : V} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {x y : V} {g : Deck Q v₀} {f : meshFam Q c x ⟶ meshFam Q c y} (hf : f ∈ (deckGrading Q c v₀).part g x y) (hf0 : f ≠ 0) :
    ∃ (p : Quiver.Path x y), (degW Q v₀).deg p = g

    A nonzero morphism between lifted labels contains the image of a path of its degree.

    source
    theorem MultiplicativeBasisDeformations.MeshWalk.exists_nz_of_ne_zero {k : Type u} [Field k] [IsAlgClosed k] [Infinite k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {v₀ : V} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {p q : D.PV} {u : D.F0 p ⟶ D.F0 q} (hu : u ≠ 0) :
    ∃ (g : Deck Q v₀), NZ Q c v₀ D (p, q, g)

    A nonzero morphism of A₀ has a nonzero deck piece.

    source
    theorem MultiplicativeBasisDeformations.MeshWalk.idem_apply₀ {k : Type u} [Field k] [IsAlgClosed k] [Infinite k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (x y z : D.PV) :
    CatAlg.idem x y z = CategoryTheory.CategoryStruct.comp (CatAlg.idTo y x) (CatAlg.idTo x z)
    source
    theorem MultiplicativeBasisDeformations.MeshWalk.idem_mul_mul_idem_apply {k : Type u} [Field k] [IsAlgClosed k] [Infinite k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (u : CatAlg.Alg D.F0) (p q y z : D.PV) :
    (CatAlg.idem q * u * CatAlg.idem p) y z = CategoryTheory.CategoryStruct.comp (CatAlg.idTo y q) (CategoryTheory.CategoryStruct.comp (u q p) (CatAlg.idTo p z))
    source
    theorem MultiplicativeBasisDeformations.MeshWalk.exists_nz_of_corner {k : Type u} [Field k] [IsAlgClosed k] [Infinite k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {v₀ : V} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {p q : D.PV} {x : (CatAlg.Alg D.F0)ᵐᵒᵖ} (h : MulOpposite.op (CatAlg.idem p) * x * MulOpposite.op (CatAlg.idem q) ≠ 0) :
    ∃ (g : Deck Q v₀), NZ Q c v₀ D (q, p, g)

    Nonzero corners e_p A₀ e_q give nonzero pieces.

    source
    theorem MultiplicativeBasisDeformations.MeshWalk.A0Conn_of_corners {k : Type u} [Field k] [IsAlgClosed k] [Infinite k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {v₀ : V} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (h : ∀ (p q : D.PV), Relation.EqvGen (fun (p q : D.PV) => ∃ (x : (CatAlg.Alg D.F0)ᵐᵒᵖ), MulOpposite.op (CatAlg.idem p) * x * MulOpposite.op (CatAlg.idem q) ≠ 0) p q) (x₀ : D.PV) :
    A0Conn Q c v₀ D x₀

    Connectedness of A₀ by its corners gives A0Conn.

    source
    theorem MultiplicativeBasisDeformations.MeshWalk.hK_of_A0Conn {k : Type u} [Field k] [IsAlgClosed k] [Infinite k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {v₀ : V} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (x₀ : D.PV) (hconn : A0Conn Q c v₀ D x₀) (X : V) :
    ∃ (g : Deck Q v₀), aconn Q v₀ (↑x₀, 1) (X, g)

    Every vertex is reached from the base projective by a lifted walk, when A₀ is connected: projectives are joined by paths of nonzero pieces, and every lifted object receives a nonzero map, hence a path, from a lifted projective.