Documentation

TauCeti.Algebra.Homology.Ginzburg.ZerothCohomology

The zeroth cohomology of the two-dimensional Ginzburg algebra #

Let Q be a finite quiver and Π₂(Q) its non-completed two-dimensional Ginzburg differential graded algebra (TauCeti.isDGAlgebra_ginzburgTwoDifferential). This file proves

H⁰(Π₂(Q)) ≅ Π_k(Q),

the zeroth cohomology algebra of Π₂(Q) is the additive preprojective algebra of Q, over every commutative ring k.

The inclusion of the doubled path algebra gives a map Π_k(Q) → H(Π₂(Q)). Killing adjoined loops gives a map in the other direction, from cohomology to Π_k(Q). These maps identify Π_k(Q) with the degree-zero cohomology. The path-algebra retraction and its degree-zero characterization are available in TauCeti.Algebra.Homology.Ginzburg.LoopGrading.

Main definitions #

Main results #

References #

Boundaries vanish in the preprojective algebra #

source
theorem TauCeti.preprojectiveMk_ginzburgRetraction_ginzburgTwoDifferential (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (x : pathAlgebra k (GinzburgQuiver Q)) :
(preprojectiveMk k Q) ((ginzburgRetraction k) ((ginzburgTwoDifferential k) x)) = 0

Every boundary of Π₂(Q) vanishes in Π_k(Q) once the loops are killed.

The zeroth cohomology #

source
noncomputable def TauCeti.preprojectiveToGinzburgTwoCohomology (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] :
preprojectiveAlgebra k Q →ₐ[k] ⋯.Cohomology

The algebra homomorphism Π_k(Q) → H(Π₂(Q)) sending the class of a doubled path to the cohomology class of the same path, a cycle of Π₂(Q). It is well defined because the relator ρ_i is the boundary d t_i.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.preprojectiveToGinzburgTwoCohomology_preprojectiveMk (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (x : pathAlgebra k (Quiver.Symmetrify Q)) :
    (preprojectiveToGinzburgTwoCohomology k Q) ((preprojectiveMk k Q) x) = (Ideal.Quotient.mk (TwoSidedIdeal.asIdeal ⋯.boundaries)) ⟨(ginzburgMap k) x, ⋯⟩

    The map Π_k(Q) → H(Π₂(Q)) sends the class of a doubled element to the cohomology class of its image in the Ginzburg path algebra.

    source
    noncomputable def TauCeti.ginzburgTwoCohomologyToPreprojective (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] :
    ⋯.Cohomology →ₐ[k] preprojectiveAlgebra k Q

    The algebra homomorphism H(Π₂(Q)) → Π_k(Q) sending the class of a cycle to the class of the doubled element obtained by killing its adjoined loops. It is well defined by TauCeti.preprojectiveMk_ginzburgRetraction_ginzburgTwoDifferential.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem TauCeti.ginzburgTwoCohomologyToPreprojective_mk (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (z : ↥⋯.cycles) :
      (ginzburgTwoCohomologyToPreprojective k Q) ((Ideal.Quotient.mk (TwoSidedIdeal.asIdeal ⋯.boundaries)) z) = (preprojectiveMk k Q) ((ginzburgRetraction k) ↑z)

      The map H(Π₂(Q)) → Π_k(Q) sends the class of a cycle to the class of the doubled element obtained by killing its loops.

      source
      @[simp]
      theorem TauCeti.ginzburgTwoCohomologyToPreprojective_preprojectiveToGinzburgTwoCohomology (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (x : preprojectiveAlgebra k Q) :
      (ginzburgTwoCohomologyToPreprojective k Q) ((preprojectiveToGinzburgTwoCohomology k Q) x) = x

      Π_k(Q) is a retract of H(Π₂(Q)): killing the loops undoes the map Π_k(Q) → H(Π₂(Q)).

      source
      theorem TauCeti.preprojectiveToGinzburgTwoCohomology_injective (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] :
      Function.Injective ⇑(preprojectiveToGinzburgTwoCohomology k Q)

      The map Π_k(Q) → H(Π₂(Q)) is injective.

      source
      theorem TauCeti.mem_range_preprojectiveToGinzburgTwoCohomology_iff (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] {x : ⋯.Cohomology} :
      x ∈ (preprojectiveToGinzburgTwoCohomology k Q).range ↔ x ∈ ⋯.cohomologyGrading 0

      The image of Π_k(Q) in H(Π₂(Q)) is the degree-zero cohomology.

      source
      noncomputable def TauCeti.preprojectiveEquivGinzburgTwoCohomologyZero (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] :
      preprojectiveAlgebra k Q ≃ₐ[k] ↥(⋯.cohomologyGrading 0)

      The zeroth cohomology of the two-dimensional Ginzburg algebra is the preprojective algebra: Π_k(Q) ≃ H⁰(Π₂(Q)) as k-algebras, the class of a doubled path going to the cohomology class of the same path.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem TauCeti.coe_preprojectiveEquivGinzburgTwoCohomologyZero_apply (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (x : preprojectiveAlgebra k Q) :
        ↑((preprojectiveEquivGinzburgTwoCohomologyZero k Q) x) = (preprojectiveToGinzburgTwoCohomology k Q) x

        The isomorphism Π_k(Q) ≃ H⁰(Π₂(Q)) agrees with TauCeti.preprojectiveToGinzburgTwoCohomology after forgetting the degree.

        source
        @[simp]
        theorem TauCeti.preprojectiveEquivGinzburgTwoCohomologyZero_symm_apply (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (z : ↥(⋯.cohomologyGrading 0)) :
        (preprojectiveEquivGinzburgTwoCohomologyZero k Q).symm z = (ginzburgTwoCohomologyToPreprojective k Q) ↑z

        The inverse of Π_k(Q) ≃ H⁰(Π₂(Q)) is TauCeti.ginzburgTwoCohomologyToPreprojective on degree-zero classes.