English
If the bonding maps f' i j h are injective for all i ≤ j, then the canonical injections of each component into the direct limit are injective.
Русский
Если связующие отображения f' i j h инъективны для всех i ≤ j, то канонические вложения компонентов в прямой предел инъективны.
LaTeX
$$$\\forall i,\\; \\mathrm{of}\\;G\\;f\\;i: G_i \\to \\mathrm{DirectLimit}(G,f)\\;\\text{injective}.$$$
Lean4
/-- Noncomputable field structure on the direct limit of fields.
See note [reducible non-instances]. -/
protected noncomputable abbrev field [DirectedSystem G (f' · · ·)] : Field (Ring.DirectLimit G (f' · · ·)) where
-- This used to include the parent CommRing and Nontrivial instances,
-- but leaving them implicit avoids a very expensive (2-3 minutes!) eta expansion.
inv := inv G (f' · · ·)
mul_inv_cancel := fun _ ↦ DirectLimit.mul_inv_cancel G (f' · · ·)
inv_zero := dif_pos rfl
nnqsmul := _
nnqsmul_def _ _ := rfl
qsmul := _
qsmul_def _ _ := rfl
