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 : β)
:
The map from the original ring into the Cauchy completion.
Equations
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]
:
Equations
- CauSeq.Completion.instInhabitedCauchy = { default := 0 }
theorem
CauSeq.Completion.ofRat_zero
{α : Type u_1}
[LinearOrderedField α]
{β : Type u_2}
[Ring β]
{abv : β → α}
[IsAbsoluteValue abv]
:
theorem
CauSeq.Completion.ofRat_one
{α : Type u_1}
[LinearOrderedField α]
{β : Type u_2}
[Ring β]
{abv : β → α}
[IsAbsoluteValue abv]
:
@[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)
:
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)
:
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)
:
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)
:
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]
:
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]
:
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 : β)
:
theorem
CauSeq.Completion.ofRat_neg
{α : Type u_1}
[LinearOrderedField α]
{β : Type u_2}
[Ring β]
{abv : β → α}
[IsAbsoluteValue abv]
(x : β)
:
theorem
CauSeq.Completion.ofRat_mul
{α : Type u_1}
[LinearOrderedField α]
{β : Type u_2}
[Ring β]
{abv : β → α}
[IsAbsoluteValue abv]
(x 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 : β)
:
instance
CauSeq.Completion.Cauchy.commRing
{α : Type u_1}
[LinearOrderedField α]
{β : Type u_2}
[CommRing β]
{abv : β → α}
[IsAbsoluteValue 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]
:
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]
:
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]
:
@[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]
:
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}
:
theorem
CauSeq.Completion.mul_inv_cancel
{α : Type u_1}
[LinearOrderedField α]
{β : Type u_2}
[DivisionRing β]
{abv : β → α}
[IsAbsoluteValue abv]
{x : CauSeq.Completion.Cauchy abv}
:
theorem
CauSeq.Completion.ofRat_inv
{α : Type u_1}
[LinearOrderedField α]
{β : Type u_2}
[DivisionRing β]
{abv : β → α}
[IsAbsoluteValue abv]
(x : β)
:
noncomputable instance
CauSeq.Completion.instDivInvMonoid
{α : Type u_1}
[LinearOrderedField α]
{β : Type u_2}
[DivisionRing β]
{abv : β → α}
[IsAbsoluteValue 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 : β)
:
noncomputable instance
CauSeq.Completion.Cauchy.divisionRing
{α : Type u_1}
[LinearOrderedField α]
{β : Type u_2}
[DivisionRing β]
{abv : β → α}
[IsAbsoluteValue 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]
:
The Cauchy completion forms a field.
class
CauSeq.IsComplete
{α : Type u_1}
[LinearOrderedField α]
(β : Type u_2)
[Ring β]
(abv : β → α)
[IsAbsoluteValue 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.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)
:
theorem
CauSeq.lim_mul_lim
{α : Type u_1}
[LinearOrderedField α]
{β : Type u_2}
[Ring β]
{abv : β → α}
[IsAbsoluteValue abv]
[CauSeq.IsComplete β abv]
(f g : CauSeq β abv)
:
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)
:
theorem
CauSeq.lim_eq_zero_iff
{α : Type u_1}
[LinearOrderedField α]
{β : Type u_2}
[Ring β]
{abv : β → α}
[IsAbsoluteValue abv]
[CauSeq.IsComplete β abv]
(f : CauSeq β abv)
:
theorem
CauSeq.lim_inv
{α : Type u_1}
[LinearOrderedField α]
{β : Type u_2}
[Field β]
{abv : β → α}
[IsAbsoluteValue abv]
[CauSeq.IsComplete β abv]
{f : CauSeq β abv}
(hf : ¬f.LimZero)
:
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