Cauchy completion #
This file generalizes the Cauchy completion of (ℚ, abs) to the completion of a commutative ring
with absolute value.
def
cau_seq.completion.Cauchy
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[comm_ring β]
{abv : β → α}
[is_absolute_value abv] :
Type u_2
The Cauchy completion of a commutative ring with absolute value.
Equations
def
cau_seq.completion.mk
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[comm_ring β]
{abv : β → α}
[is_absolute_value abv] :
cau_seq β abv → cau_seq.completion.Cauchy
The map from Cauchy sequences into the Cauchy completion.
Equations
@[simp]
theorem
cau_seq.completion.mk_eq_mk
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[comm_ring β]
{abv : β → α}
[is_absolute_value abv]
(f : cau_seq β abv) :
theorem
cau_seq.completion.mk_eq
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[comm_ring β]
{abv : β → α}
[is_absolute_value abv]
{f g : cau_seq β abv} :
cau_seq.completion.mk f = cau_seq.completion.mk g ↔ f ≈ g
def
cau_seq.completion.of_rat
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[comm_ring β]
{abv : β → α}
[is_absolute_value abv]
(x : β) :
The map from the original ring into the Cauchy completion.
Equations
@[protected, instance]
def
cau_seq.completion.Cauchy.has_zero
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[comm_ring β]
{abv : β → α}
[is_absolute_value abv] :
Equations
@[protected, instance]
def
cau_seq.completion.Cauchy.has_one
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[comm_ring β]
{abv : β → α}
[is_absolute_value abv] :
Equations
@[protected, instance]
def
cau_seq.completion.Cauchy.inhabited
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[comm_ring β]
{abv : β → α}
[is_absolute_value abv] :
Equations
theorem
cau_seq.completion.of_rat_zero
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[comm_ring β]
{abv : β → α}
[is_absolute_value abv] :
theorem
cau_seq.completion.of_rat_one
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[comm_ring β]
{abv : β → α}
[is_absolute_value abv] :
@[simp]
theorem
cau_seq.completion.mk_eq_zero
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[comm_ring β]
{abv : β → α}
[is_absolute_value abv]
{f : cau_seq β abv} :
cau_seq.completion.mk f = 0 ↔ f.lim_zero
@[protected, instance]
def
cau_seq.completion.Cauchy.has_add
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[comm_ring β]
{abv : β → α}
[is_absolute_value abv] :
Equations
- cau_seq.completion.Cauchy.has_add = {add := λ (x y : cau_seq.completion.Cauchy), quotient.lift_on₂ x y (λ (f g : cau_seq β abv), cau_seq.completion.mk (f + g)) cau_seq.completion.Cauchy.has_add._proof_1}
@[simp]
theorem
cau_seq.completion.mk_add
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[comm_ring β]
{abv : β → α}
[is_absolute_value abv]
(f g : cau_seq β abv) :
@[protected, instance]
def
cau_seq.completion.Cauchy.has_neg
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[comm_ring β]
{abv : β → α}
[is_absolute_value abv] :
Equations
- cau_seq.completion.Cauchy.has_neg = {neg := λ (x : cau_seq.completion.Cauchy), quotient.lift_on x (λ (f : cau_seq β abv), cau_seq.completion.mk (-f)) cau_seq.completion.Cauchy.has_neg._proof_1}
@[simp]
theorem
cau_seq.completion.mk_neg
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[comm_ring β]
{abv : β → α}
[is_absolute_value abv]
(f : cau_seq β abv) :
@[protected, instance]
def
cau_seq.completion.Cauchy.has_mul
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[comm_ring β]
{abv : β → α}
[is_absolute_value abv] :
Equations
- cau_seq.completion.Cauchy.has_mul = {mul := λ (x y : cau_seq.completion.Cauchy), quotient.lift_on₂ x y (λ (f g : cau_seq β abv), cau_seq.completion.mk (f * g)) cau_seq.completion.Cauchy.has_mul._proof_1}
@[simp]
theorem
cau_seq.completion.mk_mul
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[comm_ring β]
{abv : β → α}
[is_absolute_value abv]
(f g : cau_seq β abv) :
(cau_seq.completion.mk f) * cau_seq.completion.mk g = cau_seq.completion.mk (f * g)
@[protected, instance]
def
cau_seq.completion.Cauchy.has_sub
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[comm_ring β]
{abv : β → α}
[is_absolute_value abv] :
Equations
- cau_seq.completion.Cauchy.has_sub = {sub := λ (x y : cau_seq.completion.Cauchy), quotient.lift_on₂ x y (λ (f g : cau_seq β abv), cau_seq.completion.mk (f - g)) cau_seq.completion.Cauchy.has_sub._proof_1}
@[simp]
theorem
cau_seq.completion.mk_sub
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[comm_ring β]
{abv : β → α}
[is_absolute_value abv]
(f g : cau_seq β abv) :
theorem
cau_seq.completion.of_rat_add
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[comm_ring β]
{abv : β → α}
[is_absolute_value abv]
(x y : β) :
theorem
cau_seq.completion.of_rat_neg
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[comm_ring β]
{abv : β → α}
[is_absolute_value abv]
(x : β) :
theorem
cau_seq.completion.of_rat_mul
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[comm_ring β]
{abv : β → α}
[is_absolute_value abv]
(x y : β) :
@[protected, instance]
def
cau_seq.completion.Cauchy.comm_ring
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[comm_ring β]
{abv : β → α}
[is_absolute_value abv] :
Equations
- cau_seq.completion.Cauchy.comm_ring = {add := has_add.add cau_seq.completion.Cauchy.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := nsmul_rec cau_seq.completion.Cauchy.has_add, nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg cau_seq.completion.Cauchy.has_neg, sub := has_sub.sub cau_seq.completion.Cauchy.has_sub, sub_eq_add_neg := _, zsmul := zsmul_rec cau_seq.completion.Cauchy.has_neg, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := has_mul.mul cau_seq.completion.Cauchy.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := npow_rec cau_seq.completion.Cauchy.has_mul, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _}
theorem
cau_seq.completion.of_rat_sub
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[comm_ring β]
{abv : β → α}
[is_absolute_value abv]
(x y : β) :
@[protected, instance]
noncomputable
def
cau_seq.completion.Cauchy.has_inv
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[field β]
{abv : β → α}
[is_absolute_value abv] :
Equations
- cau_seq.completion.Cauchy.has_inv = {inv := λ (x : cau_seq.completion.Cauchy), quotient.lift_on x (λ (f : cau_seq β abv), cau_seq.completion.mk (dite f.lim_zero (λ (h : f.lim_zero), 0) (λ (h : ¬f.lim_zero), f.inv h))) cau_seq.completion.Cauchy.has_inv._proof_1}
@[simp]
theorem
cau_seq.completion.inv_zero
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[field β]
{abv : β → α}
[is_absolute_value abv] :
@[simp]
theorem
cau_seq.completion.inv_mk
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[field β]
{abv : β → α}
[is_absolute_value abv]
{f : cau_seq β abv}
(hf : ¬f.lim_zero) :
(cau_seq.completion.mk f)⁻¹ = cau_seq.completion.mk (f.inv hf)
theorem
cau_seq.completion.cau_seq_zero_ne_one
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[field β]
{abv : β → α}
[is_absolute_value abv] :
theorem
cau_seq.completion.zero_ne_one
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[field β]
{abv : β → α}
[is_absolute_value abv] :
0 ≠ 1
@[protected]
theorem
cau_seq.completion.inv_mul_cancel
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[field β]
{abv : β → α}
[is_absolute_value abv]
{x : cau_seq.completion.Cauchy} :
noncomputable
def
cau_seq.completion.field
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[field β]
{abv : β → α}
[is_absolute_value abv] :
The Cauchy completion forms a field. See note [reducible non-instances].
Equations
- cau_seq.completion.field = {add := comm_ring.add cau_seq.completion.Cauchy.comm_ring, add_assoc := _, zero := comm_ring.zero cau_seq.completion.Cauchy.comm_ring, zero_add := _, add_zero := _, nsmul := comm_ring.nsmul cau_seq.completion.Cauchy.comm_ring, nsmul_zero' := _, nsmul_succ' := _, neg := comm_ring.neg cau_seq.completion.Cauchy.comm_ring, sub := comm_ring.sub cau_seq.completion.Cauchy.comm_ring, sub_eq_add_neg := _, zsmul := comm_ring.zsmul cau_seq.completion.Cauchy.comm_ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := comm_ring.mul cau_seq.completion.Cauchy.comm_ring, mul_assoc := _, one := comm_ring.one cau_seq.completion.Cauchy.comm_ring, one_mul := _, mul_one := _, npow := comm_ring.npow cau_seq.completion.Cauchy.comm_ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _, inv := has_inv.inv cau_seq.completion.Cauchy.has_inv, div := div_inv_monoid.div._default comm_ring.mul cau_seq.completion.field._proof_20 comm_ring.one cau_seq.completion.field._proof_21 cau_seq.completion.field._proof_22 comm_ring.npow cau_seq.completion.field._proof_23 cau_seq.completion.field._proof_24 has_inv.inv, div_eq_mul_inv := _, zpow := div_inv_monoid.zpow._default comm_ring.mul cau_seq.completion.field._proof_26 comm_ring.one cau_seq.completion.field._proof_27 cau_seq.completion.field._proof_28 comm_ring.npow cau_seq.completion.field._proof_29 cau_seq.completion.field._proof_30 has_inv.inv, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, mul_inv_cancel := _, inv_zero := _}
theorem
cau_seq.completion.of_rat_inv
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[field β]
{abv : β → α}
[is_absolute_value abv]
(x : β) :
theorem
cau_seq.completion.of_rat_div
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[field β]
{abv : β → α}
[is_absolute_value abv]
(x y : β) :
@[class]
structure
cau_seq.is_complete
{α : Type u_1}
[linear_ordered_field α]
(β : Type u_2)
[ring β]
(abv : β → α)
[is_absolute_value abv] :
Prop
- is_complete : ∀ (s : cau_seq β abv), ∃ (b : β), s ≈ cau_seq.const abv b
A class stating that a ring with an absolute value is complete, i.e. every Cauchy sequence has a limit.
theorem
cau_seq.complete
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
[cau_seq.is_complete β abv]
(s : cau_seq β abv) :
∃ (b : β), s ≈ cau_seq.const abv b
noncomputable
def
cau_seq.lim
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
[cau_seq.is_complete β abv]
(s : cau_seq β abv) :
β
The limit of a Cauchy sequence in a complete ring. Chosen non-computably.
Equations
- s.lim = classical.some _
theorem
cau_seq.equiv_lim
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
[cau_seq.is_complete β abv]
(s : cau_seq β abv) :
s ≈ cau_seq.const abv s.lim
theorem
cau_seq.eq_lim_of_const_equiv
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
[cau_seq.is_complete β abv]
{f : cau_seq β abv}
{x : β}
(h : cau_seq.const abv x ≈ f) :
theorem
cau_seq.lim_eq_of_equiv_const
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
[cau_seq.is_complete β abv]
{f : cau_seq β abv}
{x : β}
(h : f ≈ cau_seq.const abv x) :
theorem
cau_seq.lim_eq_lim_of_equiv
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
[cau_seq.is_complete β abv]
{f g : cau_seq β abv}
(h : f ≈ g) :
@[simp]
theorem
cau_seq.lim_const
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
[cau_seq.is_complete β abv]
(x : β) :
(cau_seq.const abv x).lim = x
theorem
cau_seq.lim_add
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
[cau_seq.is_complete β abv]
(f g : cau_seq β abv) :
theorem
cau_seq.lim_mul_lim
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
[cau_seq.is_complete β abv]
(f g : cau_seq β abv) :
theorem
cau_seq.lim_mul
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
[cau_seq.is_complete β abv]
(f : cau_seq β abv)
(x : β) :
theorem
cau_seq.lim_neg
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
[cau_seq.is_complete β abv]
(f : cau_seq β abv) :
theorem
cau_seq.lim_eq_zero_iff
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
[cau_seq.is_complete β abv]
(f : cau_seq β abv) :
theorem
cau_seq.lim_inv
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[field β]
{abv : β → α}
[is_absolute_value abv]
[cau_seq.is_complete β abv]
{f : cau_seq β abv}
(hf : ¬f.lim_zero) :
theorem
cau_seq.lim_le
{α : Type u_1}
[linear_ordered_field α]
[cau_seq.is_complete α abs]
{f : cau_seq α abs}
{x : α}
(h : f ≤ cau_seq.const abs x) :
theorem
cau_seq.le_lim
{α : Type u_1}
[linear_ordered_field α]
[cau_seq.is_complete α abs]
{f : cau_seq α abs}
{x : α}
(h : cau_seq.const abs x ≤ f) :
theorem
cau_seq.lt_lim
{α : Type u_1}
[linear_ordered_field α]
[cau_seq.is_complete α abs]
{f : cau_seq α abs}
{x : α}
(h : cau_seq.const abs x < f) :
theorem
cau_seq.lim_lt
{α : Type u_1}
[linear_ordered_field α]
[cau_seq.is_complete α abs]
{f : cau_seq α abs}
{x : α}
(h : f < cau_seq.const abs x) :