Documentation

Mathlib.Algebra.DirectLimit

Direct limit of modules, abelian groups, rings, and fields. #

See Atiyah-Macdonald PP.32-33, Matsumura PP.269-270

Generalizes the notion of "union", or "gluing", of incomparable modules over the same ring, or incomparable abelian groups, or rings, or fields.

It is constructed as a quotient of the free module (for the module case) or quotient of the free commutative ring (for the ring case) instead of a quotient of the disjoint union so as to make the operations (addition etc.) "computable".

Main definitions #

class DirectedSystem {ι : Type v} [Preorder ι] (G : ιType w) (f : (i j : ι) → i jG iG j) :
  • map_self' : ∀ (i : ι) (x : G i) (h : i i), f i i h x = x
  • map_map' : ∀ {i j k : ι} (hij : i j) (hjk : j k) (x : G i), f j k hjk (f i j hij x) = f i k (_ : i k) x

A directed system is a functor from a category (directed poset) to another category.

Instances
    theorem DirectedSystem.map_self {ι : Type v} [Preorder ι] {G : ιType w} (f : (i j : ι) → i jG iG j) [DirectedSystem G fun i j h => f i j h] (i : ι) (x : G i) (h : i i) :
    f i i h x = x
    theorem DirectedSystem.map_map {ι : Type v} [Preorder ι] {G : ιType w} (f : (i j : ι) → i jG iG j) [DirectedSystem G fun i j h => f i j h] {i : ι} {j : ι} {k : ι} (hij : i j) (hjk : j k) (x : G i) :
    f j k hjk (f i j hij x) = f i k (_ : i k) x
    theorem Module.DirectedSystem.map_self {R : Type u} [Ring R] {ι : Type v} [Preorder ι] {G : ιType w} [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → i jG i →ₗ[R] G j) [DirectedSystem G fun i j h => ↑(f i j h)] (i : ι) (x : G i) (h : i i) :
    ↑(f i i h) x = x

    A copy of DirectedSystem.map_self specialized to linear maps, as otherwise the fun i j h ↦ f i j h can confuse the simplifier.

    theorem Module.DirectedSystem.map_map {R : Type u} [Ring R] {ι : Type v} [Preorder ι] {G : ιType w} [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → i jG i →ₗ[R] G j) [DirectedSystem G fun i j h => ↑(f i j h)] {i : ι} {j : ι} {k : ι} (hij : i j) (hjk : j k) (x : G i) :
    ↑(f j k hjk) (↑(f i j hij) x) = ↑(f i k (_ : i k)) x

    A copy of DirectedSystem.map_map specialized to linear maps, as otherwise the fun i j h ↦ f i j h can confuse the simplifier.

    def Module.DirectLimit {R : Type u} [Ring R] {ι : Type v} [dec_ι : DecidableEq ι] [Preorder ι] (G : ιType w) [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → i jG i →ₗ[R] G j) :
    Type (max v w)

    The direct limit of a directed system is the modules glued together along the maps.

    Instances For
      instance Module.DirectLimit.addCommGroup {R : Type u} [Ring R] {ι : Type v} [dec_ι : DecidableEq ι] [Preorder ι] (G : ιType w) [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → i jG i →ₗ[R] G j) :
      instance Module.DirectLimit.module {R : Type u} [Ring R] {ι : Type v} [dec_ι : DecidableEq ι] [Preorder ι] (G : ιType w) [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → i jG i →ₗ[R] G j) :
      instance Module.DirectLimit.inhabited {R : Type u} [Ring R] {ι : Type v} [dec_ι : DecidableEq ι] [Preorder ι] (G : ιType w) [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → i jG i →ₗ[R] G j) :
      def Module.DirectLimit.of (R : Type u) [Ring R] (ι : Type v) [dec_ι : DecidableEq ι] [Preorder ι] (G : ιType w) [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → i jG i →ₗ[R] G j) (i : ι) :

      The canonical map from a component to the direct limit.

      Instances For
        @[simp]
        theorem Module.DirectLimit.of_f {R : Type u} [Ring R] {ι : Type v} [dec_ι : DecidableEq ι] [Preorder ι] {G : ιType w} [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] {f : (i j : ι) → i jG i →ₗ[R] G j} {i : ι} {j : ι} {hij : i j} {x : G i} :
        ↑(Module.DirectLimit.of R ι G f j) (↑(f i j hij) x) = ↑(Module.DirectLimit.of R ι G f i) x
        theorem Module.DirectLimit.exists_of {R : Type u} [Ring R] {ι : Type v} [dec_ι : DecidableEq ι] [Preorder ι] {G : ιType w} [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] {f : (i j : ι) → i jG i →ₗ[R] G j} [Nonempty ι] [IsDirected ι fun x x_1 => x x_1] (z : Module.DirectLimit G f) :
        i x, ↑(Module.DirectLimit.of R ι G f i) x = z

        Every element of the direct limit corresponds to some element in some component of the directed system.

        theorem Module.DirectLimit.induction_on {R : Type u} [Ring R] {ι : Type v} [dec_ι : DecidableEq ι] [Preorder ι] {G : ιType w} [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] {f : (i j : ι) → i jG i →ₗ[R] G j} [Nonempty ι] [IsDirected ι fun x x_1 => x x_1] {C : Module.DirectLimit G fProp} (z : Module.DirectLimit G f) (ih : (i : ι) → (x : G i) → C (↑(Module.DirectLimit.of R ι G f i) x)) :
        C z
        def Module.DirectLimit.lift (R : Type u) [Ring R] (ι : Type v) [dec_ι : DecidableEq ι] [Preorder ι] (G : ιType w) [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → i jG i →ₗ[R] G j) {P : Type u₁} [AddCommGroup P] [Module R P] (g : (i : ι) → G i →ₗ[R] P) (Hg : ∀ (i j : ι) (hij : i j) (x : G i), ↑(g j) (↑(f i j hij) x) = ↑(g i) x) :

        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.

        Instances For
          theorem Module.DirectLimit.lift_of {R : Type u} [Ring R] {ι : Type v} [dec_ι : DecidableEq ι] [Preorder ι] {G : ιType w} [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] {f : (i j : ι) → i jG i →ₗ[R] G j} {P : Type u₁} [AddCommGroup P] [Module R P] (g : (i : ι) → G i →ₗ[R] P) (Hg : ∀ (i j : ι) (hij : i j) (x : G i), ↑(g j) (↑(f i j hij) x) = ↑(g i) x) {i : ι} (x : G i) :
          ↑(Module.DirectLimit.lift R ι G f g Hg) (↑(Module.DirectLimit.of R ι G f i) x) = ↑(g i) x
          theorem Module.DirectLimit.lift_unique {R : Type u} [Ring R] {ι : Type v} [dec_ι : DecidableEq ι] [Preorder ι] {G : ιType w} [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] {f : (i j : ι) → i jG i →ₗ[R] G j} {P : Type u₁} [AddCommGroup P] [Module R P] [Nonempty ι] [IsDirected ι fun x x_1 => x x_1] (F : Module.DirectLimit G f →ₗ[R] P) (x : Module.DirectLimit G f) :
          F x = ↑(Module.DirectLimit.lift R ι G f (fun i => LinearMap.comp F (Module.DirectLimit.of R ι G f i)) (_ : ∀ (i j : ι) (hij : i j) (x : G i), ↑((fun i => LinearMap.comp F (Module.DirectLimit.of R ι G f i)) j) (↑(f i j hij) x) = ↑((fun i => LinearMap.comp F (Module.DirectLimit.of R ι G f i)) i) x)) x
          noncomputable def Module.DirectLimit.totalize {R : Type u} [Ring R] {ι : Type v} [Preorder ι] (G : ιType w) [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → i jG i →ₗ[R] G j) (i : ι) (j : ι) :
          G i →ₗ[R] G j

          totalize G f i j is a linear map from G i to G j, for every i and j. If i ≤ j, then it is the map f i j that comes with the directed system G, and otherwise it is the zero map.

          Instances For
            theorem Module.DirectLimit.totalize_of_le {R : Type u} [Ring R] {ι : Type v} [Preorder ι] {G : ιType w} [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] {f : (i j : ι) → i jG i →ₗ[R] G j} {i : ι} {j : ι} (h : i j) :
            theorem Module.DirectLimit.totalize_of_not_le {R : Type u} [Ring R] {ι : Type v} [Preorder ι] {G : ιType w} [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] {f : (i j : ι) → i jG i →ₗ[R] G j} {i : ι} {j : ι} (h : ¬i j) :
            theorem Module.DirectLimit.toModule_totalize_of_le {R : Type u} [Ring R] {ι : Type v} [dec_ι : DecidableEq ι] [Preorder ι] {G : ιType w} [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] {f : (i j : ι) → i jG i →ₗ[R] G j} [DirectedSystem G fun i j h => ↑(f i j h)] {x : DirectSum ι G} {i : ι} {j : ι} (hij : i j) (hx : ∀ (k : ι), k DFinsupp.support xk i) :
            ↑(DirectSum.toModule R ι (G j) fun k => Module.DirectLimit.totalize G f k j) x = ↑(f i j hij) (↑(DirectSum.toModule R ι (G i) fun k => Module.DirectLimit.totalize G f k i) x)
            theorem Module.DirectLimit.of.zero_exact_aux {R : Type u} [Ring R] {ι : Type v} [dec_ι : DecidableEq ι] [Preorder ι] {G : ιType w} [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] {f : (i j : ι) → i jG i →ₗ[R] G j} [DirectedSystem G fun i j h => ↑(f i j h)] [Nonempty ι] [IsDirected ι fun x x_1 => x x_1] {x : DirectSum ι G} (H : Submodule.Quotient.mk x = 0) :
            j, (∀ (k : ι), k DFinsupp.support xk j) ↑(DirectSum.toModule R ι (G j) fun i => Module.DirectLimit.totalize G f i j) x = 0
            theorem Module.DirectLimit.of.zero_exact {R : Type u} [Ring R] {ι : Type v} [dec_ι : DecidableEq ι] [Preorder ι] {G : ιType w} [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] {f : (i j : ι) → i jG i →ₗ[R] G j} [DirectedSystem G fun i j h => ↑(f i j h)] [IsDirected ι fun x x_1 => x x_1] {i : ι} {x : G i} (H : ↑(Module.DirectLimit.of R ι G f i) x = 0) :
            j hij, ↑(f i j hij) x = 0

            A component that corresponds to zero in the direct limit is already zero in some bigger module in the directed system.

            def AddCommGroup.DirectLimit {ι : Type v} [dec_ι : DecidableEq ι] [Preorder ι] (G : ιType w) [(i : ι) → AddCommGroup (G i)] (f : (i j : ι) → i jG i →+ G j) :
            Type (max w v)

            The direct limit of a directed system is the abelian groups glued together along the maps.

            Instances For
              theorem AddCommGroup.DirectLimit.directedSystem {ι : Type v} [Preorder ι] (G : ιType w) [(i : ι) → AddCommGroup (G i)] (f : (i j : ι) → i jG i →+ G j) [h : DirectedSystem G fun i j h => ↑(f i j h)] :
              DirectedSystem G fun i j hij => ↑(AddMonoidHom.toIntLinearMap (f i j hij))
              instance AddCommGroup.DirectLimit.instAddCommGroupDirectLimit {ι : Type v} [dec_ι : DecidableEq ι] [Preorder ι] (G : ιType w) [(i : ι) → AddCommGroup (G i)] (f : (i j : ι) → i jG i →+ G j) :
              instance AddCommGroup.DirectLimit.instInhabitedDirectLimit {ι : Type v} [dec_ι : DecidableEq ι] [Preorder ι] (G : ιType w) [(i : ι) → AddCommGroup (G i)] (f : (i j : ι) → i jG i →+ G j) :
              def AddCommGroup.DirectLimit.of {ι : Type v} [dec_ι : DecidableEq ι] [Preorder ι] (G : ιType w) [(i : ι) → AddCommGroup (G i)] (f : (i j : ι) → i jG i →+ G j) (i : ι) :

              The canonical map from a component to the direct limit.

              Instances For
                @[simp]
                theorem AddCommGroup.DirectLimit.of_f {ι : Type v} [dec_ι : DecidableEq ι] [Preorder ι] {G : ιType w} [(i : ι) → AddCommGroup (G i)] {f : (i j : ι) → i jG i →+ G j} {i : ι} {j : ι} (hij : i j) (x : G i) :
                ↑(AddCommGroup.DirectLimit.of G f j) (↑(f i j hij) x) = ↑(AddCommGroup.DirectLimit.of G f i) x
                theorem AddCommGroup.DirectLimit.induction_on {ι : Type v} [dec_ι : DecidableEq ι] [Preorder ι] {G : ιType w} [(i : ι) → AddCommGroup (G i)] {f : (i j : ι) → i jG i →+ G j} [Nonempty ι] [IsDirected ι fun x x_1 => x x_1] {C : AddCommGroup.DirectLimit G fProp} (z : AddCommGroup.DirectLimit G f) (ih : (i : ι) → (x : G i) → C (↑(AddCommGroup.DirectLimit.of G f i) x)) :
                C z
                theorem AddCommGroup.DirectLimit.of.zero_exact {ι : Type v} [dec_ι : DecidableEq ι] [Preorder ι] {G : ιType w} [(i : ι) → AddCommGroup (G i)] {f : (i j : ι) → i jG i →+ G j} [IsDirected ι fun x x_1 => x x_1] [DirectedSystem G fun i j h => ↑(f i j h)] (i : ι) (x : G i) (h : ↑(AddCommGroup.DirectLimit.of G f i) x = 0) :
                j hij, ↑(f i j hij) x = 0

                A component that corresponds to zero in the direct limit is already zero in some bigger module in the directed system.

                def AddCommGroup.DirectLimit.lift {ι : Type v} [dec_ι : DecidableEq ι] [Preorder ι] (G : ιType w) [(i : ι) → AddCommGroup (G i)] (f : (i j : ι) → i jG i →+ G j) (P : Type u₁) [AddCommGroup P] (g : (i : ι) → G i →+ P) (Hg : ∀ (i j : ι) (hij : i j) (x : G i), ↑(g j) (↑(f i j hij) x) = ↑(g i) x) :

                The universal property of the direct limit: maps from the components to another abelian group that respect the directed system structure (i.e. make some diagram commute) give rise to a unique map out of the direct limit.

                Instances For
                  @[simp]
                  theorem AddCommGroup.DirectLimit.lift_of {ι : Type v} [dec_ι : DecidableEq ι] [Preorder ι] {G : ιType w} [(i : ι) → AddCommGroup (G i)] {f : (i j : ι) → i jG i →+ G j} (P : Type u₁) [AddCommGroup P] (g : (i : ι) → G i →+ P) (Hg : ∀ (i j : ι) (hij : i j) (x : G i), ↑(g j) (↑(f i j hij) x) = ↑(g i) x) (i : ι) (x : G i) :
                  ↑(AddCommGroup.DirectLimit.lift G f P g Hg) (↑(AddCommGroup.DirectLimit.of G f i) x) = ↑(g i) x
                  theorem AddCommGroup.DirectLimit.lift_unique {ι : Type v} [dec_ι : DecidableEq ι] [Preorder ι] {G : ιType w} [(i : ι) → AddCommGroup (G i)] {f : (i j : ι) → i jG i →+ G j} (P : Type u₁) [AddCommGroup P] [Nonempty ι] [IsDirected ι fun x x_1 => x x_1] (F : AddCommGroup.DirectLimit G f →+ P) (x : AddCommGroup.DirectLimit G f) :
                  F x = ↑(AddCommGroup.DirectLimit.lift G f P (fun i => AddMonoidHom.comp F (LinearMap.toAddMonoidHom (AddCommGroup.DirectLimit.of G f i))) (_ : ∀ (i j : ι) (hij : i j) (x : G i), F (↑(AddCommGroup.DirectLimit.of G f j) (↑(f i j hij) x)) = F (↑(AddCommGroup.DirectLimit.of G f i) x))) x
                  def Ring.DirectLimit {ι : Type v} [Preorder ι] (G : ιType w) [(i : ι) → CommRing (G i)] (f : (i j : ι) → i jG iG j) :
                  Type (max v w)

                  The direct limit of a directed system is the rings glued together along the maps.

                  Instances For
                    instance Ring.DirectLimit.commRing {ι : Type v} [Preorder ι] (G : ιType w) [(i : ι) → CommRing (G i)] (f : (i j : ι) → i jG iG j) :
                    instance Ring.DirectLimit.ring {ι : Type v} [Preorder ι] (G : ιType w) [(i : ι) → CommRing (G i)] (f : (i j : ι) → i jG iG j) :
                    instance Ring.DirectLimit.zero {ι : Type v} [Preorder ι] (G : ιType w) [(i : ι) → CommRing (G i)] (f : (i j : ι) → i jG iG j) :
                    instance Ring.DirectLimit.instInhabitedDirectLimit {ι : Type v} [Preorder ι] (G : ιType w) [(i : ι) → CommRing (G i)] (f : (i j : ι) → i jG iG j) :
                    def Ring.DirectLimit.of {ι : Type v} [Preorder ι] (G : ιType w) [(i : ι) → CommRing (G i)] (f : (i j : ι) → i jG iG j) (i : ι) :

                    The canonical map from a component to the direct limit.

                    Instances For
                      theorem Ring.DirectLimit.of_f {ι : Type v} [Preorder ι] {G : ιType w} [(i : ι) → CommRing (G i)] {f : (i j : ι) → i jG iG j} {i : ι} {j : ι} (hij : i j) (x : G i) :
                      ↑(Ring.DirectLimit.of G f j) (f i j hij x) = ↑(Ring.DirectLimit.of G f i) x
                      theorem Ring.DirectLimit.exists_of {ι : Type v} [Preorder ι] {G : ιType w} [(i : ι) → CommRing (G i)] {f : (i j : ι) → i jG iG j} [Nonempty ι] [IsDirected ι fun x x_1 => x x_1] (z : Ring.DirectLimit G f) :
                      i x, ↑(Ring.DirectLimit.of G f i) x = z

                      Every element of the direct limit corresponds to some element in some component of the directed system.

                      theorem Ring.DirectLimit.Polynomial.exists_of {ι : Type v} [Preorder ι] {G : ιType w} [(i : ι) → CommRing (G i)] {f' : (i j : ι) → i jG i →+* G j} [Nonempty ι] [IsDirected ι fun x x_1 => x x_1] (q : Polynomial (Ring.DirectLimit G fun i j h => ↑(f' i j h))) :
                      i p, Polynomial.map (Ring.DirectLimit.of G (fun i j h => ↑(f' i j h)) i) p = q
                      theorem Ring.DirectLimit.induction_on {ι : Type v} [Preorder ι] {G : ιType w} [(i : ι) → CommRing (G i)] {f : (i j : ι) → i jG iG j} [Nonempty ι] [IsDirected ι fun x x_1 => x x_1] {C : Ring.DirectLimit G fProp} (z : Ring.DirectLimit G f) (ih : (i : ι) → (x : G i) → C (↑(Ring.DirectLimit.of G f i) x)) :
                      C z
                      theorem Ring.DirectLimit.of.zero_exact_aux2 {ι : Type v} [Preorder ι] (G : ιType w) [(i : ι) → CommRing (G i)] (f' : (i j : ι) → i jG i →+* G j) [DirectedSystem G fun i j h => ↑(f' i j h)] {x : FreeCommRing ((i : ι) × G i)} {s : Set ((i : ι) × G i)} {t : Set ((i : ι) × G i)} (hxs : FreeCommRing.IsSupported x s) {j : ι} {k : ι} (hj : ∀ (z : (i : ι) × G i), z sz.fst j) (hk : ∀ (z : (i : ι) × G i), z tz.fst k) (hjk : j k) (hst : s t) :
                      ↑(f' j k hjk) (↑(FreeCommRing.lift fun ix => ↑(f' (ix).fst j (hj ix (_ : ix s))) (ix).snd) (↑(FreeCommRing.restriction s) x)) = ↑(FreeCommRing.lift fun ix => ↑(f' (ix).fst k (hk ix (_ : ix t))) (ix).snd) (↑(FreeCommRing.restriction t) x)
                      theorem Ring.DirectLimit.of.zero_exact_aux {ι : Type v} [dec_ι : DecidableEq ι] [Preorder ι] {G : ιType w} [(i : ι) → CommRing (G i)] {f' : (i j : ι) → i jG i →+* G j} [DirectedSystem G fun i j h => ↑(f' i j h)] [Nonempty ι] [IsDirected ι fun x x_1 => x x_1] {x : FreeCommRing ((i : ι) × G i)} (H : ↑(Ideal.Quotient.mk (Ideal.span {a | (i j H x, FreeCommRing.of { fst := j, snd := (fun i j h => ↑(f' i j h)) i j H x } - FreeCommRing.of { fst := i, snd := x } = a) (i, FreeCommRing.of { fst := i, snd := 1 } - 1 = a) (i x y, FreeCommRing.of { fst := i, snd := x + y } - (FreeCommRing.of { fst := i, snd := x } + FreeCommRing.of { fst := i, snd := y }) = a) i x y, FreeCommRing.of { fst := i, snd := x * y } - FreeCommRing.of { fst := i, snd := x } * FreeCommRing.of { fst := i, snd := y } = a})) x = 0) :
                      j s H, FreeCommRing.IsSupported x s ↑(FreeCommRing.lift fun ix => ↑(f' (ix).fst j (_ : (ix).fst j)) (ix).snd) (↑(FreeCommRing.restriction s) x) = 0
                      theorem Ring.DirectLimit.of.zero_exact {ι : Type v} [dec_ι : DecidableEq ι] [Preorder ι] {G : ιType w} [(i : ι) → CommRing (G i)] {f' : (i j : ι) → i jG i →+* G j} [DirectedSystem G fun i j h => ↑(f' i j h)] [IsDirected ι fun x x_1 => x x_1] {i : ι} {x : G i} (hix : ↑(Ring.DirectLimit.of G (fun i j h => ↑(f' i j h)) i) x = 0) :
                      j hij, ↑(f' i j hij) x = 0

                      A component that corresponds to zero in the direct limit is already zero in some bigger module in the directed system.

                      theorem Ring.DirectLimit.of_injective {ι : Type v} [dec_ι : DecidableEq ι] [Preorder ι] {G : ιType w} [(i : ι) → CommRing (G i)] (f' : (i j : ι) → i jG i →+* G j) [IsDirected ι fun x x_1 => x x_1] [DirectedSystem G fun i j h => ↑(f' i j h)] (hf : ∀ (i j : ι) (hij : i j), Function.Injective ↑(f' i j hij)) (i : ι) :
                      Function.Injective ↑(Ring.DirectLimit.of G (fun i j h => ↑(f' i j h)) i)

                      If the maps in the directed system are injective, then the canonical maps from the components to the direct limits are injective.

                      def Ring.DirectLimit.lift {ι : Type v} [Preorder ι] (G : ιType w) [(i : ι) → CommRing (G i)] (f : (i j : ι) → i jG iG j) (P : Type u₁) [CommRing P] (g : (i : ι) → G i →+* P) (Hg : ∀ (i j : ι) (hij : i j) (x : G i), ↑(g j) (f i j hij x) = ↑(g i) x) :

                      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.

                      Instances For
                        theorem Ring.DirectLimit.lift_of {ι : Type v} [Preorder ι] {G : ιType w} [(i : ι) → CommRing (G i)] {f : (i j : ι) → i jG iG j} (P : Type u₁) [CommRing P] (g : (i : ι) → G i →+* P) (Hg : ∀ (i j : ι) (hij : i j) (x : G i), ↑(g j) (f i j hij x) = ↑(g i) x) (i : ι) (x : G i) :
                        ↑(Ring.DirectLimit.lift G f P g Hg) (↑(Ring.DirectLimit.of G f i) x) = ↑(g i) x
                        theorem Ring.DirectLimit.lift_unique {ι : Type v} [Preorder ι] {G : ιType w} [(i : ι) → CommRing (G i)] {f : (i j : ι) → i jG iG j} (P : Type u₁) [CommRing P] [Nonempty ι] [IsDirected ι fun x x_1 => x x_1] (F : Ring.DirectLimit G f →+* P) (x : Ring.DirectLimit G f) :
                        F x = ↑(Ring.DirectLimit.lift G f P (fun i => RingHom.comp F (Ring.DirectLimit.of G f i)) (_ : ∀ (i j : ι) (hij : i j) (x : G i), F (↑(Ring.DirectLimit.of G f j) (f i j hij x)) = F (↑(Ring.DirectLimit.of G f i) x))) x
                        instance Field.DirectLimit.nontrivial {ι : Type v} [dec_ι : DecidableEq ι] [Preorder ι] (G : ιType w) [Nonempty ι] [IsDirected ι fun x x_1 => x x_1] [(i : ι) → Field (G i)] (f' : (i j : ι) → i jG i →+* G j) [DirectedSystem G fun i j h => ↑(f' i j h)] :
                        Nontrivial (Ring.DirectLimit G fun i j h => ↑(f' i j h))
                        theorem Field.DirectLimit.exists_inv {ι : Type v} [Preorder ι] (G : ιType w) [Nonempty ι] [IsDirected ι fun x x_1 => x x_1] [(i : ι) → Field (G i)] (f : (i j : ι) → i jG iG j) {p : Ring.DirectLimit G f} :
                        p 0y, p * y = 1
                        noncomputable def Field.DirectLimit.inv {ι : Type v} [Preorder ι] (G : ιType w) [Nonempty ι] [IsDirected ι fun x x_1 => x x_1] [(i : ι) → Field (G i)] (f : (i j : ι) → i jG iG j) (p : Ring.DirectLimit G f) :

                        Noncomputable multiplicative inverse in a direct limit of fields.

                        Instances For
                          theorem Field.DirectLimit.mul_inv_cancel {ι : Type v} [Preorder ι] (G : ιType w) [Nonempty ι] [IsDirected ι fun x x_1 => x x_1] [(i : ι) → Field (G i)] (f : (i j : ι) → i jG iG j) {p : Ring.DirectLimit G f} (hp : p 0) :
                          theorem Field.DirectLimit.inv_mul_cancel {ι : Type v} [Preorder ι] (G : ιType w) [Nonempty ι] [IsDirected ι fun x x_1 => x x_1] [(i : ι) → Field (G i)] (f : (i j : ι) → i jG iG j) {p : Ring.DirectLimit G f} (hp : p 0) :
                          @[reducible]
                          noncomputable def Field.DirectLimit.field {ι : Type v} [dec_ι : DecidableEq ι] [Preorder ι] (G : ιType w) [Nonempty ι] [IsDirected ι fun x x_1 => x x_1] [(i : ι) → Field (G i)] (f' : (i j : ι) → i jG i →+* G j) [DirectedSystem G fun i j h => ↑(f' i j h)] :
                          Field (Ring.DirectLimit G fun i j h => ↑(f' i j h))

                          Noncomputable field structure on the direct limit of fields. See note [reducible non-instances].

                          Instances For