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

Main definitions #

@[class]
structure directed_system {ι : Type v} [preorder ι] (G : ι → Type w) (f : Π (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 a category (directed poset) to another category.

Instances
theorem module.directed_system.map_self {R : Type u} [ring R] {ι : Type v} [preorder ι] {G : ι → Type w} [Π (i : ι), add_comm_group (G i)] [Π (i : ι), module R (G i)] (f : Π (i j : ι), i j(G i →ₗ[R] G j)) [directed_system G (λ (i j : ι) (h : i j), (f i j h))] (i : ι) (x : G i) (h : i i) :
(f i i h) x = x

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

theorem module.directed_system.map_map {R : Type u} [ring R] {ι : Type v} [preorder ι] {G : ι → Type w} [Π (i : ι), add_comm_group (G i)] [Π (i : ι), module R (G i)] (f : Π (i j : ι), i j(G i →ₗ[R] G j)) [directed_system G (λ (i j : ι) (h : i j), (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 _) x

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

def module.direct_limit {R : Type u} [ring R] {ι : Type v} [dec_ι : decidable_eq ι] [preorder ι] (G : ι → Type w) [Π (i : ι), add_comm_group (G i)] [Π (i : ι), module R (G i)] (f : Π (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
@[protected, instance]
def module.direct_limit.add_comm_group {R : Type u} [ring R] {ι : Type v} [dec_ι : decidable_eq ι] [preorder ι] (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
@[protected, instance]
def module.direct_limit.module {R : Type u} [ring R] {ι : Type v} [dec_ι : decidable_eq ι] [preorder ι] (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
@[protected, instance]
def module.direct_limit.inhabited {R : Type u} [ring R] {ι : Type v} [dec_ι : decidable_eq ι] [preorder ι] (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 ι] [preorder ι] (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 ι] [preorder ι] {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 ι] [preorder ι] {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 ι] [is_directed ι has_le.le] (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.

@[protected]
theorem module.direct_limit.induction_on {R : Type u} [ring R] {ι : Type v} [dec_ι : decidable_eq ι] [preorder ι] {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 ι] [is_directed ι has_le.le] {C : module.direct_limit G f → Prop} (z : module.direct_limit G f) (ih : ∀ (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 ι] [preorder ι] (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) :

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 ι] [preorder ι] {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 ι] [preorder ι] {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 ι] [is_directed ι has_le.le] (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
noncomputable def module.direct_limit.totalize {R : Type u} [ring R] {ι : Type v} [preorder ι] (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_of_le {R : Type u} [ring R] {ι : Type v} [preorder ι] {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 : ι} (h : i j) :
theorem module.direct_limit.totalize_of_not_le {R : Type u} [ring R] {ι : Type v} [preorder ι] {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 : ι} (h : ¬i j) :
theorem module.direct_limit.to_module_totalize_of_le {R : Type u} [ring R] {ι : Type v} [dec_ι : decidable_eq ι] [preorder ι] {G : ι → Type w} [Π (i : ι), add_comm_group (G i)] [Π (i : ι), module R (G i)] {f : Π (i j : ι), i j(G i →ₗ[R] G j)} [directed_system G (λ (i j : ι) (h : i j), (f i j h))] {x : direct_sum ι G} {i j : ι} (hij : i j) (hx : ∀ (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 ι] [preorder ι] {G : ι → Type w} [Π (i : ι), add_comm_group (G i)] [Π (i : ι), module R (G i)] {f : Π (i j : ι), i j(G i →ₗ[R] G j)} [directed_system G (λ (i j : ι) (h : i j), (f i j h))] [nonempty ι] [is_directed ι has_le.le] {x : direct_sum ι G} (H : 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 ι] [preorder ι] {G : ι → Type w} [Π (i : ι), add_comm_group (G i)] [Π (i : ι), module R (G i)] {f : Π (i j : ι), i j(G i →ₗ[R] G j)} [directed_system G (λ (i j : ι) (h : i j), (f i j h))] [is_directed ι has_le.le] {i : ι} {x : G i} (H : (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 ι] [preorder ι] (G : ι → Type w) [Π (i : ι), add_comm_group (G i)] (f : Π (i j : ι), i jG i →+ G j) :
Type (max v w)

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

Equations
@[protected]
theorem add_comm_group.direct_limit.directed_system {ι : Type v} [preorder ι] (G : ι → Type w) [Π (i : ι), add_comm_group (G i)] (f : Π (i j : ι), i jG i →+ G j) [h : directed_system G (λ (i j : ι) (h : i j), (f i j h))] :
directed_system G (λ (i j : ι) (hij : i j), ((f i j hij).to_int_linear_map))
@[protected, instance]
def add_comm_group.direct_limit.add_comm_group {ι : Type v} [dec_ι : decidable_eq ι] [preorder ι] (G : ι → Type w) [Π (i : ι), add_comm_group (G i)] (f : Π (i j : ι), i jG i →+ G j) :
Equations
@[protected, instance]
def add_comm_group.direct_limit.inhabited {ι : Type v} [dec_ι : decidable_eq ι] [preorder ι] (G : ι → Type w) [Π (i : ι), add_comm_group (G i)] (f : Π (i j : ι), i jG i →+ G j) :
Equations
def add_comm_group.direct_limit.of {ι : Type v} [dec_ι : decidable_eq ι] [preorder ι] (G : ι → Type w) [Π (i : ι), add_comm_group (G i)] (f : Π (i j : ι), i jG i →+ G j) (i : ι) :

The canonical map from a component to the direct limit.

Equations
@[simp]
theorem add_comm_group.direct_limit.of_f {ι : Type v} [dec_ι : decidable_eq ι] [preorder ι] {G : ι → Type w} [Π (i : ι), add_comm_group (G i)] {f : Π (i j : ι), i jG i →+ G j} {i j : ι} (hij : i j) (x : G i) :
@[protected]
theorem add_comm_group.direct_limit.induction_on {ι : Type v} [dec_ι : decidable_eq ι] [preorder ι] {G : ι → Type w} [Π (i : ι), add_comm_group (G i)] {f : Π (i j : ι), i jG i →+ G j} [nonempty ι] [is_directed ι has_le.le] {C : add_comm_group.direct_limit G f → Prop} (z : add_comm_group.direct_limit G f) (ih : ∀ (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 ι] [preorder ι] {G : ι → Type w} [Π (i : ι), add_comm_group (G i)] {f : Π (i j : ι), i jG i →+ G j} [is_directed ι has_le.le] [directed_system G (λ (i j : ι) (h : i j), (f i j h))] (i : ι) (x : G i) (h : (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 ι] [preorder ι] (G : ι → Type w) [Π (i : ι), add_comm_group (G i)] (f : Π (i j : ι), i jG i →+ G j) (P : Type u₁) [add_comm_group 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
@[simp]
theorem add_comm_group.direct_limit.lift_of {ι : Type v} [dec_ι : decidable_eq ι] [preorder ι] {G : ι → Type w} [Π (i : ι), add_comm_group (G i)] {f : Π (i j : ι), i jG i →+ G j} (P : Type u₁) [add_comm_group 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 add_comm_group.direct_limit.lift_unique {ι : Type v} [dec_ι : decidable_eq ι] [preorder ι] {G : ι → Type w} [Π (i : ι), add_comm_group (G i)] {f : Π (i j : ι), i jG i →+ G j} (P : Type u₁) [add_comm_group P] [nonempty ι] [is_directed ι has_le.le] (F : add_comm_group.direct_limit G f →+ P) (x : add_comm_group.direct_limit G f) :
def ring.direct_limit {ι : Type v} [preorder ι] (G : ι → Type w) [Π (i : ι), comm_ring (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
@[protected, instance]
def ring.direct_limit.comm_ring {ι : Type v} [preorder ι] (G : ι → Type w) [Π (i : ι), comm_ring (G i)] (f : Π (i j : ι), i jG iG j) :
Equations
@[protected, instance]
def ring.direct_limit.ring {ι : Type v} [preorder ι] (G : ι → Type w) [Π (i : ι), comm_ring (G i)] (f : Π (i j : ι), i jG iG j) :
Equations
@[protected, instance]
def ring.direct_limit.inhabited {ι : Type v} [preorder ι] (G : ι → Type w) [Π (i : ι), comm_ring (G i)] (f : Π (i j : ι), i jG iG j) :
Equations
def ring.direct_limit.of {ι : Type v} [preorder ι] (G : ι → Type w) [Π (i : ι), comm_ring (G i)] (f : Π (i j : ι), i jG iG j) (i : ι) :

The canonical map from a component to the direct limit.

Equations
@[simp]
theorem ring.direct_limit.of_f {ι : Type v} [preorder ι] {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
theorem ring.direct_limit.exists_of {ι : Type v} [preorder ι] {G : ι → Type w} [Π (i : ι), comm_ring (G i)] {f : Π (i j : ι), i jG iG j} [nonempty ι] [is_directed ι has_le.le] (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} [preorder ι] {G : ι → Type w} [Π (i : ι), comm_ring (G i)] {f' : Π (i j : ι), i jG i →+* G j} [nonempty ι] [is_directed ι has_le.le] (q : (ring.direct_limit G (λ (i j : ι) (h : i j), (f' i j h)))[X]) :
∃ (i : ι) (p : (G i)[X]), polynomial.map (ring.direct_limit.of G (λ (i j : ι) (h : i j), (f' i j h)) i) p = q
theorem ring.direct_limit.induction_on {ι : Type v} [preorder ι] {G : ι → Type w} [Π (i : ι), comm_ring (G i)] {f : Π (i j : ι), i jG iG j} [nonempty ι] [is_directed ι has_le.le] {C : ring.direct_limit G f → Prop} (z : ring.direct_limit G f) (ih : ∀ (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} [preorder ι] (G : ι → Type w) [Π (i : ι), comm_ring (G i)] (f' : Π (i j : ι), i jG i →+* G j) [directed_system G (λ (i j : ι) (h : i j), (f' i j h))] {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) (hst : s t) :
(f' 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} [preorder ι] {G : ι → Type w} [Π (i : ι), comm_ring (G i)] {f' : Π (i j : ι), i jG i →+* G j} [directed_system G (λ (i j : ι) (h : i j), (f' i j h))] [nonempty ι] [is_directed ι has_le.le] {x : free_comm_ring (Σ (i : ι), G i)} (H : (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, (λ (i j : ι) (h : i j), (f' i j h)) 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} [preorder ι] {G : ι → Type w} [Π (i : ι), comm_ring (G i)] {f' : Π (i j : ι), i jG i →+* G j} [directed_system G (λ (i j : ι) (h : i j), (f' i j h))] [is_directed ι has_le.le] {i : ι} {x : G i} (hix : (ring.direct_limit.of G (λ (i j : ι) (h : i j), (f' i j h)) 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} [preorder ι] {G : ι → Type w} [Π (i : ι), comm_ring (G i)] (f' : Π (i j : ι), i jG i →+* G j) [is_directed ι has_le.le] [directed_system G (λ (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.direct_limit.of G (λ (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.

def ring.direct_limit.lift {ι : Type v} [preorder ι] (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) (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
@[simp]
theorem ring.direct_limit.lift_of {ι : Type v} [preorder ι] {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) (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
theorem ring.direct_limit.lift_unique {ι : Type v} [preorder ι] {G : ι → Type w} [Π (i : ι), comm_ring (G i)] {f : Π (i j : ι), i jG iG j} (P : Type u₁) [comm_ring P] [nonempty ι] [is_directed ι has_le.le] (F : ring.direct_limit G f →+* P) (x : ring.direct_limit G f) :
F x = (ring.direct_limit.lift G f P (λ (i : ι), F.comp (ring.direct_limit.of G f i)) _) x
@[protected, instance]
def field.direct_limit.nontrivial {ι : Type v} [preorder ι] (G : ι → Type w) [nonempty ι] [is_directed ι has_le.le] [Π (i : ι), field (G i)] (f' : Π (i j : ι), i jG i →+* G j) [directed_system G (λ (i j : ι) (h : i j), (f' i j h))] :
nontrivial (ring.direct_limit G (λ (i j : ι) (h : i j), (f' i j h)))
theorem field.direct_limit.exists_inv {ι : Type v} [preorder ι] (G : ι → Type w) [nonempty ι] [is_directed ι has_le.le] [Π (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)
noncomputable def field.direct_limit.inv {ι : Type v} [preorder ι] (G : ι → Type w) [nonempty ι] [is_directed ι has_le.le] [Π (i : ι), field (G i)] (f : Π (i j : ι), i jG iG j) (p : ring.direct_limit G f) :

Noncomputable multiplicative inverse in a direct limit of fields.

Equations
@[protected]
theorem field.direct_limit.mul_inv_cancel {ι : Type v} [preorder ι] (G : ι → Type w) [nonempty ι] [is_directed ι has_le.le] [Π (i : ι), field (G i)] (f : Π (i j : ι), i jG iG j) {p : ring.direct_limit G f} (hp : p 0) :
@[protected]
theorem field.direct_limit.inv_mul_cancel {ι : Type v} [preorder ι] (G : ι → Type w) [nonempty ι] [is_directed ι has_le.le] [Π (i : ι), field (G i)] (f : Π (i j : ι), i jG iG j) {p : ring.direct_limit G f} (hp : p 0) :
@[protected]
noncomputable def field.direct_limit.field {ι : Type v} [preorder ι] (G : ι → Type w) [nonempty ι] [is_directed ι has_le.le] [Π (i : ι), field (G i)] (f' : Π (i j : ι), i jG i →+* G j) [directed_system G (λ (i j : ι) (h : i j), (f' i j h))] :
field (ring.direct_limit G (λ (i j : ι) (h : i j), (f' i j h)))

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

Equations