Direct limit of algebraic structures #
We introduce all kinds of algebraic instances on DirectLimit
, and specialize to the cases
of modules and rings, showing that they are indeed colimits in the respective categories.
Implementation notes #
The first 400 lines are boilerplate code that defines algebraic instances on DirectLimit
from magma (Mul
) to Field
. To make everything "hom-polymorphic", we work with DirectedSystem
s
of FunLike
s rather than plain unbundled functions, and we use algebraic hom typeclasses
(e.g. LinearMapClass
, RingHomClass
) everywhere.
In Mathlib.Algebra.Colimit.ModuleRing
, Module.DirectLimit
, AddCommGroup.DirectLimit
and
Ring.DirectLimit
are defined as quotients of the universal objects (DirectSum
and
FreeCommRing
). These definitions are more general and suitable for arbitrary colimits,
but do not immediately provide criteria to determine when two elements in a component are equal
in the direct limit.
On the other hand, the DirectLimit
in this file is only defined for directed systems
and does not work for general colimits, but the equivalence relation defining DirectLimit
is very explicit. For colimits of directed systems there is no need to construct the
universal object for each type of algebraic structure; the same type DirectLimit
simply
works for all of them. This file is therefore more general than the ModuleRing
file in
terms of the variety of algebraic structures supported.
So far we only show that DirectLimit
is the colimit in the categories of modules and rings,
but for the other algebraic structures the constructions and proofs will be easy following
the same pattern. Since any two colimits are isomorphic, this allows us to golf proofs of
equality criteria for Module/AddCommGroup/Ring.DirectLimit
.
Equations
- DirectLimit.instOne = { one := DirectLimit.map₀ f fun (x : ι) => 1 }
Equations
- DirectLimit.instZero = { zero := DirectLimit.map₀ f fun (x : ι) => 0 }
Equations
- DirectLimit.instMul = { mul := DirectLimit.map₂ f f f (fun (x : ι) (x1 x2 : G x) => x1 * x2) ⋯ }
Equations
- DirectLimit.instAdd = { add := DirectLimit.map₂ f f f (fun (x : ι) (x1 x2 : G x) => x1 + x2) ⋯ }
Equations
- DirectLimit.instCommMagmaOfMulHomClass = CommMagma.mk ⋯
Equations
- DirectLimit.instAddCommMagmaOfAddHomClass = AddCommMagma.mk ⋯
Equations
- DirectLimit.instSemigroupOfMulHomClass = Semigroup.mk ⋯
Equations
- DirectLimit.instAddSemigroupOfAddHomClass = AddSemigroup.mk ⋯
Equations
- DirectLimit.instCommSemigroupOfMulHomClass = CommSemigroup.mk ⋯
Equations
- DirectLimit.instAddCommSemigroupOfAddHomClass = AddCommSemigroup.mk ⋯
Equations
- DirectLimit.instSMul = { smul := fun (r : R) => DirectLimit.map f f (fun (x : ι) (x_1 : G x) => r • x_1) ⋯ }
Equations
- DirectLimit.instVAdd = { vadd := fun (r : R) => DirectLimit.map f f (fun (x : ι) (x_1 : G x) => r +ᵥ x_1) ⋯ }
Equations
- DirectLimit.instMulActionOfMulActionHomClass = MulAction.mk ⋯ ⋯
Equations
- DirectLimit.instAddActionOfAddActionHomClass = AddAction.mk ⋯ ⋯
Equations
- DirectLimit.instMulOneClassOfMonoidHomClass = MulOneClass.mk ⋯ ⋯
Equations
- DirectLimit.instAddZeroClassOfAddMonoidHomClass = AddZeroClass.mk ⋯ ⋯
Equations
- DirectLimit.instMonoid = Monoid.mk ⋯ ⋯ (fun (n : ℕ) => DirectLimit.map f f (fun (x : ι) (x_1 : G x) => x_1 ^ n) ⋯) ⋯ ⋯
Equations
- DirectLimit.instAddMonoid = AddMonoid.mk ⋯ ⋯ (fun (n : ℕ) => DirectLimit.map f f (fun (x : ι) (x_1 : G x) => n • x_1) ⋯) ⋯ ⋯
Equations
- DirectLimit.instCommMonoidOfMonoidHomClass = CommMonoid.mk ⋯
Equations
- DirectLimit.instAddCommMonoidOfAddMonoidHomClass = AddCommMonoid.mk ⋯
Equations
- DirectLimit.instAddGroup = AddGroup.mk ⋯
Equations
- DirectLimit.instCommGroupOfMonoidHomClass = CommGroup.mk ⋯
Equations
- DirectLimit.instAddCommGroupOfAddMonoidHomClass = AddCommGroup.mk ⋯
Equations
- DirectLimit.instMulZeroClassOfMulHomClassOfZeroHomClass = MulZeroClass.mk ⋯ ⋯
Equations
- DirectLimit.instMulZeroOneClass = MulZeroOneClass.mk ⋯ ⋯
Equations
- DirectLimit.instSemigroupWithZeroOfMulHomClassOfZeroHomClass = SemigroupWithZero.mk ⋯ ⋯
Equations
- DirectLimit.instMonoidWithZeroOfMonoidWithZeroHomClass = MonoidWithZero.mk ⋯ ⋯
Equations
- DirectLimit.instCommMonoidWithZeroOfMonoidWithZeroHomClass = CommMonoidWithZero.mk ⋯ ⋯
Equations
- DirectLimit.instGroupWithZero = GroupWithZero.mk ⋯ (fun (n : ℤ) => DirectLimit.map f f (fun (x : ι) (x_1 : G x) => x_1 ^ n) ⋯) ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- DirectLimit.instCommGroupWithZeroOfMonoidWithZeroHomClass = CommGroupWithZero.mk ⋯ GroupWithZero.zpow ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- DirectLimit.instAddMonoidWithOne = AddMonoidWithOne.mk ⋯ ⋯
Equations
- DirectLimit.instAddGroupWithOne = AddGroupWithOne.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- DirectLimit.instAddCommMonoidWithOneOfAddMonoidHomClass = AddCommMonoidWithOne.mk ⋯
Equations
- DirectLimit.instAddCommGroupWithOneOfAddMonoidHomClass = AddCommGroupWithOne.mk ⋯ ⋯ ⋯ ⋯
Equations
- DirectLimit.instNonUnitalNonAssocSemiringOfNonUnitalRingHomClass = NonUnitalNonAssocSemiring.mk ⋯ ⋯ ⋯ ⋯
Equations
- DirectLimit.instNonUnitalNonAssocCommSemiringOfNonUnitalRingHomClass = NonUnitalNonAssocCommSemiring.mk ⋯
Equations
- DirectLimit.instNonUnitalSemiringOfNonUnitalRingHomClass = NonUnitalSemiring.mk ⋯
Equations
- DirectLimit.instNonUnitalCommSemiringOfNonUnitalRingHomClass = NonUnitalCommSemiring.mk ⋯
Equations
- DirectLimit.instNonAssocSemiringOfRingHomClass = NonAssocSemiring.mk ⋯ ⋯ ⋯ ⋯
Equations
- DirectLimit.instSemiringOfRingHomClass = Semiring.mk ⋯ ⋯ ⋯ ⋯ Monoid.npow ⋯ ⋯
Equations
- DirectLimit.instCommSemiringOfRingHomClass = CommSemiring.mk ⋯
Equations
- DirectLimit.instCommRingOfRingHomClass = CommRing.mk ⋯
Equations
- DirectLimit.instSMulZeroClassOfMulActionHomClass = SMulZeroClass.mk ⋯
Equations
- DirectLimit.instSMulWithZeroOfMulActionHomClassOfZeroHomClass = SMulWithZero.mk ⋯
Equations
- DirectLimit.instDistribSMulOfMulActionHomClass = DistribSMul.mk ⋯
Equations
- DirectLimit.instDistribMulAction = DistribMulAction.mk ⋯ ⋯
Equations
- DirectLimit.instMulDistribMulActionOfMulActionHomClass = MulDistribMulAction.mk ⋯ ⋯
Equations
- DirectLimit.instDivisionSemiring = DivisionSemiring.mk ⋯ GroupWithZero.zpow ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ (fun (q : ℚ≥0) => DirectLimit.map f f (fun (x : ι) (x_1 : G x) => q • x_1) ⋯) ⋯
Equations
- DirectLimit.instSemifieldOfRingHomClass = Semifield.mk ⋯ DivisionSemiring.zpow ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ DivisionSemiring.nnqsmul ⋯
Equations
- DirectLimit.instDivisionRing = DivisionRing.mk ⋯ DivisionSemiring.zpow ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ DivisionSemiring.nnqsmul ⋯ ⋯ (fun (q : ℚ) => DirectLimit.map f f (fun (x : ι) (x_1 : G x) => q • x_1) ⋯) ⋯
The canonical map from a component to the direct limit.
Equations
- DirectLimit.Module.of R ι G f i = { toFun := fun (x : G i) => ⟦⟨i, x⟩⟧, map_add' := ⋯, map_smul' := ⋯ }
Instances For
The universal property of the direct limit: maps from the components to another module that respect the directed system structure (i.e. make some diagram commute) give rise to a unique map out of the direct limit.
Equations
- DirectLimit.Module.lift R ι G f g Hg = { toFun := DirectLimit.lift f (fun (x1 : ι) (x2 : G x1) => (g x1) x2) ⋯, map_add' := ⋯, map_smul' := ⋯ }
Instances For
The canonical map from a component to the direct limit.
Equations
- DirectLimit.Ring.of G f i = { toFun := fun (x : G i) => ⟦⟨i, x⟩⟧, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
Instances For
The universal property of the direct limit: maps from the components to another ring that respect the directed system structure (i.e. make some diagram commute) give rise to a unique map out of the direct limit.
Equations
- DirectLimit.Ring.lift G f P g Hg = { toFun := DirectLimit.lift f (fun (x1 : ι) (x2 : G x1) => (g x1) x2) ⋯, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }