Q/Z as colimit of Z/nZ

Stream: new members

[Edison Xie]

(I'm a new member to category theory in lean so I'll post it here)
I want to prove that ℚ ⧸ (Algebra.ofId ℤ ℚ).range.toSubmodule is isomorphic to limit of `Zmod i. The proof I found is in here and here's some (dumb) question:

• Do we have this in mathlib?
• Do we have a subtype of natural saying that n ≤ m ↔ n ∣ m?
• I'm currently constructing this from scratch but is this the best way?
  Thanks!

[Kenny Lau]

just make sure you don't include 0

[Kenny Lau]

how "from scratch" is your construction?

[Edison Xie]

Kenny Lau said:

just make sure you don't include 0

I've noticed :-)

[Edison Xie]

Kenny Lau said:

how "from scratch" is your construction?

from constructing the functor, etc.

[Kenny Lau]

I think we've noticed that we're missing a predicate "is direct limit" in mathlib

[Kenny Lau]

Edison Xie said:

Kenny Lau said:

how "from scratch" is your construction?

from constructing the functor, etc.

you're using DirectLimit right

[Edison Xie]

oh no I'm using CategoryTheory.Limits.colimit but second thought may be a bad idea

[Kenny Lau]

yeah we're also missing API to connect DirectLimit with colimit

[Kenny Lau]

ModuleCat.directLimitIsColimit

[Kenny Lau]

we have it for modules tho

[Kenny Lau]

it looks like they did it skipping the AddCommGroup step

[Kenny Lau]

it's also a bit messy if you use Z-Mod / N-Mod because of diamonds

[Edison Xie]

The reason I don't wanna use module is that I don't wanna be find myself in this M.isModule = AddCommGroup.toIntModule M horror again

[Kenny Lau]

so I would first construct a type WithDvd M where the preorder is dvd

[Edison Xie]

yeah

[Kenny Lau]

and use PNat which is a CancelCommMonoid

[Kenny Lau]

and then i would define the "IsDirectLimit" predicate

[Kenny Lau]

(compare IsLocalization)

[Aaron Liu]

I would just state it with docs#CategoryTheory.Limits.IsColimit

[Kenny Lau]

Kenny Lau said:

and then i would define the "IsDirectLimit" predicate

a "direct cone" of F at R is a collection of add homs phi from F i to R so that phi commutes with f.

a "direct cone" at R is a direct limit iff:

1. forall y : R exists i x, phi i x = y
2. forall i j xi xj, phi i xi = phi j xj implies there is k above i and j such that f hik xi = f hjk xj

[Kenny Lau]

then you can show that these conditions are equivalent to the category conditions Aaron linked to

[Kenny Lau]

you might not even need to define direct cone separately

[Kenny Lau]

as in, you can just use Cocone

[Kenny Lau]

well this is awkward

[Kenny Lau]

AddCommGrp.FilteredColimits.colimit exists but is not defined using DirectLimit?

[Kenny Lau]

i don't think nullifies anything i said above

[Aaron Liu]

Kenny Lau said:

AddCommGrp.FilteredColimits.colimit exists but is not defined using DirectLimit?

Well yeah

[Aaron Liu]

It's giving an object in the category of add comm groups

[Aaron Liu]

So of course it's using the category theory language

[Wuyang]

The gap between DirectLimit and colimit APIs seems a bit tricky. WithDvd + PNat and a direct limit predicate could be a clean bridge.

Might be worth a quick search on LeanFinder to see if any hidden gems in mathlib or prior work match your needs.

[Wuyang]

(deleted)

[leanfinder]

Failure! Bot is unavailable

[Wuyang]

@leanfinder Q/Z as colimit of Zmod n in Lean mathlib, using DirectLimit vs colimit, missing API connections and direct limit predicates

[leanfinder]

Here’s what I found:

• abbrev DirectLimit : Type _ := Quotient (setoid f) "Given a directed system consisting of:
• A directed poset $(I, \leq)$
• A family of objects $\{F_i\}_{i \in I}$

• A family of morphisms $f_{ij} : F_i \to F_j$ for each $i \leq j$ satisfying:

  1. $f_{ii} = \text{id}_{F_i}$ (identity)
  2. $f_{jk} \circ f_{ij} = f_{ik}$ for $i \leq j \leq k$ (composition)

The direct limit $\varinjlim F$ is defined as the quotient of the disjoint union $\bigsqcup_{i \in I} F_i$ by the equivalence relation:
$(i, x) \sim (j, y) \iff \exists k \geq i,j,\ f_{ik}(x) = f_{jk}(y)$" (score: 0.721)

• definition ModuleCat.directLimitIsColimit : IsColimit (directLimitCocone G f) where desc s := ofHom <| Module.DirectLimit.lift R ι G f (fun i => (s.ι.app i).hom) fun i j h x => by simp only [Functor.const_obj_obj] rw [← s.w (homOfLE h)] rfl fac s i := by ext dsimp only [hom_comp, directLimitCocone, hom_ofHom, LinearMap.comp_apply] apply DirectLimit.lift_of uniq s m h := by have : s.ι.app = fun i => (ofHom (DirectLimit.of R ι (fun i => G i) (fun i j H => f i j H) i)) ≫ m := by funext i rw [← h] rfl ext simp only [this] apply Module.DirectLimit.lift_unique "Given a directed system of $R$-modules $(G_i)_{i \in \iota}$ indexed by a directed preorder $\iota$ with transition maps $f_{ij} \colon G_i \to G_j$ for $i \leq j$, the cocone ModuleCat.directLimitCocone G f is a colimit cocone in the category of $R$-modules.

This means that for any other cocone $s$ over the diagram directLimitDiagram G f, there exists a unique $R$-linear map from the direct limit to the vertex of $s$ that makes all the relevant diagrams commute.

The construction uses:

• The canonical maps $\iota_i \colon G_i \to \text{DirectLimit} G f$ for each $i \in \iota$
• The universal property of the direct limit, which provides a unique lift of any compatible family of maps from the $G_i$ to another module" (score: 0.695)

• definition ZMod : ℕ → Type | 0 => ℤ | n + 1 => Fin (n + 1) "The integers modulo $n$, denoted $\mathbb{Z}/n\mathbb{Z}$, is defined as:

• The integers $\mathbb{Z}$ when $n = 0$

• The finite type with $n$ elements (represented as $\text{Fin}(n)$) when $n > 0$

This construction provides the commutative ring structure on $\mathbb{Z}/n\mathbb{Z}$." (score: 0.693)

• theorem exists_of [Nonempty ι] [IsDirected ι (· ≤ ·)] (z : DirectLimit G f) : ∃ i x, of G f i x = z := Nonempty.elim (by infer_instance) fun ind : ι => Quotient.inductionOn' z fun x => FreeAbelianGroup.induction_on x ⟨ind, 0, (of _ _ ind).map_zero⟩ (fun s => Multiset.induction_on s ⟨ind, 1, (of _ _ ind).map_one⟩ fun a s ih => let ⟨i, x⟩ := a let ⟨j, y, hs⟩ := ih let ⟨k, hik, hjk⟩ := exists_ge_ge i j ⟨k, f i k hik x * f j k hjk y, by rw [(of G f k).map_mul, of_f, of_f, hs] /- porting note: In Lean3, from here, this was by refl. I have added
  the lemma FreeCommRing.of_cons to fix this proof. -/ apply congr_arg Quotient.mk'' symm apply FreeCommRing.of_cons⟩) (fun s ⟨i, x, ih⟩ => ⟨i, -x, by rw [(of G _ _).map_neg, ih] rfl⟩) fun p q ⟨i, x, ihx⟩ ⟨j, y, ihy⟩ => let ⟨k, hik, hjk⟩ := exists_ge_ge i j ⟨k, f i k hik x + f j k hjk y, by rw [(of _ _ _).map_add, of_f, of_f, ihx, ihy]; rfl⟩ "Let $\iota$ be a nonempty directed set, and let $G$ be a directed system of commutative rings indexed by $\iota$ with transition maps $f_{ij} : G_i \to G_j$ for each $i \leq j$. For any element $z$ in the direct limit $\varinjlim G$, there exists an index $i \in \iota$ and an element $x \in G_i$ such that the canonical map $\text{of}_{G,f}$ sends $x$ to $z$, i.e., $\text{of}_{G,f}(x) = z$. This means every element in the direct limit can be traced back to an element in one of the component rings." (score: 0.693)

• theorem Module.DirectLimit.quotMk_of (i x) : Quot.mk _ (.of G i x) = of R ι G f i x := rfl "For any index $i$ and element $x \in G_i$, the equivalence class of the direct sum element $\text{of } G_i x$ under the relation $\text{Eqv}$ is equal to the canonical map $\text{of } R \iota G f i x$ in the direct limit module." (score: 0.692)

• theorem DirectLimit.intCast_def [∀ i j h, OneHomClass (T h) (G i) (G j)] (n : ℤ) (i) : (n : DirectLimit G f) = ⟦⟨i, n⟩⟧ := map₀_def _ _ (fun _ _ _ ↦ map_intCast' _ (map_one _) _) _ "Let $\{G_i\}_{i \in I}$ be a directed system of algebraic structures with transition maps that are one-preserving homomorphisms (i.e., for all $i \leq j$, the map $f_{ij} : G_i \to G_j$ satisfies $f_{ij}(1) = 1$). Then for any integer $n$ and any index $i \in I$, the image of $n$ in the direct limit $\varinjlim G$ is equal to the equivalence class of the pair $(i, n)$, where $n$ is considered as an element of $G_i$ via the integer embedding.

In symbols:
$n = [\langle i, n \rangle] \text{ in } \varinjlim G.$" (score: 0.691)

• definition FirstOrder.Language.DirectLimit [DirectedSystem G fun i j h => f i j h] [IsDirected ι (· ≤ ·)] := Quotient (DirectLimit.setoid G f) "The direct limit of a directed system of first-order structures $(G_i)_{i \in \iota}$ indexed by a directed preorder $(\iota, \leq)$ with embeddings $f_{ij} : G_i \hookrightarrow G_j$ for each $i \leq j$ is the quotient of the disjoint union $\Sigma_{i \in \iota} G_i$ by the equivalence relation:
  $$
  \langle i, x \rangle \sim \langle j, y \rangle \iff \exists k \in \iota \ (i \leq k \land j \leq k \land f_{ik}(x) = f_{jk}(y))
  $$
  This construction glues together elements from different structures in the system when they eventually become equal under the embeddings." (score: 0.688)

• definition Int.quotientZMultiplesNatEquivZMod : ℤ ⧸ AddSubgroup.zmultiples (n : ℤ) ≃+ ZMod n := (quotientAddEquivOfEq (ZMod.ker_intCastAddHom _)).symm.trans <| quotientKerEquivOfRightInverse (Int.castAddHom (ZMod n)) cast intCast_zmod_cast "The additive group equivalence between the quotient group $\mathbb{Z}/n\mathbb{Z}$ (where $n\mathbb{Z}$ is the additive subgroup of $\mathbb{Z}$ generated by $n$) and the integers modulo $n$ ($\mathbb{Z}/n\mathbb{Z}$ as $\text{ZMod }n$)." (score: 0.687)

• definition FirstOrder.Language.DirectLimit.setoid [DirectedSystem G fun i j h => f i j h] [IsDirected ι (· ≤ ·)] : Setoid (Σˣ f) where r := fun ⟨i, x⟩ ⟨j, y⟩ => ∃ (k : ι) (ik : i ≤ k) (jk : j ≤ k), f i k ik x = f j k jk y iseqv := ⟨fun ⟨i, _⟩ => ⟨i, refl i, refl i, rfl⟩, @fun ⟨_, _⟩ ⟨_, _⟩ ⟨k, ik, jk, h⟩ => ⟨k, jk, ik, h.symm⟩, @fun ⟨i, x⟩ ⟨j, y⟩ ⟨k, z⟩ ⟨ij, hiij, hjij, hij⟩ ⟨jk, hjjk, hkjk, hjk⟩ => by obtain ⟨ijk, hijijk, hjkijk⟩ := directed_of (· ≤ ·) ij jk refine ⟨ijk, le_trans hiij hijijk, le_trans hkjk hjkijk, ?_⟩ rw [← DirectedSystem.map_map, hij, DirectedSystem.map_map] · symm rw [← DirectedSystem.map_map, ← hjk, DirectedSystem.map_map] assumption assumption⟩ "Given a directed system of first-order structures $(G_i)_{i \in \iota}$ indexed by a directed preorder $(\iota, \leq)$ with embeddings $f_{ij} : G_i \hookrightarrow G_j$ for each $i \leq j$, the setoid (equivalence relation) on the disjoint union $\Sigma_{i \in \iota} G_i$ is defined by:
  $$
  \langle i, x \rangle \sim \langle j, y \rangle \iff \exists k \in \iota \ (i \leq k \land j \leq k \land f_{ik}(x) = f_{jk}(y))
  $$
  This equivalence relation is reflexive, symmetric, and transitive, making it a valid setoid structure." (score: 0.683)

• /-- The direct limit constructed as a quotient of the direct sum is isomorphic to the direct limit constructed as a quotient of the disjoint union. -/ def linearEquiv : DirectLimit G f ≃ₗ[R] _root_.DirectLimit G f := .ofLinear (lift _ _ _ _ (Module.of _ _ _ _) fun _ _ _ _ ↦ .symm <| eq_of_le ..) (Module.lift _ _ _ _ (of _ _ _ _) fun _ _ _ _ ↦ of_f ..) (by ext ⟨_⟩; rw [← Quotient.mk]; simp [Module.lift, _root_.DirectLimit.lift_def]; rfl) <| by ext ⟨x⟩; refine x.induction_on (by simp) (fun i x ↦ ?_) (by simp+contextual) rw [quotMk_of, LinearMap.comp_apply, lift_of, Module.lift_of, LinearMap.id_apply] "The direct limit of a family of $R$-modules $G_i$, constructed as a quotient of their direct sum, is linearly isomorphic to the direct limit constructed as a quotient of their disjoint union. This isomorphism is established by compatible $R$-linear maps $f_{ij}$ for $i \leq j$, ensuring that the two constructions of the direct limit are equivalent." (score: 0.683)

[Kevin Buzzard]

@Madison Crim did you PR anything about direct limits of abelian groups?