DG and A-infinity algebras, categories, and modules

The declarations the status of Tau Ceti's roadmap names as Tau Ceti has them at commit ace60277.

DefinitionTauCeti.AInfinityAlgebra.minimalModel #

The minimal A∞ model on cohomology obtained by homogeneous transfer.

TauCeti.AInfinityAlgebra.minimalModel.{uK, uA} {K : Type uK} {A : Type uA} [Field K]
  [AddCommGroup A] [_root_.Module K A] (𝒜 : TauCeti.AInfinityAlgebra K A) :
  TauCeti.AInfinityAlgebra K 𝒜.Cohomology

Lean

Formalized in Tau Ceti as TauCeti.AInfinityAlgebra.minimalModel.

Sources

LeanTauCeti.AInfinityAlgebra.minimalModel

Uses 1 · Used by 2

Statement usesTauCeti.AInfinityAlgebra.transfer

Used byKadeishvili's intrinsic formality criterion · The triple Massey product is a coset of the minimal-model ternary operation

TheoremKadeishvili's intrinsic formality criterion #

Over a field, a graded algebra ℋ, presented as a minimal A∞ algebra without operations above arity two, is intrinsically formal when HH^{n, 2 - n}(H, H) = 0 for every n ≥ 3: every Hochschild cocycle of ℋ of suspended degree one concentrated on the words of length n is the Hochschild differential of a cochain of suspended degree zero concentrated on the words of length n - 1.

TauCeti.AInfinityAlgebra.isIntrinsicallyFormal_of_forall_hochschildVanishesAt.{uK, uA} {K : Type uK}
  {A : Type uA} [Field K] [AddCommGroup A] [_root_.Module K A] {ℋ : TauCeti.AInfinityAlgebra K A}
  (hℋ : ℋ.IsMinimal) (hm : ∀ (n : ℕ), 3 ≤ n → ℋ.m n = 0)
  (hHH : ∀ (n : ℕ) (hn : 3 ≤ n), ℋ.HochschildVanishesAt ⟨n, ⋯⟩) : ℋ.IsIntrinsicallyFormal

Lean

Formalized in Tau Ceti as TauCeti.AInfinityAlgebra.isIntrinsicallyFormal_of_forall_hochschildVanishesAt.

Other forms

Kadeishvili's intrinsic formality criterion, over any commutative ring. Formalized in Tau Ceti as TauCeti.AInfinityAlgebra.IsMinimal.exists_isIso_of_forall_hochschildVanishesAt.

TauCeti.AInfinityAlgebra.IsMinimal.exists_isIso_of_forall_hochschildVanishesAt.{uR, uA}
  {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [_root_.Module R A]
  {ℋ ℬ : TauCeti.AInfinityAlgebra R A} (hℬ : ℬ.IsMinimal) (hℋ : ℋ.IsMinimal)
  (hm : ∀ (n : ℕ), 3 ≤ n → ℋ.m n = 0) (hG : ℬ.grading = ℋ.grading) (h₂ : ℬ.m 2 = ℋ.m 2)
  (hHH : ∀ (n : ℕ) (hn : 3 ≤ n), ℋ.HochschildVanishesAt ⟨n, ⋯⟩) : ∃ f, f.IsIso

Sources

LeanTauCeti.AInfinityAlgebra.isIntrinsicallyFormal_of_forall_hochschildVanishesAt · TauCeti.AInfinityAlgebra.IsMinimal.exists_isIso_of_forall_hochschildVanishesAt

Uses 2

Proof usesTauCeti.AInfinityAlgebra.minimalModel · TauCeti.AInfinityAlgebra.transfer

TheoremThe triple Massey product is a coset of the minimal-model ternary operation #

if x y = 0 and y z = 0, then w lies in ⟨x, y, z⟩ exactly when w - m₃^H (x, y, z) lies in the indeterminacy τx · H + H · z.

TauCeti.AInfinityAlgebra.mem_tripleMasseyProduct_iff_sub_minimalModel_m_three_mem.{uK, uA}
  {K : Type uK} {A : Type uA} [Field K] [AddCommGroup A] [_root_.Module K A]
  (𝒜 : TauCeti.AInfinityAlgebra K A) {x y z w : 𝒜.Cohomology} (hxy : x * y = 0) (hyz : y * z = 0) :
  w ∈ 𝒜.tripleMasseyProduct x y z ↔
    w - (𝒜.minimalModel.m 3) ![x, y, z] ∈ 𝒜.tripleMasseyIndeterminacy x z

Lean

Formalized in Tau Ceti as TauCeti.AInfinityAlgebra.mem_tripleMasseyProduct_iff_sub_minimalModel_m_three_mem.

Sources

LeanTauCeti.AInfinityAlgebra.mem_tripleMasseyProduct_iff_sub_minimalModel_m_three_mem

Uses 2

Statement usesTauCeti.AInfinityAlgebra.minimalModel

Proof usesTauCeti.AInfinityAlgebra.transfer

TheoremThe transferred ternary operation on `([a], [a], [b])`#

m₃^H ([a], [a], [b]) = [a c]. Of the Kontsevich--Soibelman/Merkulov tree sum only the term -p m₂ (i (τ [a]), h m₂ (i [a], i [b])) survives, with h (a b) = c and the Koszul twist τ [a] = -[a].

TauCeti.HeisenbergDGA.minimalModel_m_three.{u_1} (R : Type u_1) [CommRing R] :
  ((TauCeti.HeisenbergDGA.minimalModel R).m 3)
      ![(TauCeti.HeisenbergDGA.aInfinityAlgebra R).cohomologyClass ⋯,
        (TauCeti.HeisenbergDGA.aInfinityAlgebra R).cohomologyClass ⋯,
        (TauCeti.HeisenbergDGA.aInfinityAlgebra R).cohomologyClass ⋯] =
    (TauCeti.HeisenbergDGA.aInfinityAlgebra R).cohomologyClass ⋯

Lean

Formalized in Tau Ceti as TauCeti.HeisenbergDGA.minimalModel_m_three.

Sources

LeanTauCeti.HeisenbergDGA.minimalModel_m_three

Uses 1

Statement usesTauCeti.AInfinityAlgebra.transfer

DefinitionTauCeti.AInfinityAlgebra.transfer #

The transferred A∞ structure on the retract H of a special contraction of (A, m₁): its Taylor map is the letter component of the transferred bar differential.

TauCeti.AInfinityAlgebra.transfer.{uR, uA, uH} {R : Type uR} {A : Type uA} {H : Type uH}
  [CommRing R] [AddCommGroup A] [_root_.Module R A] [AddCommGroup H] [_root_.Module R H]
  (𝒜 : TauCeti.AInfinityAlgebra R A) {GH : TauCeti.InternalGrading R H ℤ} {dH : Module.End R H}
  (c : TauCeti.LinearSpecialContraction 𝒜.differential dH)
  (hh : TauCeti.LinearMap.IsHomogeneous c.homotopy (𝒜.grading.piece ℤ) (𝒜.grading.piece ℤ) (-1))
  (hincl : TauCeti.LinearMap.IsHomogeneous c.incl (GH.piece ℤ) (𝒜.grading.piece ℤ) 0)
  (hproj : TauCeti.LinearMap.IsHomogeneous c.proj (𝒜.grading.piece ℤ) (GH.piece ℤ) 0) :
  TauCeti.AInfinityAlgebra R H

Lean

Formalized in Tau Ceti as TauCeti.AInfinityAlgebra.transfer.

Sources

LeanTauCeti.AInfinityAlgebra.transfer

Used by 6

Used byKadeishvili's intrinsic formality criterion · TauCeti.AInfinityAlgebra.minimalModel · TauCeti.AInfinityAlgebra.transferHomotopy · TauCeti.AInfinityCategory.transfer · The transferred ternary operation on ([a], [a], [b]) · The triple Massey product is a coset of the minimal-model ternary operation

DefinitionTauCeti.AInfinityAlgebra.transferHomotopy #

The homotopy from the identity of an A-infinity algebra to its transferred inclusion composed with its transferred projection. On bar constructions this is K - K X K, where K is the tensor-trick homotopy and X the perturbation operator.

TauCeti.AInfinityAlgebra.transferHomotopy.{uR, uA, uH} {R : Type uR} {A : Type uA} {H : Type uH}
  [CommRing R] [AddCommGroup A] [_root_.Module R A] [AddCommGroup H] [_root_.Module R H]
  (𝒜 : TauCeti.AInfinityAlgebra R A) {GH : TauCeti.InternalGrading R H ℤ} {dH : Module.End R H}
  (c : TauCeti.LinearSpecialContraction 𝒜.differential dH)
  (hh : TauCeti.LinearMap.IsHomogeneous c.homotopy (𝒜.grading.piece ℤ) (𝒜.grading.piece ℤ) (-1))
  (hincl : TauCeti.LinearMap.IsHomogeneous c.incl (GH.piece ℤ) (𝒜.grading.piece ℤ) 0)
  (hproj : TauCeti.LinearMap.IsHomogeneous c.proj (𝒜.grading.piece ℤ) (GH.piece ℤ) 0) :
  (TauCeti.AInfinityHom.id 𝒜).Homotopy
    ((𝒜.transferInclusion c hh hincl hproj).comp (𝒜.transferProjection c hh hincl hproj))

Lean

Formalized in Tau Ceti as TauCeti.AInfinityAlgebra.transferHomotopy.

Sources

LeanTauCeti.AInfinityAlgebra.transferHomotopy

Uses 1

Statement usesTauCeti.AInfinityAlgebra.transfer

DefinitionTauCeti.AInfinityCategory.transfer #

The transferred A∞ category: the A∞ structure transferred from the total algebra of morphisms of 𝒞 along a special contraction onto the total module of morphisms of D which is compatible with the hom modules along a bijection of objects e : D ≃ C. Its differential is the differential d_D of the retract (homInclusion_homDifferential_transfer), its composition is g ∘ f = p m₂(i g, i f) (homInclusion_comp_transfer), and its higher operations are those of the transferred A∞ algebra.

TauCeti.AInfinityCategory.transfer.{u₁, u₂, v₁, v₂, w} {R : Type w} [CommRing R] {C : Type u₁}
  {D : Type u₂} [TauCeti.GradedLinearQuiver R C] [TauCeti.GradedLinearQuiver R D]
  (𝒞 : TauCeti.AInfinityCategory R C) (e : D ≃ C)
  {dD : Module.End R (TauCeti.GradedLinearQuiver.TotalHom R D)}
  (c : TauCeti.LinearSpecialContraction 𝒞.differential dD)
  (hh : TauCeti.LinearMap.IsHomogeneous c.homotopy (𝒞.grading.piece ℤ) (𝒞.grading.piece ℤ) (-1))
  (hincl :
    TauCeti.LinearMap.IsHomogeneous c.incl ((TauCeti.GradedLinearQuiver.totalGrading R D).piece ℤ)
      (𝒞.grading.piece ℤ) 0)
  (hproj :
    TauCeti.LinearMap.IsHomogeneous c.proj (𝒞.grading.piece ℤ)
      ((TauCeti.GradedLinearQuiver.totalGrading R D).piece ℤ) 0)
  (hc : TauCeti.LinearSpecialContraction.IsHomCompatible e c) : TauCeti.AInfinityCategory R D

Lean

Formalized in Tau Ceti as TauCeti.AInfinityCategory.transfer.

Sources

LeanTauCeti.AInfinityCategory.transfer

Uses 1

Statement usesTauCeti.AInfinityAlgebra.transfer

DefinitionThe Yoneda lemma for right `A∞` modules #

Over an A∞ algebra with a strict unit e, for a module on which e is a right unit for the binary operation, evaluation at e is a homotopy equivalence from the morphism complex out of the free module of rank one to the underlying complex of the module, with homotopy inverse the Yoneda cochains.

TauCeti.AInfinityRightModule.yonedaHomotopyEquiv.{u} {R A M : Type u} [CommRing R] [AddCommGroup A]
  [_root_.Module R A] [AddCommGroup M] [_root_.Module R M] {AA : TauCeti.AInfinityAlgebra R A}
  (MM : TauCeti.AInfinityRightModule AA M) {e : A} (he : AA.StrictUnit e)
  (hM : ∀ (x : M), ((MM.m 2) x) ![e] = x) :
  HomotopyEquiv (AA.toRightModule.homComplex MM) MM.cochainComplex

Lean

Formalized in Tau Ceti as TauCeti.AInfinityRightModule.yonedaHomotopyEquiv.

Sources

LeanTauCeti.AInfinityRightModule.yonedaHomotopyEquiv

DefinitionThe Yoneda lemma for right DG modules #

DG natural transformations Hom(-, X) ⟶ F are the closed degree-zero elements of F(X). A transformation goes to the image of the identity of X under its component at X (TauCeti.dgYonedaEquiv_apply_coe), and a closed element x goes to the transformation sending g : Y ⟶ X to F(g)(x) (TauCeti.dgApp_dgYonedaEquiv_symm_v).

TauCeti.dgYonedaEquiv.{v, u} {R : Type v} [CommRing R] {C : Type u} [TauCeti.DGCategory R C] (X : C)
  (F :
    CategoryTheory.EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) Cᵒᵖ
      (CochainComplex (ModuleCat R) ℤ)) :
  TauCeti.DGNatTrans (TauCeti.dgRepresentable R X) F ≃
    ↥(ModuleCat.Hom.hom ((F.obj (Opposite.op X)).d 0 1)).ker

Lean

Formalized in Tau Ceti as TauCeti.dgYonedaEquiv.

Sources

LeanTauCeti.dgYonedaEquiv

StructureTauCeti.AInfinityFunctor #

An A∞ functor between nonunital A∞ categories ℬ on C and 𝒞 on D: a map of objects obj : C → D together with an A∞ morphism from the total algebra of morphisms of ℬ to that of the induced category 𝒞.induced obj, whose components send a composable string of C to a morphism between the images of its endpoints and every other string to zero. Its component of arity n on a composable string X₀, …, Xₙ is the functor component fₙ : Hom(Xₙ₋₁, Xₙ) ⊗ ⋯ ⊗ Hom(X₀, X₁) ⟶ Hom(obj X₀, obj Xₙ) of degree 1 - n.

TauCeti.AInfinityFunctor.{u₁, u₂, v₁, v₂, w} {R : Type w} [CommRing R] {C : Type u₁} {D : Type u₂}
  [TauCeti.GradedLinearQuiver R C] [TauCeti.GradedLinearQuiver R D]
  (ℬ : TauCeti.AInfinityCategory R C) (𝒞 : TauCeti.AInfinityCategory R D) :
  Type (max (max (max (max u₁ u₂) v₁) v₂) w)

Lean

Formalized in Tau Ceti as TauCeti.AInfinityFunctor.

Sources

LeanTauCeti.AInfinityFunctor

TheoremThe Hochschild differential squares to zero #

[m, [m, F]] = 0 for every cochain F of degree q.

TauCeti.AInfinityAlgebra.hochschildDifferential_hochschildDifferential.{uR, uA} {R : Type uR}
  {A : Type uA} [CommRing R] [AddCommGroup A] [_root_.Module R A] (𝒜 : TauCeti.AInfinityAlgebra R A)
  {q : ℤ} {F : TauCeti.ReducedTensorWords R A →ₗ[R] A}
  (hF :
    TauCeti.LinearMap.IsHomogeneous F (TauCeti.ReducedTensorWords.gradedPiece (𝒜.grading.shift 1))
      ((𝒜.grading.shift 1).piece ℤ) q) :
  𝒜.hochschildDifferential (1 + q) (𝒜.hochschildDifferential q F) = 0

Lean

Formalized in Tau Ceti as TauCeti.AInfinityAlgebra.hochschildDifferential_hochschildDifferential.

Sources

LeanTauCeti.AInfinityAlgebra.hochschildDifferential_hochschildDifferential

StructureTauCeti.DGTwistedObject #

A twisted object of a differential graded category: an object obj with a degree-one endomorphism twist satisfying the Maurer–Cartan equation d δ = dgComp δ δ, which in Keller's order is d δ + δ ∘ δ = 0. The twisted objects form a differential graded category whose Hom complexes carry the twisted differential; see TauCeti.DGTwistedObject.homComplexData.

TauCeti.DGTwistedObject.{v, u} (R : Type v) [CommRing R] (C : Type u) [TauCeti.DGCategory R C] :
  Type (max u v)

Lean

Formalized in Tau Ceti as TauCeti.DGTwistedObject.

Sources

LeanTauCeti.DGTwistedObject

Used by 1

Used byTauCeti.DGTwistedObject.cone

AbbreviationTauCeti.DGTwistedObject.cone #

The cone of a closed degree-zero morphism u : P ⟶ Q of twisted objects: the twisted object (Q ⊕ P⟦1⟧, δ) whose twisting matrix has the twists of Q and P⟦1⟧ on the diagonal and the morphism P⟦1⟧ ⟶ P ⟶ Q underlying u in the block from P⟦1⟧ to Q.

TauCeti.DGTwistedObject.cone.{v, u} {R : Type v} [CommRing R] {C : Type u} [TauCeti.DGCategory R C]
  {P Q : TauCeti.DGTwistedObject R (TauCeti.DGAdditiveClosure (TauCeti.DGShiftClosure C))}
  (u : TauCeti.DGHom R 0 P Q) (hu : (TauCeti.dgDifferential R 0) u = 0) :
  TauCeti.DGTwistedObject R (TauCeti.DGAdditiveClosure (TauCeti.DGShiftClosure C))

Lean

Formalized in Tau Ceti as TauCeti.DGTwistedObject.cone.

Sources

LeanTauCeti.DGTwistedObject.cone

Uses 1

Statement usesTauCeti.DGTwistedObject

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

DG and A-infinity algebras, categories, and modules

DefinitionTauCeti.AInfinityAlgebra.minimalModel#

Lean

Sources

TheoremKadeishvili's intrinsic formality criterion#

Lean

Other forms

Sources

TheoremThe triple Massey product is a coset of the minimal-model ternary operation#

Lean

Sources

TheoremThe transferred ternary operation on ([a], [a], [b])#

Lean

Sources

DefinitionTauCeti.AInfinityAlgebra.transfer#

Lean

Sources

DefinitionTauCeti.AInfinityAlgebra.transferHomotopy#

Lean

Sources

DefinitionTauCeti.AInfinityCategory.transfer#

Lean

Sources

DefinitionThe Yoneda lemma for right A∞ modules#

Lean

Sources

DefinitionThe Yoneda lemma for right DG modules#

Lean

Sources

StructureTauCeti.AInfinityFunctor#

Lean

Sources

TheoremThe Hochschild differential squares to zero#

Lean

Sources

StructureTauCeti.DGTwistedObject#

Lean

Sources

AbbreviationTauCeti.DGTwistedObject.cone#

Lean

Sources

DefinitionTauCeti.AInfinityAlgebra.minimalModel #

TheoremKadeishvili's intrinsic formality criterion #

TheoremThe triple Massey product is a coset of the minimal-model ternary operation #

TheoremThe transferred ternary operation on `([a], [a], [b])`#

DefinitionTauCeti.AInfinityAlgebra.transfer #

DefinitionTauCeti.AInfinityAlgebra.transferHomotopy #

DefinitionTauCeti.AInfinityCategory.transfer #

DefinitionThe Yoneda lemma for right `A∞` modules #

DefinitionThe Yoneda lemma for right DG modules #

StructureTauCeti.AInfinityFunctor #

TheoremThe Hochschild differential squares to zero #

StructureTauCeti.DGTwistedObject #

AbbreviationTauCeti.DGTwistedObject.cone #