Documentation

Mathlib.Algebra.Colimit.ModuleRing

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 #

theorem Module.DirectedSystem.map_self {ι : Type u_1} [Preorder ι] {F : ιType u_4} {T : i j : ι⦄ → i jSort u_8} (f : (i j : ι) → (h : i j) → T h) [i j : ι⦄ → (h : i j) → FunLike (T h) (F i) (F j)] [DirectedSystem F fun (x1 x2 : ι) (x3 : x1 x2) => (f x1 x2 x3)] ⦃i : ι (x : F i) :
(f i i ) x = x

Alias of DirectedSystem.map_self'.


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

theorem Module.DirectedSystem.map_map {ι : Type u_1} [Preorder ι] {F : ιType u_4} {T : i j : ι⦄ → i jSort u_8} (f : (i j : ι) → (h : i j) → T h) [i j : ι⦄ → (h : i j) → FunLike (T h) (F i) (F j)] [DirectedSystem F fun (x1 x2 : ι) (x3 : x1 x2) => (f x1 x2 x3)] ⦃i j k : ι (hij : i j) (hjk : j k) (x : F i) :
(f j k hjk) ((f i j hij) x) = (f i k ) x

Alias of DirectedSystem.map_map'.


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

noncomputable def Module.DirectLimit {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) [DecidableEq ι] :
Type (max v w)

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

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    noncomputable instance Module.DirectLimit.addCommGroup {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) [DecidableEq ι] :
    Equations
    • One or more equations did not get rendered due to their size.
    noncomputable instance Module.DirectLimit.module {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) [DecidableEq ι] :
    Equations
    • One or more equations did not get rendered due to their size.
    noncomputable instance Module.DirectLimit.inhabited {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) [DecidableEq ι] :
    Equations
    noncomputable instance Module.DirectLimit.unique {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) [DecidableEq ι] [IsEmpty ι] :
    Equations
    • One or more equations did not get rendered due to their size.
    noncomputable def Module.DirectLimit.of (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) [DecidableEq ι] (i : ι) :

    The canonical map from a component to the direct limit.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[simp]
      theorem Module.DirectLimit.of_f {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} [DecidableEq ι] {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} [Preorder ι] {G : ιType w} [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] {f : (i j : ι) → i jG i →ₗ[R] G j} [DecidableEq ι] [Nonempty ι] [IsDirected ι fun (x1 x2 : ι) => x1 x2] (z : Module.DirectLimit G f) :
      ∃ (i : ι) (x : G i), (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} [Preorder ι] {G : ιType w} [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] {f : (i j : ι) → i jG i →ₗ[R] G j} [DecidableEq ι] [Nonempty ι] [IsDirected ι fun (x1 x2 : ι) => x1 x2] {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
      noncomputable def Module.DirectLimit.lift (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) [DecidableEq ι] {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.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[simp]
        theorem Module.DirectLimit.lift_of {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} [DecidableEq ι] {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} [Preorder ι] {G : ιType w} [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] {f : (i j : ι) → i jG i →ₗ[R] G j} [DecidableEq ι] {P : Type u₁} [AddCommGroup P] [Module R P] [IsDirected ι fun (x1 x2 : ι) => x1 x2] (F : Module.DirectLimit G f →ₗ[R] P) (x : Module.DirectLimit G f) :
        F x = (Module.DirectLimit.lift R ι G f (fun (i : ι) => F ∘ₗ Module.DirectLimit.of R ι G f i) ) x
        theorem Module.DirectLimit.lift_injective {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} [DecidableEq ι] {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) [IsDirected ι fun (x1 x2 : ι) => x1 x2] (injective : ∀ (i : ι), Function.Injective (g i)) :
        noncomputable def Module.DirectLimit.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} [DecidableEq ι] {G' : ιType v'} [(i : ι) → AddCommGroup (G' i)] [(i : ι) → Module R (G' i)] {f' : (i j : ι) → i jG' i →ₗ[R] G' j} (g : (i : ι) → G i →ₗ[R] G' i) (hg : ∀ (i j : ι) (h : i j), g j ∘ₗ f i j h = f' i j h ∘ₗ g i) :

        Consider direct limits lim G and lim G' with direct system f and f' respectively, any family of linear maps gᵢ : Gᵢ ⟶ G'ᵢ such that g ∘ f = f' ∘ g induces a linear map lim G ⟶ lim G'.

        Equations
        Instances For
          @[simp]
          theorem Module.DirectLimit.map_apply_of {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} [DecidableEq ι] {G' : ιType v'} [(i : ι) → AddCommGroup (G' i)] [(i : ι) → Module R (G' i)] {f' : (i j : ι) → i jG' i →ₗ[R] G' j} (g : (i : ι) → G i →ₗ[R] G' i) (hg : ∀ (i j : ι) (h : i j), g j ∘ₗ f i j h = f' i j h ∘ₗ g i) {i : ι} (x : G i) :
          (Module.DirectLimit.map g hg) ((Module.DirectLimit.of R ι G f i) x) = (Module.DirectLimit.of R ι G' f' i) ((g i) x)
          @[simp]
          theorem Module.DirectLimit.map_id {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} [DecidableEq ι] [IsDirected ι fun (x1 x2 : ι) => x1 x2] :
          Module.DirectLimit.map (fun (x : ι) => LinearMap.id) = LinearMap.id
          theorem Module.DirectLimit.map_comp {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} [DecidableEq ι] {G' : ιType v'} [(i : ι) → AddCommGroup (G' i)] [(i : ι) → Module R (G' i)] {f' : (i j : ι) → i jG' i →ₗ[R] G' j} {G'' : ιType v''} [(i : ι) → AddCommGroup (G'' i)] [(i : ι) → Module R (G'' i)] {f'' : (i j : ι) → i jG'' i →ₗ[R] G'' j} [IsDirected ι fun (x1 x2 : ι) => x1 x2] (g₁ : (i : ι) → G i →ₗ[R] G' i) (g₂ : (i : ι) → G' i →ₗ[R] G'' i) (hg₁ : ∀ (i j : ι) (h : i j), g₁ j ∘ₗ f i j h = f' i j h ∘ₗ g₁ i) (hg₂ : ∀ (i j : ι) (h : i j), g₂ j ∘ₗ f' i j h = f'' i j h ∘ₗ g₂ i) :
          Module.DirectLimit.map g₂ hg₂ ∘ₗ Module.DirectLimit.map g₁ hg₁ = Module.DirectLimit.map (fun (i : ι) => g₂ i ∘ₗ g₁ i)
          noncomputable def Module.DirectLimit.congr {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} [DecidableEq ι] {G' : ιType v'} [(i : ι) → AddCommGroup (G' i)] [(i : ι) → Module R (G' i)] {f' : (i j : ι) → i jG' i →ₗ[R] G' j} [IsDirected ι fun (x1 x2 : ι) => x1 x2] (e : (i : ι) → G i ≃ₗ[R] G' i) (he : ∀ (i j : ι) (h : i j), (e j) ∘ₗ f i j h = f' i j h ∘ₗ (e i)) :

          Consider direct limits lim G and lim G' with direct system f and f' respectively, any family of equivalences eᵢ : Gᵢ ≅ G'ᵢ such that e ∘ f = f' ∘ e induces an equivalence lim G ≅ lim G'.

          Equations
          Instances For
            theorem Module.DirectLimit.congr_apply_of {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} [DecidableEq ι] {G' : ιType v'} [(i : ι) → AddCommGroup (G' i)] [(i : ι) → Module R (G' i)] {f' : (i j : ι) → i jG' i →ₗ[R] G' j} [IsDirected ι fun (x1 x2 : ι) => x1 x2] (e : (i : ι) → G i ≃ₗ[R] G' i) (he : ∀ (i j : ι) (h : i j), (e j) ∘ₗ f i j h = f' i j h ∘ₗ (e i)) {i : ι} (g : G i) :
            (Module.DirectLimit.congr e he) ((Module.DirectLimit.of R ι G f i) g) = (Module.DirectLimit.of R ι G' f' i) ((e i) g)
            theorem Module.DirectLimit.congr_symm_apply_of {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} [DecidableEq ι] {G' : ιType v'} [(i : ι) → AddCommGroup (G' i)] [(i : ι) → Module R (G' i)] {f' : (i j : ι) → i jG' i →ₗ[R] G' j} [IsDirected ι fun (x1 x2 : ι) => x1 x2] (e : (i : ι) → G i ≃ₗ[R] G' i) (he : ∀ (i j : ι) (h : i j), (e j) ∘ₗ f i j h = f' i j h ∘ₗ (e i)) {i : ι} (g : G' i) :
            (Module.DirectLimit.congr e he).symm ((Module.DirectLimit.of R ι G' f' i) g) = (Module.DirectLimit.of R ι G f i) ((e i).symm g)
            noncomputable def Module.DirectLimit.linearEquiv {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) [Nonempty ι] [IsDirected ι fun (x1 x2 : ι) => x1 x2] [DecidableEq ι] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 x2) => (f x1 x2 x3)] :

            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.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              theorem Module.DirectLimit.linearEquiv_of {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) [Nonempty ι] [IsDirected ι fun (x1 x2 : ι) => x1 x2] [DecidableEq ι] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 x2) => (f x1 x2 x3)] {i : ι} {g : G i} :
              (Module.DirectLimit.linearEquiv G f) ((Module.DirectLimit.of R ι G f i) g) = i, g
              theorem Module.DirectLimit.linearEquiv_symm_mk {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) [Nonempty ι] [IsDirected ι fun (x1 x2 : ι) => x1 x2] [DecidableEq ι] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 x2) => (f x1 x2 x3)] {g : (i : ι) × G i} :
              (Module.DirectLimit.linearEquiv G f).symm g = (Module.DirectLimit.of R ι G f g.fst) g.snd
              theorem Module.DirectLimit.of.zero_exact {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 (x1 x2 : ι) (x3 : x1 x2) => (f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 x2] [DecidableEq ι] {i : ι} {x : G i} (H : (Module.DirectLimit.of R ι G f i) x = 0) :
              ∃ (j : ι) (hij : i j), (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.

              noncomputable def AddCommGroup.DirectLimit {ι : Type v} [Preorder ι] (G : ιType w) [(i : ι) → AddCommGroup (G i)] [DecidableEq ι] (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.

              Equations
              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 : i j) => (f i j h)] :
                DirectedSystem G fun (i j : ι) (hij : i j) => (f i j hij).toIntLinearMap
                noncomputable instance AddCommGroup.DirectLimit.inst {ι : Type v} [Preorder ι] (G : ιType w) [(i : ι) → AddCommGroup (G i)] (f : (i j : ι) → i jG i →+ G j) [DecidableEq ι] :
                Equations
                noncomputable instance AddCommGroup.DirectLimit.instInhabited {ι : Type v} [Preorder ι] (G : ιType w) [(i : ι) → AddCommGroup (G i)] (f : (i j : ι) → i jG i →+ G j) [DecidableEq ι] :
                Equations
                noncomputable instance AddCommGroup.DirectLimit.instUniqueOfIsEmpty {ι : Type v} [Preorder ι] (G : ιType w) [(i : ι) → AddCommGroup (G i)] (f : (i j : ι) → i jG i →+ G j) [DecidableEq ι] [IsEmpty ι] :
                Equations
                noncomputable def AddCommGroup.DirectLimit.of {ι : Type v} [Preorder ι] (G : ιType w) [(i : ι) → AddCommGroup (G i)] (f : (i j : ι) → i jG i →+ G j) [DecidableEq ι] (i : ι) :

                The canonical map from a component to the direct limit.

                Equations
                Instances For
                  @[simp]
                  theorem AddCommGroup.DirectLimit.of_f {ι : Type v} [Preorder ι] {G : ιType w} [(i : ι) → AddCommGroup (G i)] {f : (i j : ι) → i jG i →+ G j} [DecidableEq ι] {i j : ι} (hij : i j) (x : G i) :
                  theorem AddCommGroup.DirectLimit.induction_on {ι : Type v} [Preorder ι] {G : ιType w} [(i : ι) → AddCommGroup (G i)] {f : (i j : ι) → i jG i →+ G j} [DecidableEq ι] [Nonempty ι] [IsDirected ι fun (x1 x2 : ι) => x1 x2] {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} [Preorder ι] {G : ιType w} [(i : ι) → AddCommGroup (G i)] {f : (i j : ι) → i jG i →+ G j} [DecidableEq ι] [IsDirected ι fun (x1 x2 : ι) => x1 x2] [DirectedSystem G fun (i j : ι) (h : i j) => (f i j h)] (i : ι) (x : G i) (h : (AddCommGroup.DirectLimit.of G f i) x = 0) :
                  ∃ (j : ι) (hij : i j), (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.

                  noncomputable def AddCommGroup.DirectLimit.lift {ι : Type v} [Preorder ι] (G : ιType w) [(i : ι) → AddCommGroup (G i)] (f : (i j : ι) → i jG i →+ G j) [DecidableEq ι] (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.

                  Equations
                  Instances For
                    @[simp]
                    theorem AddCommGroup.DirectLimit.lift_of {ι : Type v} [Preorder ι] {G : ιType w} [(i : ι) → AddCommGroup (G i)] {f : (i j : ι) → i jG i →+ G j} [DecidableEq ι] (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) :
                    theorem AddCommGroup.DirectLimit.lift_unique {ι : Type v} [Preorder ι] {G : ιType w} [(i : ι) → AddCommGroup (G i)] {f : (i j : ι) → i jG i →+ G j} [DecidableEq ι] (P : Type u₁) [AddCommGroup P] [IsDirected ι fun (x1 x2 : ι) => x1 x2] (F : AddCommGroup.DirectLimit G f →+ P) (x : AddCommGroup.DirectLimit G f) :
                    F x = (AddCommGroup.DirectLimit.lift G f P (fun (i : ι) => F.comp (AddCommGroup.DirectLimit.of G f i)) ) x
                    theorem AddCommGroup.DirectLimit.lift_injective {ι : Type v} [Preorder ι] {G : ιType w} [(i : ι) → AddCommGroup (G i)] {f : (i j : ι) → i jG i →+ G j} [DecidableEq ι] (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) [IsDirected ι fun (x1 x2 : ι) => x1 x2] (injective : ∀ (i : ι), Function.Injective (g i)) :
                    noncomputable def AddCommGroup.DirectLimit.map {ι : Type v} [Preorder ι] {G : ιType w} [(i : ι) → AddCommGroup (G i)] {f : (i j : ι) → i jG i →+ G j} [DecidableEq ι] {G' : ιType v'} [(i : ι) → AddCommGroup (G' i)] {f' : (i j : ι) → i jG' i →+ G' j} (g : (i : ι) → G i →+ G' i) (hg : ∀ (i j : ι) (h : i j), (g j).comp (f i j h) = (f' i j h).comp (g i)) :

                    Consider direct limits lim G and lim G' with direct system f and f' respectively, any family of group homomorphisms gᵢ : Gᵢ ⟶ G'ᵢ such that g ∘ f = f' ∘ g induces a group homomorphism lim G ⟶ lim G'.

                    Equations
                    Instances For
                      @[simp]
                      theorem AddCommGroup.DirectLimit.map_apply_of {ι : Type v} [Preorder ι] {G : ιType w} [(i : ι) → AddCommGroup (G i)] {f : (i j : ι) → i jG i →+ G j} [DecidableEq ι] {G' : ιType v'} [(i : ι) → AddCommGroup (G' i)] {f' : (i j : ι) → i jG' i →+ G' j} (g : (i : ι) → G i →+ G' i) (hg : ∀ (i j : ι) (h : i j), (g j).comp (f i j h) = (f' i j h).comp (g i)) {i : ι} (x : G i) :
                      @[simp]
                      theorem AddCommGroup.DirectLimit.map_id {ι : Type v} [Preorder ι] {G : ιType w} [(i : ι) → AddCommGroup (G i)] {f : (i j : ι) → i jG i →+ G j} [DecidableEq ι] [IsDirected ι fun (x1 x2 : ι) => x1 x2] :
                      theorem AddCommGroup.DirectLimit.map_comp {ι : Type v} [Preorder ι] {G : ιType w} [(i : ι) → AddCommGroup (G i)] {f : (i j : ι) → i jG i →+ G j} [DecidableEq ι] {G' : ιType v'} [(i : ι) → AddCommGroup (G' i)] {f' : (i j : ι) → i jG' i →+ G' j} {G'' : ιType v''} [(i : ι) → AddCommGroup (G'' i)] {f'' : (i j : ι) → i jG'' i →+ G'' j} [IsDirected ι fun (x1 x2 : ι) => x1 x2] (g₁ : (i : ι) → G i →+ G' i) (g₂ : (i : ι) → G' i →+ G'' i) (hg₁ : ∀ (i j : ι) (h : i j), (g₁ j).comp (f i j h) = (f' i j h).comp (g₁ i)) (hg₂ : ∀ (i j : ι) (h : i j), (g₂ j).comp (f' i j h) = (f'' i j h).comp (g₂ i)) :
                      (AddCommGroup.DirectLimit.map g₂ hg₂).comp (AddCommGroup.DirectLimit.map g₁ hg₁) = AddCommGroup.DirectLimit.map (fun (i : ι) => (g₂ i).comp (g₁ i))
                      noncomputable def AddCommGroup.DirectLimit.congr {ι : Type v} [Preorder ι] {G : ιType w} [(i : ι) → AddCommGroup (G i)] {f : (i j : ι) → i jG i →+ G j} [DecidableEq ι] {G' : ιType v'} [(i : ι) → AddCommGroup (G' i)] {f' : (i j : ι) → i jG' i →+ G' j} [IsDirected ι fun (x1 x2 : ι) => x1 x2] (e : (i : ι) → G i ≃+ G' i) (he : ∀ (i j : ι) (h : i j), (e j).toAddMonoidHom.comp (f i j h) = (f' i j h).comp (e i)) :

                      Consider direct limits lim G and lim G' with direct system f and f' respectively, any family of equivalences eᵢ : Gᵢ ≅ G'ᵢ such that e ∘ f = f' ∘ e induces an equivalence lim G ⟶ lim G'.

                      Equations
                      Instances For
                        theorem AddCommGroup.DirectLimit.congr_apply_of {ι : Type v} [Preorder ι] {G : ιType w} [(i : ι) → AddCommGroup (G i)] {f : (i j : ι) → i jG i →+ G j} [DecidableEq ι] {G' : ιType v'} [(i : ι) → AddCommGroup (G' i)] {f' : (i j : ι) → i jG' i →+ G' j} [IsDirected ι fun (x1 x2 : ι) => x1 x2] (e : (i : ι) → G i ≃+ G' i) (he : ∀ (i j : ι) (h : i j), (e j).toAddMonoidHom.comp (f i j h) = (f' i j h).comp (e i)) {i : ι} (g : G i) :
                        theorem AddCommGroup.DirectLimit.congr_symm_apply_of {ι : Type v} [Preorder ι] {G : ιType w} [(i : ι) → AddCommGroup (G i)] {f : (i j : ι) → i jG i →+ G j} [DecidableEq ι] {G' : ιType v'} [(i : ι) → AddCommGroup (G' i)] {f' : (i j : ι) → i jG' i →+ G' j} [IsDirected ι fun (x1 x2 : ι) => x1 x2] (e : (i : ι) → G i ≃+ G' i) (he : ∀ (i j : ι) (h : i j), (e j).toAddMonoidHom.comp (f i j h) = (f' i j h).comp (e i)) {i : ι} (g : G' i) :
                        noncomputable 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.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          noncomputable instance Ring.DirectLimit.commRing {ι : Type v} [Preorder ι] (G : ιType w) [(i : ι) → CommRing (G i)] (f : (i j : ι) → i jG iG j) :
                          Equations
                          • One or more equations did not get rendered due to their size.
                          noncomputable instance Ring.DirectLimit.ring {ι : Type v} [Preorder ι] (G : ιType w) [(i : ι) → CommRing (G i)] (f : (i j : ι) → i jG iG j) :
                          Equations
                          noncomputable instance Ring.DirectLimit.zero {ι : Type v} [Preorder ι] (G : ιType w) [(i : ι) → CommRing (G i)] (f : (i j : ι) → i jG iG j) :
                          Equations
                          noncomputable instance Ring.DirectLimit.instInhabited {ι : Type v} [Preorder ι] (G : ιType w) [(i : ι) → CommRing (G i)] (f : (i j : ι) → i jG iG j) :
                          Equations
                          noncomputable 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.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            @[simp]
                            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 (x1 x2 : ι) => x1 x2] (z : Ring.DirectLimit G f) :
                            ∃ (i : ι) (x : G i), (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 (x1 x2 : ι) => x1 x2] (q : Polynomial (Ring.DirectLimit G fun (i j : ι) (h : i j) => (f' i j h))) :
                            ∃ (i : ι) (p : Polynomial (G i)), Polynomial.map (Ring.DirectLimit.of G (fun (i j : ι) (h : i j) => (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 (x1 x2 : ι) => x1 x2] {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
                            noncomputable 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.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              @[simp]
                              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] [IsDirected ι fun (x1 x2 : ι) => x1 x2] (F : Ring.DirectLimit G f →+* P) (x : Ring.DirectLimit G f) :
                              F x = (Ring.DirectLimit.lift G f P (fun (i : ι) => F.comp (Ring.DirectLimit.of G f i)) ) x
                              theorem Ring.DirectLimit.lift_injective {ι : 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) [Nonempty ι] [IsDirected ι fun (x1 x2 : ι) => x1 x2] (injective : ∀ (i : ι), Function.Injective (g i)) :
                              noncomputable def Ring.DirectLimit.ringEquiv {ι : Type v} [Preorder ι] (G : ιType w) [(i : ι) → CommRing (G i)] (f' : (i j : ι) → i jG i →+* G j) [DirectedSystem G fun (i j : ι) (h : i j) => (f' i j h)] [IsDirected ι fun (x1 x2 : ι) => x1 x2] [Nonempty ι] :
                              (Ring.DirectLimit G fun (x1 x2 : ι) (x3 : x1 x2) => (f' x1 x2 x3)) ≃+* DirectLimit G f'

                              The direct limit constructed as a quotient of the free commutative ring is isomorphic to the direct limit constructed as a quotient of the disjoint union.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                theorem Ring.DirectLimit.ringEquiv_of {ι : Type v} [Preorder ι] (G : ιType w) [(i : ι) → CommRing (G i)] (f' : (i j : ι) → i jG i →+* G j) [DirectedSystem G fun (i j : ι) (h : i j) => (f' i j h)] [IsDirected ι fun (x1 x2 : ι) => x1 x2] [Nonempty ι] {i : ι} {g : G i} :
                                (Ring.DirectLimit.ringEquiv G f') ((Ring.DirectLimit.of G (fun (x1 x2 : ι) (x3 : x1 x2) => (f' x1 x2 x3)) i) g) = i, g
                                theorem Ring.DirectLimit.ringEquiv_symm_mk {ι : Type v} [Preorder ι] (G : ιType w) [(i : ι) → CommRing (G i)] (f' : (i j : ι) → i jG i →+* G j) [DirectedSystem G fun (i j : ι) (h : i j) => (f' i j h)] [IsDirected ι fun (x1 x2 : ι) => x1 x2] [Nonempty ι] {g : (i : ι) × G i} :
                                (Ring.DirectLimit.ringEquiv G f').symm g = (Ring.DirectLimit.of G (fun (x1 x2 : ι) (x3 : x1 x2) => (f' x1 x2 x3)) g.fst) g.snd
                                theorem Ring.DirectLimit.of.zero_exact {ι : Type v} [Preorder ι] {G : ιType w} [(i : ι) → CommRing (G i)] {f' : (i j : ι) → i jG i →+* G j} [DirectedSystem G fun (i j : ι) (h : i j) => (f' i j h)] [IsDirected ι fun (x1 x2 : ι) => x1 x2] {i : ι} {x : G i} (hix : (Ring.DirectLimit.of G (fun (x1 x2 : ι) (x3 : x1 x2) => (f' x1 x2 x3)) i) x = 0) :
                                ∃ (j : ι) (hij : i j), (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} [Preorder ι] {G : ιType w} [(i : ι) → CommRing (G i)] (f' : (i j : ι) → i jG i →+* G j) [IsDirected ι fun (x1 x2 : ι) => x1 x2] [DirectedSystem G fun (i j : ι) (h : i j) => (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 : i j) => (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.

                                noncomputable def Ring.DirectLimit.map {ι : Type v} [Preorder ι] {G : ιType w} [(i : ι) → CommRing (G i)] {f : (i j : ι) → i jG i →+* G j} {G' : ιType v'} [(i : ι) → CommRing (G' i)] {f' : (i j : ι) → i jG' i →+* G' j} (g : (i : ι) → G i →+* G' i) (hg : ∀ (i j : ι) (h : i j), (g j).comp (f i j h) = (f' i j h).comp (g i)) :
                                (Ring.DirectLimit G fun (x x_1 : ι) (h : x x_1) => (f x x_1 h)) →+* Ring.DirectLimit G' fun (x x_1 : ι) (h : x x_1) => (f' x x_1 h)

                                Consider direct limits lim G and lim G' with direct system f and f' respectively, any family of ring homomorphisms gᵢ : Gᵢ ⟶ G'ᵢ such that g ∘ f = f' ∘ g induces a ring homomorphism lim G ⟶ lim G'.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  @[simp]
                                  theorem Ring.DirectLimit.map_apply_of {ι : Type v} [Preorder ι] {G : ιType w} [(i : ι) → CommRing (G i)] {f : (i j : ι) → i jG i →+* G j} {G' : ιType v'} [(i : ι) → CommRing (G' i)] {f' : (i j : ι) → i jG' i →+* G' j} (g : (i : ι) → G i →+* G' i) (hg : ∀ (i j : ι) (h : i j), (g j).comp (f i j h) = (f' i j h).comp (g i)) {i : ι} (x : G i) :
                                  (Ring.DirectLimit.map g hg) ((Ring.DirectLimit.of G (fun (x x_1 : ι) (h : x x_1) => (f x x_1 h)) i) x) = (Ring.DirectLimit.of G' (fun (x x_1 : ι) (h : x x_1) => (f' x x_1 h)) i) ((g i) x)
                                  @[simp]
                                  theorem Ring.DirectLimit.map_id {ι : Type v} [Preorder ι] {G : ιType w} [(i : ι) → CommRing (G i)] {f : (i j : ι) → i jG i →+* G j} [Nonempty ι] [IsDirected ι fun (x1 x2 : ι) => x1 x2] :
                                  Ring.DirectLimit.map (fun (x : ι) => RingHom.id (G x)) = RingHom.id (Ring.DirectLimit G fun (x x_1 : ι) (h : x x_1) => (f x x_1 h))
                                  theorem Ring.DirectLimit.map_comp {ι : Type v} [Preorder ι] {G : ιType w} [(i : ι) → CommRing (G i)] {f : (i j : ι) → i jG i →+* G j} {G' : ιType v'} [(i : ι) → CommRing (G' i)] {f' : (i j : ι) → i jG' i →+* G' j} {G'' : ιType v''} [(i : ι) → CommRing (G'' i)] {f'' : (i j : ι) → i jG'' i →+* G'' j} [Nonempty ι] [IsDirected ι fun (x1 x2 : ι) => x1 x2] (g₁ : (i : ι) → G i →+* G' i) (g₂ : (i : ι) → G' i →+* G'' i) (hg₁ : ∀ (i j : ι) (h : i j), (g₁ j).comp (f i j h) = (f' i j h).comp (g₁ i)) (hg₂ : ∀ (i j : ι) (h : i j), (g₂ j).comp (f' i j h) = (f'' i j h).comp (g₂ i)) :
                                  (Ring.DirectLimit.map g₂ hg₂).comp (Ring.DirectLimit.map g₁ hg₁) = Ring.DirectLimit.map (fun (i : ι) => (g₂ i).comp (g₁ i))
                                  noncomputable def Ring.DirectLimit.congr {ι : Type v} [Preorder ι] {G : ιType w} [(i : ι) → CommRing (G i)] {f : (i j : ι) → i jG i →+* G j} {G' : ιType v'} [(i : ι) → CommRing (G' i)] {f' : (i j : ι) → i jG' i →+* G' j} [Nonempty ι] [IsDirected ι fun (x1 x2 : ι) => x1 x2] (e : (i : ι) → G i ≃+* G' i) (he : ∀ (i j : ι) (h : i j), (e j).toRingHom.comp (f i j h) = (f' i j h).comp (e i)) :
                                  (Ring.DirectLimit G fun (x x_1 : ι) (h : x x_1) => (f x x_1 h)) ≃+* Ring.DirectLimit G' fun (x x_1 : ι) (h : x x_1) => (f' x x_1 h)

                                  Consider direct limits lim G and lim G' with direct system f and f' respectively, any family of equivalences eᵢ : Gᵢ ≅ G'ᵢ such that e ∘ f = f' ∘ e induces an equivalence lim G ⟶ lim G'.

                                  Equations
                                  Instances For
                                    theorem Ring.DirectLimit.congr_apply_of {ι : Type v} [Preorder ι] {G : ιType w} [(i : ι) → CommRing (G i)] {f : (i j : ι) → i jG i →+* G j} {G' : ιType v'} [(i : ι) → CommRing (G' i)] {f' : (i j : ι) → i jG' i →+* G' j} [Nonempty ι] [IsDirected ι fun (x1 x2 : ι) => x1 x2] (e : (i : ι) → G i ≃+* G' i) (he : ∀ (i j : ι) (h : i j), (e j).toRingHom.comp (f i j h) = (f' i j h).comp (e i)) {i : ι} (g : G i) :
                                    (Ring.DirectLimit.congr e he) ((Ring.DirectLimit.of G (fun (x x_1 : ι) (h : x x_1) => (f x x_1 h)) i) g) = (Ring.DirectLimit.of G' (fun (x x_1 : ι) (h : x x_1) => (f' x x_1 h)) i) ((e i) g)
                                    theorem Ring.DirectLimit.congr_symm_apply_of {ι : Type v} [Preorder ι] {G : ιType w} [(i : ι) → CommRing (G i)] {f : (i j : ι) → i jG i →+* G j} {G' : ιType v'} [(i : ι) → CommRing (G' i)] {f' : (i j : ι) → i jG' i →+* G' j} [Nonempty ι] [IsDirected ι fun (x1 x2 : ι) => x1 x2] (e : (i : ι) → G i ≃+* G' i) (he : ∀ (i j : ι) (h : i j), (e j).toRingHom.comp (f i j h) = (f' i j h).comp (e i)) {i : ι} (g : G' i) :
                                    (Ring.DirectLimit.congr e he).symm ((Ring.DirectLimit.of G' (fun (x x_1 : ι) (h : x x_1) => (f' x x_1 h)) i) g) = (Ring.DirectLimit.of G (fun (x x_1 : ι) (h : x x_1) => (f x x_1 h)) i) ((e i).symm g)
                                    instance Field.DirectLimit.nontrivial {ι : Type v} [Preorder ι] (G : ιType w) [Nonempty ι] [IsDirected ι fun (x1 x2 : ι) => x1 x2] [(i : ι) → Field (G i)] (f' : (i j : ι) → i jG i →+* G j) [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 x2) => (f' x1 x2 x3)] :
                                    Nontrivial (Ring.DirectLimit G fun (x1 x2 : ι) (x3 : x1 x2) => (f' x1 x2 x3))
                                    theorem Field.DirectLimit.exists_inv {ι : Type v} [Preorder ι] (G : ιType w) [Nonempty ι] [IsDirected ι fun (x1 x2 : ι) => x1 x2] [(i : ι) → Field (G i)] (f : (i j : ι) → i jG iG j) {p : Ring.DirectLimit G f} :
                                    p 0∃ (y : Ring.DirectLimit G f), p * y = 1
                                    noncomputable def Field.DirectLimit.inv {ι : Type v} [Preorder ι] (G : ιType w) [Nonempty ι] [IsDirected ι fun (x1 x2 : ι) => x1 x2] [(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.

                                    Equations
                                    Instances For
                                      theorem Field.DirectLimit.mul_inv_cancel {ι : Type v} [Preorder ι] (G : ιType w) [Nonempty ι] [IsDirected ι fun (x1 x2 : ι) => x1 x2] [(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 (x1 x2 : ι) => x1 x2] [(i : ι) → Field (G i)] (f : (i j : ι) → i jG iG j) {p : Ring.DirectLimit G f} (hp : p 0) :
                                      @[reducible, inline]
                                      noncomputable abbrev Field.DirectLimit.field {ι : Type v} [Preorder ι] (G : ιType w) [Nonempty ι] [IsDirected ι fun (x1 x2 : ι) => x1 x2] [(i : ι) → Field (G i)] (f' : (i j : ι) → i jG i →+* G j) [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 x2) => (f' x1 x2 x3)] :
                                      Field (Ring.DirectLimit G fun (x1 x2 : ι) (x3 : x1 x2) => (f' x1 x2 x3))

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

                                      Equations
                                      Instances For