Cauchy completion #
This file generalizes the Cauchy completion of (ℚ, abs)
to the completion of a ring
with absolute value.
The Cauchy completion of a ring with absolute value.
Equations
- CauSeq.Completion.Cauchy abv = Quotient CauSeq.equiv
Instances For
The map from Cauchy sequences into the Cauchy completion.
Equations
- CauSeq.Completion.mk = Quotient.mk''
Instances For
The map from the original ring into the Cauchy completion.
Equations
Instances For
Equations
- CauSeq.Completion.instZeroCauchy = { zero := CauSeq.Completion.ofRat 0 }
Equations
- CauSeq.Completion.instOneCauchy = { one := CauSeq.Completion.ofRat 1 }
Equations
- CauSeq.Completion.instInhabitedCauchy = { default := 0 }
Equations
- CauSeq.Completion.instAddCauchy = { add := Quotient.map₂ (fun (x x_1 : CauSeq β abv) => x + x_1) ⋯ }
Equations
- CauSeq.Completion.instNegCauchy = { neg := Quotient.map Neg.neg ⋯ }
Equations
- CauSeq.Completion.instMulCauchy = { mul := Quotient.map₂ (fun (x x_1 : CauSeq β abv) => x * x_1) ⋯ }
Equations
- CauSeq.Completion.instSubCauchy = { sub := Quotient.map₂ Sub.sub ⋯ }
Equations
- CauSeq.Completion.instSMulCauchyOfIsScalarTower = { smul := fun (c : γ) => Quotient.map (fun (x : CauSeq β abv) => c • x) ⋯ }
Equations
- CauSeq.Completion.instPowCauchyNat = { pow := fun (x : CauSeq.Completion.Cauchy abv) (n : ℕ) => Quotient.map (fun (x : CauSeq β abv) => x ^ n) ⋯ x }
Equations
- CauSeq.Completion.instNatCastCauchy = { natCast := fun (n : ℕ) => CauSeq.Completion.mk ↑n }
Equations
- CauSeq.Completion.instIntCastCauchy = { intCast := fun (n : ℤ) => CauSeq.Completion.mk ↑n }
Equations
- CauSeq.Completion.Cauchy.ring = Function.Surjective.ring CauSeq.Completion.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
CauSeq.Completion.ofRat
as a RingHom
Equations
- CauSeq.Completion.ofRatRingHom = { toFun := CauSeq.Completion.ofRat, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
Instances For
Equations
- CauSeq.Completion.Cauchy.commRing = Function.Surjective.commRing CauSeq.Completion.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- CauSeq.Completion.instNNRatCast = { nnratCast := fun (q : ℚ≥0) => CauSeq.Completion.ofRat ↑q }
Equations
- CauSeq.Completion.instRatCast = { ratCast := fun (q : ℚ) => CauSeq.Completion.ofRat ↑q }
Equations
- One or more equations did not get rendered due to their size.
Equations
- CauSeq.Completion.instDivInvMonoid = DivInvMonoid.mk ⋯ zpowRec ⋯ ⋯ ⋯
The Cauchy completion forms a division ring.
Equations
- One or more equations did not get rendered due to their size.
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.
The Cauchy completion forms a field.
Equations
- One or more equations did not get rendered due to their size.
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
Every Cauchy sequence has a limit.
The limit of a Cauchy sequence in a complete ring. Chosen non-computably.
Equations
- s.lim = Classical.choose ⋯