Documentation

DerivedAlgGeo.Algebra.Category.Grp.Products

The categorical product of abelian groups is the Pi type #

AddCommGrpCat has products — Mathlib.Algebra.Category.Grp.Limits gives it all limits — but nothing identifies ∏ᶜ Z with ∀ i, Z i. Mathlib carries that identification under the name piIsoPi for ModuleCat (Algebra/Category/ModuleCat/Products.lean), TopCat, and Grpd, and for AddCommGrpCat only in the finite biproduct case (biproductIsoPi, over a Fintype index). The infinite-index product form is absent, checked against the pinned revision.

It is needed here because a Čech complex is indexed by Fin (p + 1) → ι with ι the variable type of a polynomial ring, so the index is infinite whenever the ambient projective space is — biproductIsoPi does not apply, and the Čech term of an abelian-group-valued sheaf cannot be compared with an explicit Pi type without it.

The construction is ModuleCat.piIsoPi's, transported: the concrete cone on ∀ i, Z i with the evaluation homomorphisms as projections, shown limiting by the universal property of Pi, then limit.isoLimitCone.

Main declarations #

Implementation notes #

This is owned library code, not a placeholder held open against an upstream fix; no Mathlib PR is planned. If Mathlib does later declare these names, redeclaring them here is a hard error rather than a shadowing warning, so this file is deleted at that point. That can only surface during a deliberate lakefile.toml pin bump, since the Mathlib revision is an exact pin, and the fix is deleting the file — hence the bare AddCommGrpCat namespace is kept rather than hedged behind a repository prefix, per ARCHITECTURE.md.

The trap for a caller is the codomain of piIsoPi. It is the bundled object AddCommGrpCat.of (∀ i, Z i), not the type ∀ i, Z i, so piIsoPi does not compose with an equivalence of Pi types. piAddEquivPi is the form that does.

The elementwise variants piIsoPi_inv_π_apply and piIsoPi_hom_eval_apply are the applied forms a caller indexing into the function type wants. Following Mathlib they are not simp lemmas — neither side of the applied equation is more normal than the other — so use them by name.

Tags #

abelian group, categorical product, limit, concrete category

source
def AddCommGrpCat.productCone {ι : Type v} (Z : ι → AddCommGrpCat) :
CategoryTheory.Limits.Fan Z

The product cone induced by the concrete product.

Equations
Instances For
    source
    def AddCommGrpCat.productConeIsLimit {ι : Type v} (Z : ι → AddCommGrpCat) :
    CategoryTheory.Limits.IsLimit (productCone Z)

    The concrete product cone is limiting.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def AddCommGrpCat.piIsoPi {ι : Type v} (Z : ι → AddCommGrpCat) [CategoryTheory.Limits.HasProduct Z] :
      ∏ᶜ Z ≅ of ((i : ι) → ↑(Z i))

      The categorical product of a family of abelian groups is the Pi type.

      The ModuleCat analogue is ModuleCat.piIsoPi; this is the same statement one forgetful functor further down, and is what lets a Čech term over an infinite index set be named concretely. The codomain is the bundled object, so to compose with an equivalence of function types reach for piAddEquivPi instead.

      Equations
      Instances For
        source
        @[simp]
        theorem AddCommGrpCat.piIsoPi_inv_π {ι : Type v} (Z : ι → AddCommGrpCat) [CategoryTheory.Limits.HasProduct Z] (i : ι) :
        CategoryTheory.CategoryStruct.comp (piIsoPi Z).inv (CategoryTheory.Limits.Pi.π Z i) = ofHom (Pi.evalAddMonoidHom (fun (i : ι) => ↑(Z i)) i)

        The isomorphism is compatible with the projections, in the direction callers need: reading a component off the Pi type agrees with the categorical projection.

        source
        theorem AddCommGrpCat.piIsoPi_inv_π_apply {ι : Type v} (Z : ι → AddCommGrpCat) [CategoryTheory.Limits.HasProduct Z] (i : ι) (x : (i : ι) → ↑(Z i)) :
        (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π Z i)) ((CategoryTheory.ConcreteCategory.hom (piIsoPi Z).inv) x) = x i

        The isomorphism is compatible with the projections, in the direction callers need: reading a component off the Pi type agrees with the categorical projection.

        source
        @[simp]
        theorem AddCommGrpCat.piIsoPi_hom_eval {ι : Type v} (Z : ι → AddCommGrpCat) [CategoryTheory.Limits.HasProduct Z] (i : ι) :
        CategoryTheory.CategoryStruct.comp (piIsoPi Z).hom (ofHom (Pi.evalAddMonoidHom (fun (i : ι) => ↑(Z i)) i)) = CategoryTheory.Limits.Pi.π Z i

        Evaluating at an index after transporting the categorical product into the dependent function type is the categorical projection.

        source
        theorem AddCommGrpCat.piIsoPi_hom_eval_apply {ι : Type v} (Z : ι → AddCommGrpCat) [CategoryTheory.Limits.HasProduct Z] (i : ι) (x : ↑(∏ᶜ Z)) :
        (CategoryTheory.ConcreteCategory.hom (piIsoPi Z).hom) x i = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π Z i)) x

        Evaluating at an index after transporting the categorical product into the dependent function type is the categorical projection.

        source
        noncomputable def AddCommGrpCat.piAddEquivPi {ι : Type v} (Z : ι → AddCommGrpCat) [CategoryTheory.Limits.HasProduct Z] :
        ↑(∏ᶜ Z) ≃+ ((i : ι) → ↑(Z i))

        The categorical product of a family of abelian groups as an AddEquiv onto the Pi type.

        This is piIsoPi with the bundled codomain forgotten. It is the form that composes with equivalences of function types — AddEquiv.piCongrRight and friends — which is what comparing a product-valued complex against a pointwise-defined one needs, and is the shape in which the Čech term meets polynomialVariableCechCochains. Its forward and inverse actions are piIsoPi_hom_eval_apply and piIsoPi_inv_π_apply, which apply to it definitionally.

        Equations
        Instances For