The Euler class of a finite projective resolution, and the resolution theorem #
Let E be an exact structure on an additive category C and let P be a property of objects
consisting of E-projectives, containing a zero object and closed under binary biproducts. Then
P is extension closed, so the full subcategory on P carries an induced exact structure — in
fact the split one — and every finite P-resolution
Kₙ ↪ Qₙ₋₁ ↠ Kₙ₋₁, …, K₁ ↪ Q₀ ↠ X
has an alternating class [Q₀] - [Q₁] + ⋯ + (-1)ⁿ [Kₙ] in the exact K₀ of that subcategory.
Unlike the ambient class of TauCeti/CategoryTheory/GrothendieckGroup/Resolution.lean, which
telescopes to [X] and is therefore independent of every choice for trivial reasons, this class
is not visibly determined by X: nothing in the subcategory relates [Q₀] - [K₁] to X.
That it is determined by X is the content of this file. Schanuel's lemma turns two first
steps K ↪ Q ↠ X and K' ↪ Q' ↠ X into an isomorphism K ⊞ Q' ≅ K' ⊞ Q, and an induction on
the sum of the two lengths does the rest. The horseshoe lemma then makes the resulting invariant
additive on conflations, so it factors through the exact K₀ of the objects of finite
P-dimension and inverts the map induced by the inclusion: this is Weibel's resolution
theorem in the projective case.
Main definitions #
TauCeti.ExactStructure.FiniteResolution.eulerClassFullSubcategory: the alternating class of a finiteP-resolution, in the exactK₀of the exact structure induced on the full subcategory onP. On top of the additivity hypotheses assumed throughout, its definition needs only extension closure ofP, not projectivity.TauCeti.ExactStructure.resolutionEquiv: the isomorphism of the resolution theorem.
Main results #
TauCeti.ExactStructure.FiniteResolution.eulerClassFullSubcategory_eq_eulerClassFullSubcategory: the Euler class depends only on the resolved object, by Schanuel's lemma.TauCeti.ExactStructure.eulerClassOf_eq_sub_of_conflationandTauCeti.ExactStructure.eulerClassOf_eq_add_of_conflation: the Euler class drops by one step along a conflation with resolving middle term, and is additive on conflations. The second is the horseshoe lemma, iterated.TauCeti.ExactStructure.map_eulerClassFullSubcategory_eq_of: in the exactK₀of the objects of finiteP-dimension the alternating class of a resolution ofXis[X].TauCeti.ExactStructure.resolutionEquiv,TauCeti.ExactStructure.resolutionEquiv_ofandTauCeti.ExactStructure.resolutionEquiv_symm_of: the resolution theorem. The inclusion of the full subcategory onPinto the objects admitting a finiteP-resolution induces an isomorphism on exactK₀, whose inverse is the Euler class.
Implementation notes #
The well-definedness, conflation-additivity, and resolution-theorem results here carry
P ≤ E.isProjective as an explicit hypothesis. On top of ContainsZero and
IsClosedUnderBinaryProducts, which are assumed throughout, the underlying Euler-class definitions
and formal computation lemmas need only extension closure. The resolution theorem for a resolving
subcategory, where every object of the ambient category has a finite resolution and Schanuel's
lemma and the horseshoe are replaced by pullbacks of deflations and dimension shifting, is
TauCeti.ExactStructure.IsResolving.resolutionEquiv in
TauCeti/CategoryTheory/GrothendieckGroup/Resolving.lean. The projective case proved here needs
no kernel closure and resolves only the objects of finite P-dimension.
The class of an object, as opposed to that of a resolution, is
TauCeti.ExactStructure.eulerClassOf of
TauCeti/CategoryTheory/GrothendieckGroup/Resolution.lean, defined by choosing a resolution with
Nonempty.some; TauCeti.ExactStructure.eulerClassOf_eq immediately removes the choice under the
projectivity hypothesis, so no result below depends on it.
Two inductions are carried out on a numerical bound rather than on the resolutions themselves:
the well-definedness induction consumes the sum of the two lengths, because Schanuel's lemma
replaces both chains at once, and the additivity induction consumes a common bound for the two
outer lengths, because the horseshoe replaces both at once. Both are stated as private
auxiliaries over an explicit n.
References #
- Charles A. Weibel, The K-book: An Introduction to Algebraic K-theory, Chapter II, Theorem 7.6 and Lemma 7.6.1: the resolution theorem and the independence of the Euler class.
- Theo Bühler, Exact categories, Expositiones Mathematicae 28 (2010), 1--69, Sections 11--12, for Schanuel's lemma and the horseshoe lemma in a Quillen exact category.
- The Tau Ceti Grothendieck groups, Cartan maps, and Euler forms roadmap, Layer 3, whose Euler-class and resolution-theorem bullets are the targets proved here in the projective case, and whose Layer 4 Cartan comparison consumes them.
A property containing a zero object and closed under binary products is automatically
replete, by CategoryTheory.ObjectProperty.isClosedUnderIsomorphisms_of_containsZero.
The Euler class in the K₀ of the full subcategory on P depends only on the resolved
object. Any two finite P-resolutions of the same object have the same alternating class in the
exact K₀ of the canonically induced structure on P, as soon as every object satisfying P is
E-projective.
The proof is an induction on the sum of the two lengths whose only geometric input is Schanuel's
lemma TauCeti.ExactStructure.nonempty_iso_biprod_of_projective: it turns the two first steps
K ↪ Q ↠ X and K' ↪ Q' ↠ X into an isomorphism K ⊞ Q' ≅ K' ⊞ Q, and the two remaining
chains, each enlarged by the other's resolving term, resolve the two sides.
Every finite P-resolution of X computes TauCeti.ExactStructure.eulerClassOf.
On an object satisfying P the Euler class is the class of that object.
The Euler class drops by one step along a conflation with resolving middle term:
χ(X) = [Q] - χ(K) for a conflation K ↪ Q ↠ X with P Q.
The Euler class is additive on conflations. This is the second half of the Euler-class
package: together with TauCeti.ExactStructure.eulerClassOf_eq it makes the alternating class of
a finite projective resolution a conflation-additive invariant of the objects of finite
P-dimension.
The Euler class is invariant under isomorphism of the resolved object.
The class of an object of finite P-dimension is the alternating class of any of its
finite P-resolutions, after pushing the latter forward along the inclusion. This is the
telescoping computation of TauCeti.ExactStructure.FiniteResolution.eulerClass_eq_of, carried
out in the exact K₀ of the objects of finite P-dimension rather than in that of the whole
ambient category.
The inverse of the comparison map of the resolution theorem: the homomorphism sending the
class of an object of finite P-dimension to the alternating class of any of its finite
P-resolutions.
Equations
Instances For
The resolution theorem for finite projective resolutions. When every object satisfying
P is E-projective, the inclusion of the full subcategory on P into the full subcategory of
objects admitting a finite P-resolution induces an isomorphism of exact Grothendieck groups.
Its inverse sends the class of an object to the alternating class of any finite P-resolution of
it, by TauCeti.ExactStructure.resolutionEquiv_symm_of.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The forward map of the resolution equivalence sends a P-object to its class in the full
subcategory of objects admitting a finite P-resolution.
The inverse map of the resolution equivalence sends an object class to its Euler class.