mathlib documentation

algebra.direct_limit

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".

@[class]
structure directed_system {ι : Type v} [directed_order ι] (G : ι → Type w) :
(Π (i j : ι), i jG iG j) → Prop
  • 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 _ x

A directed system is a functor from the category (directed poset) to another category. This is used for abelian groups and rings and fields because their maps are not bundled. See module.directed_system

Instances
@[class]
structure module.directed_system {R : Type u} [ring R] {ι : Type v} [directed_order ι] (G : ι → Type w) [Π (i : ι), add_comm_group (G i)] [Π (i : ι), module R (G i)] :
(Π (i j : ι), i j(G i →ₗ[R] G j)) → Prop
  • 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 _) x

A directed system is a functor from the category (directed poset) to the category of R-modules.

def module.direct_limit {R : Type u} [ring R] {ι : Type v} [dec_ι : decidable_eq ι] [directed_order ι] (G : ι → Type w) [Π (i : ι), add_comm_group (G i)] [Π (i : ι), module R (G i)] :
(Π (i j : ι), i j(G i →ₗ[R] G j))Type (max v w)

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

Equations
@[instance]
def module.direct_limit.add_comm_group {R : Type u} [ring R] {ι : Type v} [dec_ι : decidable_eq ι] [directed_order ι] (G : ι → Type w) [Π (i : ι), add_comm_group (G i)] [Π (i : ι), module R (G i)] (f : Π (i j : ι), i j(G i →ₗ[R] G j)) :

Equations
@[instance]
def module.direct_limit.semimodule {R : Type u} [ring R] {ι : Type v} [dec_ι : decidable_eq ι] [directed_order ι] (G : ι → Type w) [Π (i : ι), add_comm_group (G i)] [Π (i : ι), module R (G i)] (f : Π (i j : ι), i j(G i →ₗ[R] G j)) :

Equations
@[instance]
def module.direct_limit.inhabited {R : Type u} [ring R] {ι : Type v} [dec_ι : decidable_eq ι] [directed_order ι] (G : ι → Type w) [Π (i : ι), add_comm_group (G i)] [Π (i : ι), module R (G i)] (f : Π (i j : ι), i j(G i →ₗ[R] G j)) :

Equations
def module.direct_limit.of (R : Type u) [ring R] (ι : Type v) [dec_ι : decidable_eq ι] [directed_order ι] (G : ι → Type w) [Π (i : ι), add_comm_group (G i)] [Π (i : ι), module R (G i)] (f : Π (i j : ι), i j(G i →ₗ[R] G j)) (i : ι) :

The canonical map from a component to the direct limit.

Equations
@[simp]
theorem module.direct_limit.of_f {R : Type u} [ring R] {ι : Type v} [dec_ι : decidable_eq ι] [directed_order ι] {G : ι → Type w} [Π (i : ι), add_comm_group (G i)] [Π (i : ι), module R (G i)] {f : Π (i j : ι), i j(G i →ₗ[R] G j)} {i j : ι} {hij : i j} {x : G i} :
(module.direct_limit.of R ι G f j) ((f i j hij) x) = (module.direct_limit.of R ι G f i) x

theorem module.direct_limit.exists_of {R : Type u} [ring R] {ι : Type v} [dec_ι : decidable_eq ι] [directed_order ι] {G : ι → Type w} [Π (i : ι), add_comm_group (G i)] [Π (i : ι), module R (G i)] {f : Π (i j : ι), i j(G i →ₗ[R] G j)} [nonempty ι] (z : module.direct_limit G f) :
∃ (i : ι) (x : G i), (module.direct_limit.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.direct_limit.induction_on {R : Type u} [ring R] {ι : Type v} [dec_ι : decidable_eq ι] [directed_order ι] {G : ι → Type w} [Π (i : ι), add_comm_group (G i)] [Π (i : ι), module R (G i)] {f : Π (i j : ι), i j(G i →ₗ[R] G j)} [nonempty ι] {C : module.direct_limit G f → Prop} (z : module.direct_limit G f) :
(∀ (i : ι) (x : G i), C ((module.direct_limit.of R ι G f i) x))C z

def module.direct_limit.lift (R : Type u) [ring R] (ι : Type v) [dec_ι : decidable_eq ι] [directed_order ι] (G : ι → Type w) [Π (i : ι), add_comm_group (G i)] [Π (i : ι), module R (G i)] (f : Π (i j : ι), i j(G i →ₗ[R] G j)) {P : Type u₁} [add_comm_group P] [module R P] (g : Π (i : ι), G i →ₗ[R] P) :
(∀ (i j : ι) (hij : i j) (x : G i), (g j) ((f i j hij) x) = (g i) x)(module.direct_limit G f →ₗ[R] P)

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
theorem module.direct_limit.lift_of {R : Type u} [ring R] {ι : Type v} [dec_ι : decidable_eq ι] [directed_order ι] {G : ι → Type w} [Π (i : ι), add_comm_group (G i)] [Π (i : ι), module R (G i)] {f : Π (i j : ι), i j(G i →ₗ[R] G j)} {P : Type u₁} [add_comm_group 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.direct_limit.lift R ι G f g Hg) ((module.direct_limit.of R ι G f i) x) = (g i) x

theorem module.direct_limit.lift_unique {R : Type u} [ring R] {ι : Type v} [dec_ι : decidable_eq ι] [directed_order ι] {G : ι → Type w} [Π (i : ι), add_comm_group (G i)] [Π (i : ι), module R (G i)] {f : Π (i j : ι), i j(G i →ₗ[R] G j)} {P : Type u₁} [add_comm_group P] [module R P] [nonempty ι] (F : module.direct_limit G f →ₗ[R] P) (x : module.direct_limit G f) :
F x = (module.direct_limit.lift R ι G f (λ (i : ι), F.comp (module.direct_limit.of R ι G f i)) _) x

def module.direct_limit.totalize {R : Type u} [ring R] {ι : Type v} [directed_order ι] (G : ι → Type w) [Π (i : ι), add_comm_group (G i)] [Π (i : ι), module R (G i)] (f : Π (i j : ι), i j(G 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.

Equations
theorem module.direct_limit.totalize_apply {R : Type u} [ring R] {ι : Type v} [directed_order ι] {G : ι → Type w} [Π (i : ι), add_comm_group (G i)] [Π (i : ι), module R (G i)] {f : Π (i j : ι), i j(G i →ₗ[R] G j)} (i j : ι) (x : G i) :
(module.direct_limit.totalize G f i j) x = dite (i j) (λ (h : i j), (f i j h) x) (λ (h : ¬i j), 0)

theorem module.direct_limit.to_module_totalize_of_le {R : Type u} [ring R] {ι : Type v} [dec_ι : decidable_eq ι] [directed_order ι] {G : ι → Type w} [Π (i : ι), add_comm_group (G i)] [Π (i : ι), module R (G i)] {f : Π (i j : ι), i j(G i →ₗ[R] G j)} [module.directed_system G f] {x : direct_sum ι G} {i j : ι} (hij : i j) :
(∀ (k : ι), k dfinsupp.support xk i)(direct_sum.to_module R ι (G j) (λ (k : ι), module.direct_limit.totalize G f k j)) x = (f i j hij) ((direct_sum.to_module R ι (G i) (λ (k : ι), module.direct_limit.totalize G f k i)) x)

theorem module.direct_limit.of.zero_exact_aux {R : Type u} [ring R] {ι : Type v} [dec_ι : decidable_eq ι] [directed_order ι] {G : ι → Type w} [Π (i : ι), add_comm_group (G i)] [Π (i : ι), module R (G i)] {f : Π (i j : ι), i j(G i →ₗ[R] G j)} [module.directed_system G f] [nonempty ι] {x : direct_sum ι G} :
submodule.quotient.mk x = 0(∃ (j : ι), (∀ (k : ι), k dfinsupp.support xk j) (direct_sum.to_module R ι (G j) (λ (i : ι), module.direct_limit.totalize G f i j)) x = 0)

theorem module.direct_limit.of.zero_exact {R : Type u} [ring R] {ι : Type v} [dec_ι : decidable_eq ι] [directed_order ι] {G : ι → Type w} [Π (i : ι), add_comm_group (G i)] [Π (i : ι), module R (G i)] {f : Π (i j : ι), i j(G i →ₗ[R] G j)} [module.directed_system G f] {i : ι} {x : G i} :
(module.direct_limit.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.

def add_comm_group.direct_limit {ι : Type v} [dec_ι : decidable_eq ι] [directed_order ι] (G : ι → Type w) [Π (i : ι), add_comm_group (G i)] (f : Π (i j : ι), i jG iG j) [∀ (i j : ι) (hij : i j), is_add_group_hom (f i j hij)] :
Type (max v w)

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

Equations
theorem add_comm_group.direct_limit.directed_system {ι : Type v} [directed_order ι] (G : ι → Type w) [Π (i : ι), add_comm_group (G i)] (f : Π (i j : ι), i jG iG j) [∀ (i j : ι) (hij : i j), is_add_group_hom (f i j hij)] [directed_system G f] :
module.directed_system G (λ (i j : ι) (hij : i j), (add_monoid_hom.of (f i j hij)).to_int_linear_map)

@[instance]
def add_comm_group.direct_limit.add_comm_group {ι : Type v} [dec_ι : decidable_eq ι] [directed_order ι] (G : ι → Type w) [Π (i : ι), add_comm_group (G i)] (f : Π (i j : ι), i jG iG j) [∀ (i j : ι) (hij : i j), is_add_group_hom (f i j hij)] :

Equations
@[instance]
def add_comm_group.direct_limit.inhabited {ι : Type v} [dec_ι : decidable_eq ι] [directed_order ι] (G : ι → Type w) [Π (i : ι), add_comm_group (G i)] (f : Π (i j : ι), i jG iG j) [∀ (i j : ι) (hij : i j), is_add_group_hom (f i j hij)] :

Equations
def add_comm_group.direct_limit.of {ι : Type v} [dec_ι : decidable_eq ι] [directed_order ι] (G : ι → Type w) [Π (i : ι), add_comm_group (G i)] (f : Π (i j : ι), i jG iG j) [∀ (i j : ι) (hij : i j), is_add_group_hom (f i j hij)] (i : ι) :

The canonical map from a component to the direct limit.

Equations
@[instance]
def add_comm_group.direct_limit.of.is_add_group_hom {ι : Type v} [dec_ι : decidable_eq ι] [directed_order ι] {G : ι → Type w} [Π (i : ι), add_comm_group (G i)] {f : Π (i j : ι), i jG iG j} [∀ (i j : ι) (hij : i j), is_add_group_hom (f i j hij)] (i : ι) :

@[simp]
theorem add_comm_group.direct_limit.of_f {ι : Type v} [dec_ι : decidable_eq ι] [directed_order ι] {G : ι → Type w} [Π (i : ι), add_comm_group (G i)] {f : Π (i j : ι), i jG iG j} [∀ (i j : ι) (hij : i j), is_add_group_hom (f i j hij)] {i j : ι} (hij : i j) (x : G i) :

@[simp]
theorem add_comm_group.direct_limit.of_zero {ι : Type v} [dec_ι : decidable_eq ι] [directed_order ι] {G : ι → Type w} [Π (i : ι), add_comm_group (G i)] {f : Π (i j : ι), i jG iG j} [∀ (i j : ι) (hij : i j), is_add_group_hom (f i j hij)] (i : ι) :

@[simp]
theorem add_comm_group.direct_limit.of_add {ι : Type v} [dec_ι : decidable_eq ι] [directed_order ι] {G : ι → Type w} [Π (i : ι), add_comm_group (G i)] {f : Π (i j : ι), i jG iG j} [∀ (i j : ι) (hij : i j), is_add_group_hom (f i j hij)] (i : ι) (x y : G i) :

@[simp]
theorem add_comm_group.direct_limit.of_neg {ι : Type v} [dec_ι : decidable_eq ι] [directed_order ι] {G : ι → Type w} [Π (i : ι), add_comm_group (G i)] {f : Π (i j : ι), i jG iG j} [∀ (i j : ι) (hij : i j), is_add_group_hom (f i j hij)] (i : ι) (x : G i) :

@[simp]
theorem add_comm_group.direct_limit.of_sub {ι : Type v} [dec_ι : decidable_eq ι] [directed_order ι] {G : ι → Type w} [Π (i : ι), add_comm_group (G i)] {f : Π (i j : ι), i jG iG j} [∀ (i j : ι) (hij : i j), is_add_group_hom (f i j hij)] (i : ι) (x y : G i) :

theorem add_comm_group.direct_limit.induction_on {ι : Type v} [dec_ι : decidable_eq ι] [directed_order ι] {G : ι → Type w} [Π (i : ι), add_comm_group (G i)] {f : Π (i j : ι), i jG iG j} [∀ (i j : ι) (hij : i j), is_add_group_hom (f i j hij)] [nonempty ι] {C : add_comm_group.direct_limit G f → Prop} (z : add_comm_group.direct_limit G f) :
(∀ (i : ι) (x : G i), C (add_comm_group.direct_limit.of G f i x))C z

theorem add_comm_group.direct_limit.of.zero_exact {ι : Type v} [dec_ι : decidable_eq ι] [directed_order ι] {G : ι → Type w} [Π (i : ι), add_comm_group (G i)] {f : Π (i j : ι), i jG iG j} [∀ (i j : ι) (hij : i j), is_add_group_hom (f i j hij)] [directed_system G f] (i : ι) (x : G i) :
add_comm_group.direct_limit.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.

def add_comm_group.direct_limit.lift {ι : Type v} [dec_ι : decidable_eq ι] [directed_order ι] (G : ι → Type w) [Π (i : ι), add_comm_group (G i)] (f : Π (i j : ι), i jG iG j) [∀ (i j : ι) (hij : i j), is_add_group_hom (f i j hij)] (P : Type u₁) [add_comm_group P] (g : Π (i : ι), G i → P) [∀ (i : ι), is_add_group_hom (g i)] :
(∀ (i j : ι) (hij : i j) (x : G i), g j (f i j hij x) = g i x)add_comm_group.direct_limit G f → P

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
@[instance]
def add_comm_group.direct_limit.lift.is_add_group_hom {ι : Type v} [dec_ι : decidable_eq ι] [directed_order ι] {G : ι → Type w} [Π (i : ι), add_comm_group (G i)] {f : Π (i j : ι), i jG iG j} [∀ (i j : ι) (hij : i j), is_add_group_hom (f i j hij)] (P : Type u₁) [add_comm_group P] (g : Π (i : ι), G i → P) [∀ (i : ι), is_add_group_hom (g i)] (Hg : ∀ (i j : ι) (hij : i j) (x : G i), g j (f i j hij x) = g i x) :

@[simp]
theorem add_comm_group.direct_limit.lift_of {ι : Type v} [dec_ι : decidable_eq ι] [directed_order ι] {G : ι → Type w} [Π (i : ι), add_comm_group (G i)] {f : Π (i j : ι), i jG iG j} [∀ (i j : ι) (hij : i j), is_add_group_hom (f i j hij)] (P : Type u₁) [add_comm_group P] (g : Π (i : ι), G i → P) [∀ (i : ι), is_add_group_hom (g i)] (Hg : ∀ (i j : ι) (hij : i j) (x : G i), g j (f i j hij x) = g i x) (i : ι) (x : G i) :

@[simp]
theorem add_comm_group.direct_limit.lift_zero {ι : Type v} [dec_ι : decidable_eq ι] [directed_order ι] {G : ι → Type w} [Π (i : ι), add_comm_group (G i)] {f : Π (i j : ι), i jG iG j} [∀ (i j : ι) (hij : i j), is_add_group_hom (f i j hij)] (P : Type u₁) [add_comm_group P] (g : Π (i : ι), G i → P) [∀ (i : ι), is_add_group_hom (g i)] (Hg : ∀ (i j : ι) (hij : i j) (x : G i), g j (f i j hij x) = g i x) :

@[simp]
theorem add_comm_group.direct_limit.lift_add {ι : Type v} [dec_ι : decidable_eq ι] [directed_order ι] {G : ι → Type w} [Π (i : ι), add_comm_group (G i)] {f : Π (i j : ι), i jG iG j} [∀ (i j : ι) (hij : i j), is_add_group_hom (f i j hij)] (P : Type u₁) [add_comm_group P] (g : Π (i : ι), G i → P) [∀ (i : ι), is_add_group_hom (g i)] (Hg : ∀ (i j : ι) (hij : i j) (x : G i), g j (f i j hij x) = g i x) (x y : add_comm_group.direct_limit G f) :

@[simp]
theorem add_comm_group.direct_limit.lift_neg {ι : Type v} [dec_ι : decidable_eq ι] [directed_order ι] {G : ι → Type w} [Π (i : ι), add_comm_group (G i)] {f : Π (i j : ι), i jG iG j} [∀ (i j : ι) (hij : i j), is_add_group_hom (f i j hij)] (P : Type u₁) [add_comm_group P] (g : Π (i : ι), G i → P) [∀ (i : ι), is_add_group_hom (g i)] (Hg : ∀ (i j : ι) (hij : i j) (x : G i), g j (f i j hij x) = g i x) (x : add_comm_group.direct_limit G f) :

@[simp]
theorem add_comm_group.direct_limit.lift_sub {ι : Type v} [dec_ι : decidable_eq ι] [directed_order ι] {G : ι → Type w} [Π (i : ι), add_comm_group (G i)] {f : Π (i j : ι), i jG iG j} [∀ (i j : ι) (hij : i j), is_add_group_hom (f i j hij)] (P : Type u₁) [add_comm_group P] (g : Π (i : ι), G i → P) [∀ (i : ι), is_add_group_hom (g i)] (Hg : ∀ (i j : ι) (hij : i j) (x : G i), g j (f i j hij x) = g i x) (x y : add_comm_group.direct_limit G f) :

theorem add_comm_group.direct_limit.lift_unique {ι : Type v} [dec_ι : decidable_eq ι] [directed_order ι] {G : ι → Type w} [Π (i : ι), add_comm_group (G i)] {f : Π (i j : ι), i jG iG j} [∀ (i j : ι) (hij : i j), is_add_group_hom (f i j hij)] (P : Type u₁) [add_comm_group P] [nonempty ι] (F : add_comm_group.direct_limit G f → P) [is_add_group_hom F] (x : add_comm_group.direct_limit G f) :
F x = add_comm_group.direct_limit.lift G f P (λ (i : ι) (x : G i), F (add_comm_group.direct_limit.of G f i x)) _ x

def ring.direct_limit {ι : Type v} [directed_order ι] (G : ι → Type w) [Π (i : ι), comm_ring (G i)] :
(Π (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
@[instance]
def ring.direct_limit.comm_ring {ι : Type v} [directed_order ι] (G : ι → Type w) [Π (i : ι), comm_ring (G i)] (f : Π (i j : ι), i jG iG j) :

Equations
@[instance]
def ring.direct_limit.ring {ι : Type v} [directed_order ι] (G : ι → Type w) [Π (i : ι), comm_ring (G i)] (f : Π (i j : ι), i jG iG j) :

Equations
@[instance]
def ring.direct_limit.inhabited {ι : Type v} [directed_order ι] (G : ι → Type w) [Π (i : ι), comm_ring (G i)] (f : Π (i j : ι), i jG iG j) :

Equations
def ring.direct_limit.of {ι : Type v} [directed_order ι] (G : ι → Type w) [Π (i : ι), comm_ring (G i)] (f : Π (i j : ι), i jG iG j) (i : ι) :
G iring.direct_limit G f

The canonical map from a component to the direct limit.

Equations
@[instance]
def ring.direct_limit.of.is_ring_hom {ι : Type v} [directed_order ι] {G : ι → Type w} [Π (i : ι), comm_ring (G i)] {f : Π (i j : ι), i jG iG j} (i : ι) :

@[simp]
theorem ring.direct_limit.of_f {ι : Type v} [directed_order ι] {G : ι → Type w} [Π (i : ι), comm_ring (G i)] {f : Π (i j : ι), i jG iG j} {i j : ι} (hij : i j) (x : G i) :
ring.direct_limit.of G f j (f i j hij x) = ring.direct_limit.of G f i x

@[simp]
theorem ring.direct_limit.of_zero {ι : Type v} [directed_order ι] {G : ι → Type w} [Π (i : ι), comm_ring (G i)] {f : Π (i j : ι), i jG iG j} (i : ι) :

@[simp]
theorem ring.direct_limit.of_one {ι : Type v} [directed_order ι] {G : ι → Type w} [Π (i : ι), comm_ring (G i)] {f : Π (i j : ι), i jG iG j} (i : ι) :

@[simp]
theorem ring.direct_limit.of_add {ι : Type v} [directed_order ι] {G : ι → Type w} [Π (i : ι), comm_ring (G i)] {f : Π (i j : ι), i jG iG j} (i : ι) (x y : G i) :

@[simp]
theorem ring.direct_limit.of_neg {ι : Type v} [directed_order ι] {G : ι → Type w} [Π (i : ι), comm_ring (G i)] {f : Π (i j : ι), i jG iG j} (i : ι) (x : G i) :

@[simp]
theorem ring.direct_limit.of_sub {ι : Type v} [directed_order ι] {G : ι → Type w} [Π (i : ι), comm_ring (G i)] {f : Π (i j : ι), i jG iG j} (i : ι) (x y : G i) :

@[simp]
theorem ring.direct_limit.of_mul {ι : Type v} [directed_order ι] {G : ι → Type w} [Π (i : ι), comm_ring (G i)] {f : Π (i j : ι), i jG iG j} (i : ι) (x y : G i) :

@[simp]
theorem ring.direct_limit.of_pow {ι : Type v} [directed_order ι] {G : ι → Type w} [Π (i : ι), comm_ring (G i)] {f : Π (i j : ι), i jG iG j} (i : ι) (x : G i) (n : ) :

theorem ring.direct_limit.exists_of {ι : Type v} [directed_order ι] {G : ι → Type w} [Π (i : ι), comm_ring (G i)] {f : Π (i j : ι), i jG iG j} [nonempty ι] (z : ring.direct_limit G f) :
∃ (i : ι) (x : G i), ring.direct_limit.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.direct_limit.polynomial.exists_of {ι : Type v} [directed_order ι] {G : ι → Type w} [Π (i : ι), comm_ring (G i)] {f : Π (i j : ι), i jG iG j} [∀ (i j : ι) (hij : i j), is_ring_hom (f i j hij)] [nonempty ι] (q : polynomial (ring.direct_limit G f)) :
∃ (i : ι) (p : polynomial (G i)), polynomial.map (ring_hom.of (ring.direct_limit.of G f i)) p = q

theorem ring.direct_limit.induction_on {ι : Type v} [directed_order ι] {G : ι → Type w} [Π (i : ι), comm_ring (G i)] {f : Π (i j : ι), i jG iG j} [nonempty ι] {C : ring.direct_limit G f → Prop} (z : ring.direct_limit G f) :
(∀ (i : ι) (x : G i), C (ring.direct_limit.of G f i x))C z

theorem ring.direct_limit.of.zero_exact_aux2 {ι : Type v} [directed_order ι] (G : ι → Type w) [Π (i : ι), comm_ring (G i)] (f : Π (i j : ι), i jG iG j) [∀ (i j : ι) (hij : i j), is_ring_hom (f i j hij)] [directed_system G f] {x : free_comm_ring (Σ (i : ι), G i)} {s t : set (Σ (i : ι), G i)} (hxs : x.is_supported s) {j k : ι} (hj : ∀ (z : Σ (i : ι), G i), z sz.fst j) (hk : ∀ (z : Σ (i : ι), G i), z tz.fst k) (hjk : j k) :
s tf j k hjk ((free_comm_ring.lift (λ (ix : s), f ix.val.fst j _ ix.val.snd)) ((free_comm_ring.restriction s) x)) = (free_comm_ring.lift (λ (ix : t), f ix.val.fst k _ ix.val.snd)) ((free_comm_ring.restriction t) x)

theorem ring.direct_limit.of.zero_exact_aux {ι : Type v} [directed_order ι] {G : ι → Type w} [Π (i : ι), comm_ring (G i)] {f : Π (i j : ι), i jG iG j} [∀ (i j : ι) (hij : i j), is_ring_hom (f i j hij)] [directed_system G f] [nonempty ι] {x : free_comm_ring (Σ (i : ι), G i)} :
(ideal.quotient.mk (ideal.span {a : free_comm_ring (Σ (i : ι), G i) | (∃ (i j : ι) (H : i j) (x : G i), free_comm_ring.of j, f i j H x - free_comm_ring.of i, x⟩ = a) (∃ (i : ι), free_comm_ring.of i, 1⟩ - 1 = a) (∃ (i : ι) (x y : G i), free_comm_ring.of i, x + y - (free_comm_ring.of i, x⟩ + free_comm_ring.of i, y⟩) = a) ∃ (i : ι) (x y : G i), free_comm_ring.of i, x * y - (free_comm_ring.of i, x⟩) * free_comm_ring.of i, y⟩ = a})) x = 0(∃ (j : ι) (s : set (Σ (i : ι), G i)) (H : ∀ (k : Σ (i : ι), G i), k sk.fst j), x.is_supported s (free_comm_ring.lift (λ (ix : s), f ix.val.fst j _ ix.val.snd)) ((free_comm_ring.restriction s) x) = 0)

theorem ring.direct_limit.of.zero_exact {ι : Type v} [directed_order ι] {G : ι → Type w} [Π (i : ι), comm_ring (G i)] {f : Π (i j : ι), i jG iG j} [∀ (i j : ι) (hij : i j), is_ring_hom (f i j hij)] [directed_system G f] {i : ι} {x : G i} :
ring.direct_limit.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.

theorem ring.direct_limit.of_injective {ι : Type v} [directed_order ι] {G : ι → Type w} [Π (i : ι), comm_ring (G i)] {f : Π (i j : ι), i jG iG j} [∀ (i j : ι) (hij : i j), is_ring_hom (f i j hij)] [directed_system G f] (hf : ∀ (i j : ι) (hij : i j), function.injective (f i j hij)) (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.direct_limit.lift_hom {ι : Type v} [directed_order ι] (G : ι → Type w) [Π (i : ι), comm_ring (G i)] (f : Π (i j : ι), i jG iG j) (P : Type u₁) [comm_ring P] (g : Π (i : ι), G i → P) [∀ (i : ι), is_ring_hom (g i)] :
(∀ (i j : ι) (hij : i j) (x : G i), g j (f i j hij x) = g i x)ring.direct_limit G f →+* P

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.

We don't use this function as the canonical form because Lean 3 fails to automatically coerce it to a function; use lift instead.

Equations
def ring.direct_limit.lift {ι : Type v} [directed_order ι] (G : ι → Type w) [Π (i : ι), comm_ring (G i)] (f : Π (i j : ι), i jG iG j) (P : Type u₁) [comm_ring P] (g : Π (i : ι), G i → P) [∀ (i : ι), is_ring_hom (g i)] :
(∀ (i j : ι) (hij : i j) (x : G i), g j (f i j hij x) = g i x)ring.direct_limit G f → P

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
@[instance]
def ring.direct_limit.lift_is_ring_hom {ι : Type v} [directed_order ι] (G : ι → Type w) [Π (i : ι), comm_ring (G i)] (f : Π (i j : ι), i jG iG j) (P : Type u₁) [comm_ring P] (g : Π (i : ι), G i → P) [∀ (i : ι), is_ring_hom (g i)] (Hg : ∀ (i j : ι) (hij : i j) (x : G i), g j (f i j hij x) = g i x) :

@[simp]
theorem ring.direct_limit.lift_of {ι : Type v} [directed_order ι] {G : ι → Type w} [Π (i : ι), comm_ring (G i)] {f : Π (i j : ι), i jG iG j} (P : Type u₁) [comm_ring P] (g : Π (i : ι), G i → P) [∀ (i : ι), is_ring_hom (g i)] (Hg : ∀ (i j : ι) (hij : i j) (x : G i), g j (f i j hij x) = g i x) (i : ι) (x : G i) :
ring.direct_limit.lift G f P g Hg (ring.direct_limit.of G f i x) = g i x

@[simp]
theorem ring.direct_limit.lift_zero {ι : Type v} [directed_order ι] {G : ι → Type w} [Π (i : ι), comm_ring (G i)] {f : Π (i j : ι), i jG iG j} (P : Type u₁) [comm_ring P] (g : Π (i : ι), G i → P) [∀ (i : ι), is_ring_hom (g i)] (Hg : ∀ (i j : ι) (hij : i j) (x : G i), g j (f i j hij x) = g i x) :
ring.direct_limit.lift G f P g Hg 0 = 0

@[simp]
theorem ring.direct_limit.lift_one {ι : Type v} [directed_order ι] {G : ι → Type w} [Π (i : ι), comm_ring (G i)] {f : Π (i j : ι), i jG iG j} (P : Type u₁) [comm_ring P] (g : Π (i : ι), G i → P) [∀ (i : ι), is_ring_hom (g i)] (Hg : ∀ (i j : ι) (hij : i j) (x : G i), g j (f i j hij x) = g i x) :
ring.direct_limit.lift G f P g Hg 1 = 1

@[simp]
theorem ring.direct_limit.lift_add {ι : Type v} [directed_order ι] {G : ι → Type w} [Π (i : ι), comm_ring (G i)] {f : Π (i j : ι), i jG iG j} (P : Type u₁) [comm_ring P] (g : Π (i : ι), G i → P) [∀ (i : ι), is_ring_hom (g i)] (Hg : ∀ (i j : ι) (hij : i j) (x : G i), g j (f i j hij x) = g i x) (x y : ring.direct_limit G f) :
ring.direct_limit.lift G f P g Hg (x + y) = ring.direct_limit.lift G f P g Hg x + ring.direct_limit.lift G f P g Hg y

@[simp]
theorem ring.direct_limit.lift_neg {ι : Type v} [directed_order ι] {G : ι → Type w} [Π (i : ι), comm_ring (G i)] {f : Π (i j : ι), i jG iG j} (P : Type u₁) [comm_ring P] (g : Π (i : ι), G i → P) [∀ (i : ι), is_ring_hom (g i)] (Hg : ∀ (i j : ι) (hij : i j) (x : G i), g j (f i j hij x) = g i x) (x : ring.direct_limit G f) :

@[simp]
theorem ring.direct_limit.lift_sub {ι : Type v} [directed_order ι] {G : ι → Type w} [Π (i : ι), comm_ring (G i)] {f : Π (i j : ι), i jG iG j} (P : Type u₁) [comm_ring P] (g : Π (i : ι), G i → P) [∀ (i : ι), is_ring_hom (g i)] (Hg : ∀ (i j : ι) (hij : i j) (x : G i), g j (f i j hij x) = g i x) (x y : ring.direct_limit G f) :
ring.direct_limit.lift G f P g Hg (x - y) = ring.direct_limit.lift G f P g Hg x - ring.direct_limit.lift G f P g Hg y

@[simp]
theorem ring.direct_limit.lift_mul {ι : Type v} [directed_order ι] {G : ι → Type w} [Π (i : ι), comm_ring (G i)] {f : Π (i j : ι), i jG iG j} (P : Type u₁) [comm_ring P] (g : Π (i : ι), G i → P) [∀ (i : ι), is_ring_hom (g i)] (Hg : ∀ (i j : ι) (hij : i j) (x : G i), g j (f i j hij x) = g i x) (x y : ring.direct_limit G f) :
ring.direct_limit.lift G f P g Hg (x * y) = (ring.direct_limit.lift G f P g Hg x) * ring.direct_limit.lift G f P g Hg y

@[simp]
theorem ring.direct_limit.lift_pow {ι : Type v} [directed_order ι] {G : ι → Type w} [Π (i : ι), comm_ring (G i)] {f : Π (i j : ι), i jG iG j} (P : Type u₁) [comm_ring P] (g : Π (i : ι), G i → P) [∀ (i : ι), is_ring_hom (g i)] (Hg : ∀ (i j : ι) (hij : i j) (x : G i), g j (f i j hij x) = g i x) (x : ring.direct_limit G f) (n : ) :
ring.direct_limit.lift G f P g Hg (x ^ n) = ring.direct_limit.lift G f P g Hg x ^ n

theorem ring.direct_limit.lift_unique {ι : Type v} [directed_order ι] {G : ι → Type w} [Π (i : ι), comm_ring (G i)] {f : Π (i j : ι), i jG iG j} (P : Type u₁) [comm_ring P] [nonempty ι] (F : ring.direct_limit G f → P) [is_ring_hom F] (x : ring.direct_limit G f) :
F x = ring.direct_limit.lift G f P (λ (i : ι) (x : G i), F (ring.direct_limit.of G f i x)) _ x

@[instance]
def field.direct_limit.nontrivial {ι : Type v} [directed_order ι] (G : ι → Type w) [nonempty ι] [Π (i : ι), field (G i)] (f : Π (i j : ι), i jG iG j) [∀ (i j : ι) (hij : i j), is_ring_hom (f i j hij)] [directed_system G f] :

theorem field.direct_limit.exists_inv {ι : Type v} [directed_order ι] (G : ι → Type w) [nonempty ι] [Π (i : ι), field (G i)] (f : Π (i j : ι), i jG iG j) {p : ring.direct_limit G f} :
p 0(∃ (y : ring.direct_limit G f), p * y = 1)

def field.direct_limit.inv {ι : Type v} [directed_order ι] (G : ι → Type w) [nonempty ι] [Π (i : ι), field (G i)] (f : Π (i j : ι), i jG iG j) :

Noncomputable multiplicative inverse in a direct limit of fields.

Equations
theorem field.direct_limit.mul_inv_cancel {ι : Type v} [directed_order ι] (G : ι → Type w) [nonempty ι] [Π (i : ι), field (G i)] (f : Π (i j : ι), i jG iG j) {p : ring.direct_limit G f} :
p 0p * field.direct_limit.inv G f p = 1

theorem field.direct_limit.inv_mul_cancel {ι : Type v} [directed_order ι] (G : ι → Type w) [nonempty ι] [Π (i : ι), field (G i)] (f : Π (i j : ι), i jG iG j) {p : ring.direct_limit G f} :
p 0(field.direct_limit.inv G f p) * p = 1

def field.direct_limit.field {ι : Type v} [directed_order ι] (G : ι → Type w) [nonempty ι] [Π (i : ι), field (G i)] (f : Π (i j : ι), i jG iG j) [∀ (i j : ι) (hij : i j), is_ring_hom (f i j hij)] [directed_system G f] :

Noncomputable field structure on the direct limit of fields.

Equations