# Cauchy completion #

This file generalizes the Cauchy completion of (ℚ, abs) to the completion of a ring with absolute value.

def CauSeq.Completion.Cauchy {α : Type u_1} {β : Type u_2} [Ring β] (abv : βα) [] :
Type u_2

The Cauchy completion of a ring with absolute value.

Equations
Instances For
def CauSeq.Completion.mk {α : Type u_1} {β : Type u_2} [Ring β] {abv : βα} [] :
CauSeq β abv

The map from Cauchy sequences into the Cauchy completion.

Equations
• CauSeq.Completion.mk = Quotient.mk''
Instances For
@[simp]
theorem CauSeq.Completion.mk_eq_mk {α : Type u_1} {β : Type u_2} [Ring β] {abv : βα} [] (f : CauSeq β abv) :
theorem CauSeq.Completion.mk_eq {α : Type u_1} {β : Type u_2} [Ring β] {abv : βα} [] {f : CauSeq β abv} {g : CauSeq β abv} :
def CauSeq.Completion.ofRat {α : Type u_1} {β : Type u_2} [Ring β] {abv : βα} [] (x : β) :

The map from the original ring into the Cauchy completion.

Equations
Instances For
instance CauSeq.Completion.instZeroCauchy {α : Type u_1} {β : Type u_2} [Ring β] {abv : βα} [] :
Equations
• CauSeq.Completion.instZeroCauchy = { zero := }
instance CauSeq.Completion.instOneCauchy {α : Type u_1} {β : Type u_2} [Ring β] {abv : βα} [] :
Equations
• CauSeq.Completion.instOneCauchy = { one := }
instance CauSeq.Completion.instInhabitedCauchy {α : Type u_1} {β : Type u_2} [Ring β] {abv : βα} [] :
Equations
• CauSeq.Completion.instInhabitedCauchy = { default := 0 }
theorem CauSeq.Completion.ofRat_zero {α : Type u_1} {β : Type u_2} [Ring β] {abv : βα} [] :
theorem CauSeq.Completion.ofRat_one {α : Type u_1} {β : Type u_2} [Ring β] {abv : βα} [] :
@[simp]
theorem CauSeq.Completion.mk_eq_zero {α : Type u_1} {β : Type u_2} [Ring β] {abv : βα} [] {f : CauSeq β abv} :
f.LimZero
instance CauSeq.Completion.instAddCauchy {α : Type u_1} {β : Type u_2} [Ring β] {abv : βα} [] :
Equations
@[simp]
theorem CauSeq.Completion.mk_add {α : Type u_1} {β : Type u_2} [Ring β] {abv : βα} [] (f : CauSeq β abv) (g : CauSeq β abv) :
instance CauSeq.Completion.instNegCauchy {α : Type u_1} {β : Type u_2} [Ring β] {abv : βα} [] :
Equations
• CauSeq.Completion.instNegCauchy = { neg := Quotient.map Neg.neg }
@[simp]
theorem CauSeq.Completion.mk_neg {α : Type u_1} {β : Type u_2} [Ring β] {abv : βα} [] (f : CauSeq β abv) :
instance CauSeq.Completion.instMulCauchy {α : Type u_1} {β : Type u_2} [Ring β] {abv : βα} [] :
Equations
@[simp]
theorem CauSeq.Completion.mk_mul {α : Type u_1} {β : Type u_2} [Ring β] {abv : βα} [] (f : CauSeq β abv) (g : CauSeq β abv) :
instance CauSeq.Completion.instSubCauchy {α : Type u_1} {β : Type u_2} [Ring β] {abv : βα} [] :
Equations
@[simp]
theorem CauSeq.Completion.mk_sub {α : Type u_1} {β : Type u_2} [Ring β] {abv : βα} [] (f : CauSeq β abv) (g : CauSeq β abv) :
instance CauSeq.Completion.instSMulCauchyOfIsScalarTower {α : Type u_1} {β : Type u_2} [Ring β] {abv : βα} [] {γ : Type u_3} [SMul γ β] [] :
SMul γ ()
Equations
• CauSeq.Completion.instSMulCauchyOfIsScalarTower = { smul := fun (c : γ) => Quotient.map (fun (x : CauSeq β abv) => c x) }
@[simp]
theorem CauSeq.Completion.mk_smul {α : Type u_1} {β : Type u_2} [Ring β] {abv : βα} [] {γ : Type u_3} [SMul γ β] [] (c : γ) (f : CauSeq β abv) :
instance CauSeq.Completion.instPowCauchyNat {α : Type u_1} {β : Type u_2} [Ring β] {abv : βα} [] :
Equations
• CauSeq.Completion.instPowCauchyNat = { pow := fun (x : ) (n : ) => Quotient.map (fun (x : CauSeq β abv) => x ^ n) x }
@[simp]
theorem CauSeq.Completion.mk_pow {α : Type u_1} {β : Type u_2} [Ring β] {abv : βα} [] (n : ) (f : CauSeq β abv) :
instance CauSeq.Completion.instNatCastCauchy {α : Type u_1} {β : Type u_2} [Ring β] {abv : βα} [] :
Equations
• CauSeq.Completion.instNatCastCauchy = { natCast := fun (n : ) => }
instance CauSeq.Completion.instIntCastCauchy {α : Type u_1} {β : Type u_2} [Ring β] {abv : βα} [] :
Equations
• CauSeq.Completion.instIntCastCauchy = { intCast := fun (n : ) => }
@[simp]
theorem CauSeq.Completion.ofRat_natCast {α : Type u_1} {β : Type u_2} [Ring β] {abv : βα} [] (n : ) :
@[simp]
theorem CauSeq.Completion.ofRat_intCast {α : Type u_1} {β : Type u_2} [Ring β] {abv : βα} [] (z : ) :
theorem CauSeq.Completion.ofRat_add {α : Type u_1} {β : Type u_2} [Ring β] {abv : βα} [] (x : β) (y : β) :
theorem CauSeq.Completion.ofRat_neg {α : Type u_1} {β : Type u_2} [Ring β] {abv : βα} [] (x : β) :
theorem CauSeq.Completion.ofRat_mul {α : Type u_1} {β : Type u_2} [Ring β] {abv : βα} [] (x : β) (y : β) :
instance CauSeq.Completion.Cauchy.ring {α : Type u_1} {β : Type u_2} [Ring β] {abv : βα} [] :
Equations
• CauSeq.Completion.Cauchy.ring = Function.Surjective.ring CauSeq.Completion.mk
@[simp]
theorem CauSeq.Completion.ofRatRingHom_apply {α : Type u_1} {β : Type u_2} [Ring β] {abv : βα} [] (x : β) :
CauSeq.Completion.ofRatRingHom x =
def CauSeq.Completion.ofRatRingHom {α : Type u_1} {β : Type u_2} [Ring β] {abv : βα} [] :

CauSeq.Completion.ofRat as a RingHom

Equations
• CauSeq.Completion.ofRatRingHom = { toFun := CauSeq.Completion.ofRat, map_one' := , map_mul' := , map_zero' := , map_add' := }
Instances For
theorem CauSeq.Completion.ofRat_sub {α : Type u_1} {β : Type u_2} [Ring β] {abv : βα} [] (x : β) (y : β) :
instance CauSeq.Completion.Cauchy.commRing {α : Type u_1} {β : Type u_2} [] {abv : βα} [] :
Equations
instance CauSeq.Completion.instNNRatCast {α : Type u_1} {β : Type u_2} [] {abv : βα} [] :
Equations
• CauSeq.Completion.instNNRatCast = { nnratCast := fun (q : ℚ≥0) => }
instance CauSeq.Completion.instRatCast {α : Type u_1} {β : Type u_2} [] {abv : βα} [] :
Equations
• CauSeq.Completion.instRatCast = { ratCast := fun (q : ) => }
@[simp]
theorem CauSeq.Completion.ofRat_nnratCast {α : Type u_1} {β : Type u_2} [] {abv : βα} [] (q : ℚ≥0) :
@[simp]
theorem CauSeq.Completion.ofRat_ratCast {α : Type u_1} {β : Type u_2} [] {abv : βα} [] (q : ) :
noncomputable instance CauSeq.Completion.instInvCauchy {α : Type u_1} {β : Type u_2} [] {abv : βα} [] :
Equations
• One or more equations did not get rendered due to their size.
theorem CauSeq.Completion.inv_zero {α : Type u_1} {β : Type u_2} [] {abv : βα} [] :
0⁻¹ = 0
@[simp]
theorem CauSeq.Completion.inv_mk {α : Type u_1} {β : Type u_2} [] {abv : βα} [] {f : CauSeq β abv} (hf : ¬f.LimZero) :
theorem CauSeq.Completion.cau_seq_zero_ne_one {α : Type u_1} {β : Type u_2} [] {abv : βα} [] :
¬0 1
theorem CauSeq.Completion.zero_ne_one {α : Type u_1} {β : Type u_2} [] {abv : βα} [] :
0 1
theorem CauSeq.Completion.inv_mul_cancel {α : Type u_1} {β : Type u_2} [] {abv : βα} [] {x : } :
x 0x⁻¹ * x = 1
theorem CauSeq.Completion.mul_inv_cancel {α : Type u_1} {β : Type u_2} [] {abv : βα} [] {x : } :
x 0x * x⁻¹ = 1
theorem CauSeq.Completion.ofRat_inv {α : Type u_1} {β : Type u_2} [] {abv : βα} [] (x : β) :
noncomputable instance CauSeq.Completion.instDivInvMonoid {α : Type u_1} {β : Type u_2} [] {abv : βα} [] :
Equations
theorem CauSeq.Completion.ofRat_div {α : Type u_1} {β : Type u_2} [] {abv : βα} [] (x : β) (y : β) :
noncomputable instance CauSeq.Completion.Cauchy.divisionRing {α : Type u_1} {β : Type u_2} [] {abv : βα} [] :

The Cauchy completion forms a division ring.

Equations
• One or more equations did not get rendered due to their size.
unsafe instance CauSeq.Completion.instReprCauchy {α : Type u_1} {β : Type u_2} [] {abv : βα} [] [Repr β] :

Show the first 10 items of a representative of this equivalence class of cauchy sequences.

The representative chosen is the one passed in the VM to Quot.mk, so two cauchy sequences converging to the same number may be printed differently.

Equations
• One or more equations did not get rendered due to their size.
noncomputable instance CauSeq.Completion.Cauchy.field {α : Type u_1} {β : Type u_2} [] {abv : βα} [] :

The Cauchy completion forms a field.

Equations
• One or more equations did not get rendered due to their size.
class CauSeq.IsComplete {α : Type u_1} (β : Type u_2) [Ring β] (abv : βα) [] :

A class stating that a ring with an absolute value is complete, i.e. every Cauchy sequence has a limit.

• isComplete : ∀ (s : CauSeq β abv), ∃ (b : β), s CauSeq.const abv b

Every Cauchy sequence has a limit.

Instances
theorem CauSeq.IsComplete.isComplete {α : Type u_1} {β : Type u_2} [Ring β] {abv : βα} [] [self : ] (s : CauSeq β abv) :
∃ (b : β), s CauSeq.const abv b

Every Cauchy sequence has a limit.

theorem CauSeq.complete {α : Type u_1} {β : Type u_2} [Ring β] {abv : βα} [] [] (s : CauSeq β abv) :
∃ (b : β), s CauSeq.const abv b
noncomputable def CauSeq.lim {α : Type u_1} {β : Type u_2} [Ring β] {abv : βα} [] [] (s : CauSeq β abv) :
β

The limit of a Cauchy sequence in a complete ring. Chosen non-computably.

Equations
• s.lim =
Instances For
theorem CauSeq.equiv_lim {α : Type u_1} {β : Type u_2} [Ring β] {abv : βα} [] [] (s : CauSeq β abv) :
s CauSeq.const abv s.lim
theorem CauSeq.eq_lim_of_const_equiv {α : Type u_1} {β : Type u_2} [Ring β] {abv : βα} [] [] {f : CauSeq β abv} {x : β} (h : CauSeq.const abv x f) :
x = f.lim
theorem CauSeq.lim_eq_of_equiv_const {α : Type u_1} {β : Type u_2} [Ring β] {abv : βα} [] [] {f : CauSeq β abv} {x : β} (h : f CauSeq.const abv x) :
f.lim = x
theorem CauSeq.lim_eq_lim_of_equiv {α : Type u_1} {β : Type u_2} [Ring β] {abv : βα} [] [] {f : CauSeq β abv} {g : CauSeq β abv} (h : f g) :
f.lim = g.lim
@[simp]
theorem CauSeq.lim_const {α : Type u_1} {β : Type u_2} [Ring β] {abv : βα} [] [] (x : β) :
(CauSeq.const abv x).lim = x
theorem CauSeq.lim_add {α : Type u_1} {β : Type u_2} [Ring β] {abv : βα} [] [] (f : CauSeq β abv) (g : CauSeq β abv) :
f.lim + g.lim = (f + g).lim
theorem CauSeq.lim_mul_lim {α : Type u_1} {β : Type u_2} [Ring β] {abv : βα} [] [] (f : CauSeq β abv) (g : CauSeq β abv) :
f.lim * g.lim = (f * g).lim
theorem CauSeq.lim_mul {α : Type u_1} {β : Type u_2} [Ring β] {abv : βα} [] [] (f : CauSeq β abv) (x : β) :
f.lim * x = (f * CauSeq.const abv x).lim
theorem CauSeq.lim_neg {α : Type u_1} {β : Type u_2} [Ring β] {abv : βα} [] [] (f : CauSeq β abv) :
(-f).lim = -f.lim
theorem CauSeq.lim_eq_zero_iff {α : Type u_1} {β : Type u_2} [Ring β] {abv : βα} [] [] (f : CauSeq β abv) :
f.lim = 0 f.LimZero
theorem CauSeq.lim_inv {α : Type u_1} {β : Type u_2} [] {abv : βα} [] [] {f : CauSeq β abv} (hf : ¬f.LimZero) :
(f.inv hf).lim = f.lim⁻¹
theorem CauSeq.lim_le {α : Type u_1} [] {f : CauSeq α abs} {x : α} (h : f CauSeq.const abs x) :
f.lim x
theorem CauSeq.le_lim {α : Type u_1} [] {f : CauSeq α abs} {x : α} (h : CauSeq.const abs x f) :
x f.lim
theorem CauSeq.lt_lim {α : Type u_1} [] {f : CauSeq α abs} {x : α} (h : CauSeq.const abs x < f) :
x < f.lim
theorem CauSeq.lim_lt {α : Type u_1} [] {f : CauSeq α abs} {x : α} (h : f < CauSeq.const abs x) :
f.lim < x