GradedAlgebra.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

11 declarations, 0 contain sorry, 0 declared as axioms

The Yoneda algebra of an object of an abelian category

Let C be an abelian category with HasExt C and let X : C. The Yoneda composition Ext.comp : Ext X X a → Ext X X b → Ext X X (a + b) makes the family fun n ↦ Ext X X n a graded ring, so that ⨁ n, Ext X X n is a ring: the Yoneda algebra Ext^*(X, X) of X. When C is R-linear for a commutative ring R, it is a graded R-algebra. For Y : C, the family fun n ↦ Ext X Y n is a graded module over fun n ↦ Ext X X n, so that ⨁ n, Ext X Y n is a module over ⨁ n, Ext X X n.

Main declarations

CategoryTheory.Abelian.Ext.instGRing: the graded ring structure on fun n ↦ Ext X X n.
CategoryTheory.Abelian.Ext.instGAlgebra: the graded R-algebra structure on fun n ↦ Ext X X n when C is R-linear.
CategoryTheory.Abelian.Ext.instGmodule: the graded module structure on fun n ↦ Ext X Y n over fun n ↦ Ext X X n.

The proofs of the graded axioms compare elements of GradedMonoid in different degrees; they use GradedMonoid.mk_eq_mk and Ext.comp_heq to reduce these to equalities in a single degree.

Imports (4)

Imported by 2 files

lemma CategoryTheory.Abelian.Ext.comp_heq Up to HEq, the composition Ext.comp does not depend on the proof of the degree equation line 61 source
Source documentation
Up to HEq, the composition Ext.comp does not depend on the proof of the degree equation.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CategoryTheory.Category, CategoryTheory.Abelian, CategoryTheory.HasExt, Nat, CategoryTheory.Abelian.Ext, Eq, HAdd.hAdd, HEq, CategoryTheory.Abelian.Ext.comp
Proof uses: Eq.rec, Eq.refl, HEq.rfl
4 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma comp_heq {a b c c' : ℕ} (α : Ext X Y a) (β : Ext Y Z b) (h : a + b = c)
    (h' : a + b = c') : HEq (α.comp β h) (α.comp β h') := by
…
```
Mentions: c
instance CategoryTheory.Abelian.Ext.instGOne line 70 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CategoryTheory.Category, CategoryTheory.Abelian, CategoryTheory.HasExt, GradedMonoid.GOne, Nat, CategoryTheory.Abelian.Ext
Proof uses: GradedMonoid.GOne.mk, CategoryTheory.Abelian.Ext.mk₀, CategoryTheory.CategoryStruct.id
5 instances, coercions and auxiliary constants left out.
instance CategoryTheory.Abelian.Ext.instGMul line 73 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CategoryTheory.Category, CategoryTheory.Abelian, CategoryTheory.HasExt, GradedMonoid.GMul, Nat, CategoryTheory.Abelian.Ext
Proof uses: GradedMonoid.GMul.mk, CategoryTheory.Abelian.Ext.comp, HAdd.hAdd
4 instances, coercions and auxiliary constants left out.
instance CategoryTheory.Abelian.Ext.instGSMul line 76 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CategoryTheory.Category, CategoryTheory.Abelian, CategoryTheory.HasExt, GradedMonoid.GSMul, Nat, CategoryTheory.Abelian.Ext
Proof uses: GradedMonoid.GSMul.mk, CategoryTheory.Abelian.Ext.comp, HVAdd.hVAdd
6 instances, coercions and auxiliary constants left out.
lemma CategoryTheory.Abelian.Ext.gOne_eq line 82 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CategoryTheory.Category, CategoryTheory.Abelian, CategoryTheory.HasExt, Eq, CategoryTheory.Abelian.Ext, OfNat.ofNat, Nat, GradedMonoid.GOne.one, CategoryTheory.Abelian.Ext.mk₀, CategoryTheory.CategoryStruct.id
Proof uses: rfl
9 instances, coercions and auxiliary constants left out.
lemma CategoryTheory.Abelian.Ext.gMul_eq line 85 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CategoryTheory.Category, CategoryTheory.Abelian, CategoryTheory.HasExt, Nat, CategoryTheory.Abelian.Ext, Eq, HAdd.hAdd, GradedMonoid.GMul.mul, CategoryTheory.Abelian.Ext.comp, rfl
6 instances, coercions and auxiliary constants left out.
lemma CategoryTheory.Abelian.Ext.gSMul_eq line 89 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CategoryTheory.Category, CategoryTheory.Abelian, CategoryTheory.HasExt, Nat, CategoryTheory.Abelian.Ext, Eq, HVAdd.hVAdd, GradedMonoid.GSMul.smul, CategoryTheory.Abelian.Ext.comp, HAdd.hAdd, rfl
9 instances, coercions and auxiliary constants left out.
instance CategoryTheory.Abelian.Ext.instGMonoid line 94 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CategoryTheory.Category, CategoryTheory.Abelian, CategoryTheory.HasExt, GradedMonoid.GMonoid, Nat, CategoryTheory.Abelian.Ext
Proof uses: GradedMonoid.GMonoid.mk, GradedMonoid.GMonoid.gnpowRec
9 instances, coercions and auxiliary constants left out.
instance CategoryTheory.Abelian.Ext.instGRing line 102 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CategoryTheory.Category, CategoryTheory.Abelian, CategoryTheory.HasExt, DirectSum.GRing, Nat, CategoryTheory.Abelian.Ext
Proof uses: DirectSum.GRing.mk, DirectSum.GSemiring.mk, DirectSum.GNonUnitalNonAssocSemiring.mk, GradedMonoid.GMonoid.gnpow, HSMul.hSMul, OfNat.ofNat, CategoryTheory.Abelian.Ext.mk₀, CategoryTheory.CategoryStruct.id, Int
33 instances, coercions and auxiliary constants left out.
instance CategoryTheory.Abelian.Ext.instGmodule line 114 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CategoryTheory.Category, CategoryTheory.Abelian, CategoryTheory.HasExt, DirectSum.Gmodule, Nat, CategoryTheory.Abelian.Ext
Proof uses: DirectSum.Gmodule.mk, DirectSum.GdistribMulAction.mk, GradedMonoid.GMulAction.mk
23 instances, coercions and auxiliary constants left out.
instance CategoryTheory.Abelian.Ext.instGAlgebra line 126 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CategoryTheory.Category, CategoryTheory.Abelian, CategoryTheory.HasExt, CommRing, CategoryTheory.Linear, DirectSum.GAlgebra, Nat, CategoryTheory.Abelian.Ext
Proof uses: DirectSum.GAlgebra.mk, AddMonoidHom.mk, OfNat.ofNat, ZeroHom.mk, CategoryTheory.Abelian.Ext.mk₀, HSMul.hSMul, Quiver.Hom, CategoryTheory.CategoryStruct.id
48 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.