Transporting finite presentations

Mathlib has two ways of moving a SheafOfModules.Presentation around — along an isomorphism (Presentation.ofIsIso) and along a colimit-preserving functor (Presentation.map). Mathlib v4.32 supplies anonymous instances proving that both preserve Presentation.IsFinite; the named results in this file retain the stable API used by this project.

That gap is why SheafOfModules.IsFinitePresentation has no local-to-global criterion even though IsQuasicoherent does: QuasicoherentData.bind builds its presentations as (P.map _ _).of_isIso _, so without these two instances there is no way to conclude that the glued data is finite.

Both are immediate from the upstream instances.

Main results

• Presentation.isFinite_of_isIso
• Presentation.isFinite_map

This is DerivedAlgGeo-owned compatibility infrastructure. It remains in the SheafOfModules namespace because that is the mathematical owner of the declarations, not because the project is committed to upstreaming it.

theorem SheafOfModules.Presentation.isFinite_of_isIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (f : M ⟶ N) [CategoryTheory.IsIso f] (P : M.Presentation) [P.IsFinite] : (ofIsIso f P).IsFinite

Transporting a presentation along an isomorphism keeps it finite: of_isIso composes the generating and relating maps with an iso and leaves both index types alone.

theorem SheafOfModules.Presentation.isFinite_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {C' : Type u₂} [CategoryTheory.Category.{v₂, u₂} C'] {J' : CategoryTheory.GrothendieckTopology C'} {S : CategoryTheory.Sheaf J' RingCat} [CategoryTheory.HasSheafify J' AddCommGrpCat] [J'.WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (P : M.Presentation) [P.IsFinite] (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S)) [CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, max u u₁, max u u₂, max (max (u + 1) u₁) v₁, max (max (u + 1) u₂) v₂} F] (η : unit S ≅ F.obj (unit R)) : (P.map F η).IsFinite

Transporting a presentation along a colimit-preserving functor keeps it finite: Presentation.map builds the new generators and relations out of the same index types (map_generators_I, map_relations_I).

What these unblock

Presentation.quasicoherentData and QuasicoherentData.bind are both built out of exactly map and of_isIso, so these two instances are what any statement about finite presentation has to go through.

The global case is done in the sibling Presentation/Finite.lean: IsFinitePresentation.of_presentation. Two things were needed on top of the instances here, both recorded there — a hand-supplied preservesColimitsOfSize_shrink, and pinning S when applying isFinite_map, without which J' stays a metavariable and instance synthesis fails with a misleading "missing HasSheafify".

The local-to-global case, IsFinitePresentation.of_coversTop via bind, is implemented in the sibling Presentation/Locality.lean. It needs the same two fixes plus one more: QuasicoherentData.I lives in its own universe w, and bind returns Σ i, (D i).I, so the covering-family index has to remain universe-polymorphic for the w from exists_quasicoherentData to match the w bind produces.

A practical note for that work: introduce local data with choose D hD using …, not have D := ….choose. With have, D i is opaque and choose_spec types against _.choose rather than D i — an error with nothing to do with the real problem.