Theorems · Theorem · category theory

ModuleCat.piIsoPi_hom_ker_subtype

∀ {R : Type u} [inst : Ring R] {ι : Type v} (Z : ι → ModuleCat R) [inst_1 : CategoryTheory.Limits.HasProduct Z] (i : ι),
  CategoryTheory.CategoryStruct.comp (ModuleCat.piIsoPi Z).hom (ModuleCat.ofHom (LinearMap.proj i)) =
    CategoryTheory.Limits.Pi.π Z i

Defined in: Mathlib.Algebra.Category.ModuleCat.Products
Cited by: 1 results in Mathlib
Foundations: Depth 34 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Ring CategoryTheory.Limits.HasProduct

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites19

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Quiver.Homstatement · cited by 32,603
CategoryTheory.CategoryStruct.compstatement · cited by 17,999
CategoryTheory.Iso.homstatement · cited by 7,684
Ringstatement and proof · cited by 7,463
ModuleCatstatement and proof · cited by 1,429
ModuleCat.carrierstatement · cited by 997
CategoryTheory.Discrete.functorproof · cited by 633
ModuleCat.ofstatement · cited by 594
CategoryTheory.Limits.piObjstatement · cited by 237
ModuleCat.ofHomstatement · cited by 200
CategoryTheory.Limits.Pi.πstatement · cited by 184
CategoryTheory.Limits.limit.isLimitproof · cited by 146

Cited by1

Results whose statement or proof uses this declaration.

ModuleCat.piIsoPi_hom_ker_subtype_applyproof · cited by 0