Documentation

Mathlib.Algebra.Order.CauSeq.Completion

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
Instances For
    def CauSeq.Completion.mk {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : βα} [IsAbsoluteValue 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} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : βα} [IsAbsoluteValue abv] (f : CauSeq β abv) :
      theorem CauSeq.Completion.mk_eq {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : βα} [IsAbsoluteValue abv] {f : CauSeq β abv} {g : CauSeq β abv} :
      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
      Instances For
        instance CauSeq.Completion.instZeroCauchy {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : βα} [IsAbsoluteValue abv] :
        Equations
        instance CauSeq.Completion.instOneCauchy {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : βα} [IsAbsoluteValue abv] :
        Equations
        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] :
        Equations
        @[simp]
        theorem CauSeq.Completion.mk_add {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : βα} [IsAbsoluteValue abv] (f : CauSeq β abv) (g : CauSeq β abv) :
        instance CauSeq.Completion.instNegCauchy {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : βα} [IsAbsoluteValue 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] :
        Equations
        @[simp]
        theorem CauSeq.Completion.mk_mul {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : βα} [IsAbsoluteValue abv] (f : CauSeq β abv) (g : CauSeq β abv) :
        instance CauSeq.Completion.instSubCauchy {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : βα} [IsAbsoluteValue abv] :
        Equations
        @[simp]
        theorem CauSeq.Completion.mk_sub {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : βα} [IsAbsoluteValue abv] (f : CauSeq β abv) (g : CauSeq β abv) :
        instance CauSeq.Completion.instSMulCauchyOfIsScalarTower {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : βα} [IsAbsoluteValue abv] {γ : Type u_3} [SMul γ β] [IsScalarTower γ β β] :
        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) :
        instance CauSeq.Completion.instPowCauchyNat {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : βα} [IsAbsoluteValue abv] :
        Equations
        @[simp]
        theorem CauSeq.Completion.mk_pow {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : βα} [IsAbsoluteValue abv] (n : ) (f : CauSeq β abv) :
        instance CauSeq.Completion.instNatCastCauchy {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : βα} [IsAbsoluteValue abv] :
        Equations
        instance CauSeq.Completion.instIntCastCauchy {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : βα} [IsAbsoluteValue abv] :
        Equations
        @[simp]
        theorem CauSeq.Completion.ofRat_natCast {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : βα} [IsAbsoluteValue abv] (n : ) :
        @[simp]
        theorem CauSeq.Completion.ofRat_intCast {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : βα} [IsAbsoluteValue abv] (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] :
        Equations
        • CauSeq.Completion.Cauchy.ring = Function.Surjective.ring CauSeq.Completion.mk
        @[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
        def CauSeq.Completion.ofRatRingHom {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [Ring β] {abv : βα} [IsAbsoluteValue 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} [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
          instance CauSeq.Completion.instNNRatCast {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [DivisionRing β] {abv : βα} [IsAbsoluteValue abv] :
          Equations
          instance CauSeq.Completion.instRatCast {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [DivisionRing β] {abv : βα} [IsAbsoluteValue abv] :
          Equations
          @[simp]
          theorem CauSeq.Completion.ofRat_nnratCast {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [DivisionRing β] {abv : βα} [IsAbsoluteValue abv] (q : ℚ≥0) :
          @[simp]
          theorem CauSeq.Completion.ofRat_ratCast {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [DivisionRing β] {abv : βα} [IsAbsoluteValue abv] (q : ) :
          noncomputable instance CauSeq.Completion.instInvCauchy {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [DivisionRing β] {abv : βα} [IsAbsoluteValue 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) :
          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 0x⁻¹ * 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 0x * x⁻¹ = 1
          noncomputable instance CauSeq.Completion.instDivInvMonoid {α : Type u_1} [LinearOrderedField α] {β : Type u_2} [DivisionRing β] {abv : βα} [IsAbsoluteValue abv] :
          Equations
          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 β] :

          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.

          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] :

          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} :
            ∀ {inst : LinearOrderedField α} {β : Type u_2} {inst_1 : Ring β} {abv : βα} {inst_2 : IsAbsoluteValue abv} [self : CauSeq.IsComplete β abv] (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
            Instances For
              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 : CauSeq β abv} {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 : CauSeq β abv) (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 : CauSeq β abv) (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