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} [LinearOrderedField α] {β : Type u_2} [Ring β] (abv : β → α) [IsAbsoluteValue abv] : Type u_2

The Cauchy completion of a ring with absolute value.

Equations

• CauSeq.Completion.Cauchy abv = Quotient CauSeq.equiv

def CauSeq.Completion.mk {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : β → α} [IsAbsoluteValue abv] : CauSeq β abv → CauSeq.Completion.Cauchy abv

The map from Cauchy sequences into the Cauchy completion.

Equations

• CauSeq.Completion.mk = Quotient.mk''

@[simp]

theorem CauSeq.Completion.mk_eq_mk {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : β → α} [IsAbsoluteValue abv] (f : CauSeq β abv) : ⟦f⟧ = CauSeq.Completion.mk f

theorem CauSeq.Completion.mk_eq {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : β → α} [IsAbsoluteValue abv] {f g : CauSeq β abv} : CauSeq.Completion.mk f = CauSeq.Completion.mk g ↔ f ≈ g

def CauSeq.Completion.ofRat {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : β → α} [IsAbsoluteValue abv] (x : β) : CauSeq.Completion.Cauchy abv

The map from the original ring into the Cauchy completion.

Equations

• CauSeq.Completion.ofRat x = CauSeq.Completion.mk (CauSeq.const abv x)

instance CauSeq.Completion.instZeroCauchy {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : β → α} [IsAbsoluteValue abv] : Zero (CauSeq.Completion.Cauchy abv)

Equations

• CauSeq.Completion.instZeroCauchy = { zero := CauSeq.Completion.ofRat 0 }

instance CauSeq.Completion.instOneCauchy {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : β → α} [IsAbsoluteValue abv] : One (CauSeq.Completion.Cauchy abv)

Equations

• CauSeq.Completion.instOneCauchy = { one := CauSeq.Completion.ofRat 1 }

instance CauSeq.Completion.instInhabitedCauchy {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : β → α} [IsAbsoluteValue abv] : Inhabited (CauSeq.Completion.Cauchy abv)

Equations

• CauSeq.Completion.instInhabitedCauchy = { default := 0 }

theorem CauSeq.Completion.ofRat_zero {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : β → α} [IsAbsoluteValue abv] : CauSeq.Completion.ofRat 0 = 0

theorem CauSeq.Completion.ofRat_one {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : β → α} [IsAbsoluteValue abv] : CauSeq.Completion.ofRat 1 = 1

@[simp]

theorem CauSeq.Completion.mk_eq_zero {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : β → α} [IsAbsoluteValue abv] {f : CauSeq β abv} : CauSeq.Completion.mk f = 0 ↔ f.LimZero

instance CauSeq.Completion.instAddCauchy {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : β → α} [IsAbsoluteValue abv] : Add (CauSeq.Completion.Cauchy abv)

Equations

• CauSeq.Completion.instAddCauchy = { add := Quotient.map₂ (fun (x1 x2 : CauSeq β abv) => x1 + x2) ⋯ }

@[simp]

theorem CauSeq.Completion.mk_add {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : β → α} [IsAbsoluteValue abv] (f g : CauSeq β abv) : CauSeq.Completion.mk f + CauSeq.Completion.mk g = CauSeq.Completion.mk (f + g)

instance CauSeq.Completion.instNegCauchy {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : β → α} [IsAbsoluteValue abv] : Neg (CauSeq.Completion.Cauchy abv)

Equations

• CauSeq.Completion.instNegCauchy = { neg := Quotient.map Neg.neg ⋯ }

@[simp]

theorem CauSeq.Completion.mk_neg {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : β → α} [IsAbsoluteValue abv] (f : CauSeq β abv) : -CauSeq.Completion.mk f = CauSeq.Completion.mk (-f)

instance CauSeq.Completion.instMulCauchy {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : β → α} [IsAbsoluteValue abv] : Mul (CauSeq.Completion.Cauchy abv)

Equations

• CauSeq.Completion.instMulCauchy = { mul := Quotient.map₂ (fun (x1 x2 : CauSeq β abv) => x1 * x2) ⋯ }

@[simp]

theorem CauSeq.Completion.mk_mul {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : β → α} [IsAbsoluteValue abv] (f g : CauSeq β abv) : CauSeq.Completion.mk f * CauSeq.Completion.mk g = CauSeq.Completion.mk (f * g)

instance CauSeq.Completion.instSubCauchy {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : β → α} [IsAbsoluteValue abv] : Sub (CauSeq.Completion.Cauchy abv)

Equations

• CauSeq.Completion.instSubCauchy = { sub := Quotient.map₂ Sub.sub ⋯ }

@[simp]

theorem CauSeq.Completion.mk_sub {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : β → α} [IsAbsoluteValue abv] (f g : CauSeq β abv) : CauSeq.Completion.mk f - CauSeq.Completion.mk g = CauSeq.Completion.mk (f - g)

instance CauSeq.Completion.instSMulCauchyOfIsScalarTower {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : β → α} [IsAbsoluteValue abv] {γ : Type u_3} [SMul γ β] [IsScalarTower γ β β] : SMul γ (CauSeq.Completion.Cauchy abv)

Equations

• CauSeq.Completion.instSMulCauchyOfIsScalarTower = { smul := fun (c : γ) => Quotient.map (fun (x : CauSeq β abv) => c • x) ⋯ }

@[simp]

theorem CauSeq.Completion.mk_smul {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : β → α} [IsAbsoluteValue abv] {γ : Type u_3} [SMul γ β] [IsScalarTower γ β β] (c : γ) (f : CauSeq β abv) : c • CauSeq.Completion.mk f = CauSeq.Completion.mk (c • f)

instance CauSeq.Completion.instPowCauchyNat {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : β → α} [IsAbsoluteValue abv] : Pow (CauSeq.Completion.Cauchy abv) ℕ

Equations

• CauSeq.Completion.instPowCauchyNat = { pow := fun (x : CauSeq.Completion.Cauchy abv) (n : ℕ) => Quotient.map (fun (x : CauSeq β abv) => x ^ n) ⋯ x }

@[simp]

theorem CauSeq.Completion.mk_pow {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : β → α} [IsAbsoluteValue abv] (n : ℕ) (f : CauSeq β abv) : CauSeq.Completion.mk f ^ n = CauSeq.Completion.mk (f ^ n)

instance CauSeq.Completion.instNatCastCauchy {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : β → α} [IsAbsoluteValue abv] : NatCast (CauSeq.Completion.Cauchy abv)

Equations

• CauSeq.Completion.instNatCastCauchy = { natCast := fun (n : ℕ) => CauSeq.Completion.mk ↑n }

instance CauSeq.Completion.instIntCastCauchy {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : β → α} [IsAbsoluteValue abv] : IntCast (CauSeq.Completion.Cauchy abv)

Equations

• CauSeq.Completion.instIntCastCauchy = { intCast := fun (n : ℤ) => CauSeq.Completion.mk ↑n }

@[simp]

theorem CauSeq.Completion.ofRat_natCast {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : β → α} [IsAbsoluteValue abv] (n : ℕ) : CauSeq.Completion.ofRat ↑n = ↑n

@[simp]

theorem CauSeq.Completion.ofRat_intCast {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : β → α} [IsAbsoluteValue abv] (z : ℤ) : CauSeq.Completion.ofRat ↑z = ↑z

theorem CauSeq.Completion.ofRat_add {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : β → α} [IsAbsoluteValue abv] (x y : β) : CauSeq.Completion.ofRat (x + y) = CauSeq.Completion.ofRat x + CauSeq.Completion.ofRat y

theorem CauSeq.Completion.ofRat_neg {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : β → α} [IsAbsoluteValue abv] (x : β) : CauSeq.Completion.ofRat (-x) = -CauSeq.Completion.ofRat x

theorem CauSeq.Completion.ofRat_mul {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : β → α} [IsAbsoluteValue abv] (x y : β) : CauSeq.Completion.ofRat (x * y) = CauSeq.Completion.ofRat x * CauSeq.Completion.ofRat y

instance CauSeq.Completion.Cauchy.ring {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : β → α} [IsAbsoluteValue abv] : Ring (CauSeq.Completion.Cauchy abv)

Equations

• CauSeq.Completion.Cauchy.ring = Function.Surjective.ring CauSeq.Completion.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

def CauSeq.Completion.ofRatRingHom {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : β → α} [IsAbsoluteValue abv] : β →+* CauSeq.Completion.Cauchy abv

CauSeq.Completion.ofRat as a RingHom

Equations

• CauSeq.Completion.ofRatRingHom = { toFun := CauSeq.Completion.ofRat, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem CauSeq.Completion.ofRatRingHom_apply {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : β → α} [IsAbsoluteValue abv] (x : β) : CauSeq.Completion.ofRatRingHom x = CauSeq.Completion.ofRat x

theorem CauSeq.Completion.ofRat_sub {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : β → α} [IsAbsoluteValue abv] (x y : β) : CauSeq.Completion.ofRat (x - y) = CauSeq.Completion.ofRat x - CauSeq.Completion.ofRat y

instance CauSeq.Completion.Cauchy.commRing {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [CommRing β] {abv : β → α} [IsAbsoluteValue abv] : CommRing (CauSeq.Completion.Cauchy abv)

Equations

• CauSeq.Completion.Cauchy.commRing = Function.Surjective.commRing CauSeq.Completion.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance CauSeq.Completion.instNNRatCast {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [DivisionRing β] {abv : β → α} [IsAbsoluteValue abv] : NNRatCast (CauSeq.Completion.Cauchy abv)

Equations

• CauSeq.Completion.instNNRatCast = { nnratCast := fun (q : ℚ≥0) => CauSeq.Completion.ofRat ↑q }

instance CauSeq.Completion.instRatCast {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [DivisionRing β] {abv : β → α} [IsAbsoluteValue abv] : RatCast (CauSeq.Completion.Cauchy abv)

Equations

• CauSeq.Completion.instRatCast = { ratCast := fun (q : ℚ) => CauSeq.Completion.ofRat ↑q }

@[simp]

theorem CauSeq.Completion.ofRat_nnratCast {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [DivisionRing β] {abv : β → α} [IsAbsoluteValue abv] (q : ℚ≥0) : CauSeq.Completion.ofRat ↑q = ↑q

@[simp]

theorem CauSeq.Completion.ofRat_ratCast {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [DivisionRing β] {abv : β → α} [IsAbsoluteValue abv] (q : ℚ) : CauSeq.Completion.ofRat ↑q = ↑q

noncomputable instance CauSeq.Completion.instInvCauchy {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [DivisionRing β] {abv : β → α} [IsAbsoluteValue abv] : Inv (CauSeq.Completion.Cauchy abv)

Equations

• One or more equations did not get rendered due to their size.

theorem CauSeq.Completion.inv_zero {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [DivisionRing β] {abv : β → α} [IsAbsoluteValue abv] : 0⁻¹ = 0

@[simp]

theorem CauSeq.Completion.inv_mk {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [DivisionRing β] {abv : β → α} [IsAbsoluteValue abv] {f : CauSeq β abv} (hf : ¬f.LimZero) : (CauSeq.Completion.mk f)⁻¹ = CauSeq.Completion.mk (f.inv hf)

theorem CauSeq.Completion.cau_seq_zero_ne_one {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [DivisionRing β] {abv : β → α} [IsAbsoluteValue abv] : ¬0 ≈ 1

theorem CauSeq.Completion.zero_ne_one {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [DivisionRing β] {abv : β → α} [IsAbsoluteValue abv] : 0 ≠ 1

theorem CauSeq.Completion.inv_mul_cancel {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [DivisionRing β] {abv : β → α} [IsAbsoluteValue abv] {x : CauSeq.Completion.Cauchy abv} : x ≠ 0 → x⁻¹ * x = 1

theorem CauSeq.Completion.mul_inv_cancel {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [DivisionRing β] {abv : β → α} [IsAbsoluteValue abv] {x : CauSeq.Completion.Cauchy abv} : x ≠ 0 → x * x⁻¹ = 1

theorem CauSeq.Completion.ofRat_inv {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [DivisionRing β] {abv : β → α} [IsAbsoluteValue abv] (x : β) : CauSeq.Completion.ofRat x⁻¹ = (CauSeq.Completion.ofRat x)⁻¹

noncomputable instance CauSeq.Completion.instDivInvMonoid {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [DivisionRing β] {abv : β → α} [IsAbsoluteValue abv] : DivInvMonoid (CauSeq.Completion.Cauchy abv)

Equations

• CauSeq.Completion.instDivInvMonoid = DivInvMonoid.mk ⋯ zpowRec ⋯ ⋯ ⋯

theorem CauSeq.Completion.ofRat_div {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [DivisionRing β] {abv : β → α} [IsAbsoluteValue abv] (x y : β) : CauSeq.Completion.ofRat (x / y) = CauSeq.Completion.ofRat x / CauSeq.Completion.ofRat y

noncomputable instance CauSeq.Completion.Cauchy.divisionRing {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [DivisionRing β] {abv : β → α} [IsAbsoluteValue abv] : DivisionRing (CauSeq.Completion.Cauchy 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} [LinearOrderedField α] {β : Type u_2} [DivisionRing β] {abv : β → α} [IsAbsoluteValue abv] [Repr β] : Repr (CauSeq.Completion.Cauchy abv)

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.

noncomputable instance CauSeq.Completion.Cauchy.field {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Field β] {abv : β → α} [IsAbsoluteValue abv] : Field (CauSeq.Completion.Cauchy abv)

The Cauchy completion forms a field.

Equations

• CauSeq.Completion.Cauchy.field = Field.mk ⋯ DivisionRing.zpow ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ DivisionRing.nnqsmul ⋯ ⋯ DivisionRing.qsmul ⋯

class CauSeq.IsComplete {α : Type u_1} [LinearOrderedField α] (β : Type u_2) [Ring β] (abv : β → α) [IsAbsoluteValue abv] : Prop

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.

theorem CauSeq.complete {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : β → α} [IsAbsoluteValue abv] [CauSeq.IsComplete β abv] (s : CauSeq β abv) : ∃ (b : β), s ≈ CauSeq.const abv b

noncomputable def CauSeq.lim {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : β → α} [IsAbsoluteValue abv] [CauSeq.IsComplete β abv] (s : CauSeq β abv) : β

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

Equations

• s.lim = Classical.choose ⋯

theorem CauSeq.equiv_lim {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : β → α} [IsAbsoluteValue abv] [CauSeq.IsComplete β abv] (s : CauSeq β abv) : s ≈ CauSeq.const abv s.lim

theorem CauSeq.eq_lim_of_const_equiv {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : β → α} [IsAbsoluteValue abv] [CauSeq.IsComplete β abv] {f : CauSeq β abv} {x : β} (h : CauSeq.const abv x ≈ f) : x = f.lim

theorem CauSeq.lim_eq_of_equiv_const {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : β → α} [IsAbsoluteValue abv] [CauSeq.IsComplete β abv] {f : CauSeq β abv} {x : β} (h : f ≈ CauSeq.const abv x) : f.lim = x

theorem CauSeq.lim_eq_lim_of_equiv {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : β → α} [IsAbsoluteValue abv] [CauSeq.IsComplete β abv] {f g : CauSeq β abv} (h : f ≈ g) : f.lim = g.lim

@[simp]

theorem CauSeq.lim_const {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : β → α} [IsAbsoluteValue abv] [CauSeq.IsComplete β abv] (x : β) : (CauSeq.const abv x).lim = x

theorem CauSeq.lim_add {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : β → α} [IsAbsoluteValue abv] [CauSeq.IsComplete β abv] (f g : CauSeq β abv) : f.lim + g.lim = (f + g).lim

theorem CauSeq.lim_mul_lim {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : β → α} [IsAbsoluteValue abv] [CauSeq.IsComplete β abv] (f g : CauSeq β abv) : f.lim * g.lim = (f * g).lim

theorem CauSeq.lim_mul {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : β → α} [IsAbsoluteValue abv] [CauSeq.IsComplete β abv] (f : CauSeq β abv) (x : β) : f.lim * x = (f * CauSeq.const abv x).lim

theorem CauSeq.lim_neg {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : β → α} [IsAbsoluteValue abv] [CauSeq.IsComplete β abv] (f : CauSeq β abv) : (-f).lim = -f.lim

theorem CauSeq.lim_eq_zero_iff {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : β → α} [IsAbsoluteValue abv] [CauSeq.IsComplete β abv] (f : CauSeq β abv) : f.lim = 0 ↔ f.LimZero

theorem CauSeq.lim_inv {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Field β] {abv : β → α} [IsAbsoluteValue abv] [CauSeq.IsComplete β abv] {f : CauSeq β abv} (hf : ¬f.LimZero) : (f.inv hf).lim = f.lim⁻¹

theorem CauSeq.lim_le {α : Type u_1} [LinearOrderedField α] [CauSeq.IsComplete α abs] {f : CauSeq α abs} {x : α} (h : f ≤ CauSeq.const abs x) : f.lim ≤ x

theorem CauSeq.le_lim {α : Type u_1} [LinearOrderedField α] [CauSeq.IsComplete α abs] {f : CauSeq α abs} {x : α} (h : CauSeq.const abs x ≤ f) : x ≤ f.lim

theorem CauSeq.lt_lim {α : Type u_1} [LinearOrderedField α] [CauSeq.IsComplete α abs] {f : CauSeq α abs} {x : α} (h : CauSeq.const abs x < f) : x < f.lim

theorem CauSeq.lim_lt {α : Type u_1} [LinearOrderedField α] [CauSeq.IsComplete α abs] {f : CauSeq α abs} {x : α} (h : f < CauSeq.const abs x) : f.lim < x