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} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : 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} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [Ring β] {abv : βα} [IsAbsoluteValue abv] :
      CauSeq β abvCauchy abv

      The map from Cauchy sequences into the Cauchy completion.

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

          The map from the original ring into the Cauchy completion.

          Equations
            Instances For
              instance CauSeq.Completion.instZeroCauchy {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [Ring β] {abv : βα} [IsAbsoluteValue abv] :
              Zero (Cauchy abv)
              Equations
                instance CauSeq.Completion.instOneCauchy {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [Ring β] {abv : βα} [IsAbsoluteValue abv] :
                One (Cauchy abv)
                Equations
                  instance CauSeq.Completion.instInhabitedCauchy {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [Ring β] {abv : βα} [IsAbsoluteValue abv] :
                  Equations
                    theorem CauSeq.Completion.ofRat_zero {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [Ring β] {abv : βα} [IsAbsoluteValue abv] :
                    ofRat 0 = 0
                    theorem CauSeq.Completion.ofRat_one {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [Ring β] {abv : βα} [IsAbsoluteValue abv] :
                    ofRat 1 = 1
                    @[simp]
                    theorem CauSeq.Completion.mk_eq_zero {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [Ring β] {abv : βα} [IsAbsoluteValue abv] {f : CauSeq β abv} :
                    mk f = 0 f.LimZero
                    instance CauSeq.Completion.instAddCauchy {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [Ring β] {abv : βα} [IsAbsoluteValue abv] :
                    Add (Cauchy abv)
                    Equations
                      @[simp]
                      theorem CauSeq.Completion.mk_add {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [Ring β] {abv : βα} [IsAbsoluteValue abv] (f g : CauSeq β abv) :
                      mk f + mk g = mk (f + g)
                      instance CauSeq.Completion.instNegCauchy {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [Ring β] {abv : βα} [IsAbsoluteValue abv] :
                      Neg (Cauchy abv)
                      Equations
                        @[simp]
                        theorem CauSeq.Completion.mk_neg {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [Ring β] {abv : βα} [IsAbsoluteValue abv] (f : CauSeq β abv) :
                        -mk f = mk (-f)
                        instance CauSeq.Completion.instMulCauchy {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [Ring β] {abv : βα} [IsAbsoluteValue abv] :
                        Mul (Cauchy abv)
                        Equations
                          @[simp]
                          theorem CauSeq.Completion.mk_mul {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [Ring β] {abv : βα} [IsAbsoluteValue abv] (f g : CauSeq β abv) :
                          mk f * mk g = mk (f * g)
                          instance CauSeq.Completion.instSubCauchy {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [Ring β] {abv : βα} [IsAbsoluteValue abv] :
                          Sub (Cauchy abv)
                          Equations
                            @[simp]
                            theorem CauSeq.Completion.mk_sub {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [Ring β] {abv : βα} [IsAbsoluteValue abv] (f g : CauSeq β abv) :
                            mk f - mk g = mk (f - g)
                            instance CauSeq.Completion.instSMulCauchyOfIsScalarTower {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [Ring β] {abv : βα} [IsAbsoluteValue abv] {γ : Type u_3} [SMul γ β] [IsScalarTower γ β β] :
                            SMul γ (Cauchy abv)
                            Equations
                              @[simp]
                              theorem CauSeq.Completion.mk_smul {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [Ring β] {abv : βα} [IsAbsoluteValue abv] {γ : Type u_3} [SMul γ β] [IsScalarTower γ β β] (c : γ) (f : CauSeq β abv) :
                              c mk f = mk (c f)
                              instance CauSeq.Completion.instPowCauchyNat {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [Ring β] {abv : βα} [IsAbsoluteValue abv] :
                              Pow (Cauchy abv)
                              Equations
                                @[simp]
                                theorem CauSeq.Completion.mk_pow {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [Ring β] {abv : βα} [IsAbsoluteValue abv] (n : ) (f : CauSeq β abv) :
                                mk f ^ n = mk (f ^ n)
                                instance CauSeq.Completion.instNatCastCauchy {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [Ring β] {abv : βα} [IsAbsoluteValue abv] :
                                Equations
                                  instance CauSeq.Completion.instIntCastCauchy {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [Ring β] {abv : βα} [IsAbsoluteValue abv] :
                                  Equations
                                    @[simp]
                                    theorem CauSeq.Completion.ofRat_natCast {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [Ring β] {abv : βα} [IsAbsoluteValue abv] (n : ) :
                                    ofRat n = n
                                    @[simp]
                                    theorem CauSeq.Completion.ofRat_intCast {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [Ring β] {abv : βα} [IsAbsoluteValue abv] (z : ) :
                                    ofRat z = z
                                    theorem CauSeq.Completion.ofRat_add {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [Ring β] {abv : βα} [IsAbsoluteValue abv] (x y : β) :
                                    ofRat (x + y) = ofRat x + ofRat y
                                    theorem CauSeq.Completion.ofRat_neg {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [Ring β] {abv : βα} [IsAbsoluteValue abv] (x : β) :
                                    theorem CauSeq.Completion.ofRat_mul {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [Ring β] {abv : βα} [IsAbsoluteValue abv] (x y : β) :
                                    ofRat (x * y) = ofRat x * ofRat y
                                    instance CauSeq.Completion.Cauchy.ring {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [Ring β] {abv : βα} [IsAbsoluteValue abv] :
                                    Ring (Cauchy abv)
                                    Equations
                                      def CauSeq.Completion.ofRatRingHom {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [Ring β] {abv : βα} [IsAbsoluteValue abv] :
                                      β →+* Cauchy abv

                                      CauSeq.Completion.ofRat as a RingHom

                                      Equations
                                        Instances For
                                          @[simp]
                                          theorem CauSeq.Completion.ofRatRingHom_apply {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [Ring β] {abv : βα} [IsAbsoluteValue abv] (x : β) :
                                          theorem CauSeq.Completion.ofRat_sub {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [Ring β] {abv : βα} [IsAbsoluteValue abv] (x y : β) :
                                          ofRat (x - y) = ofRat x - ofRat y
                                          instance CauSeq.Completion.Cauchy.commRing {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [CommRing β] {abv : βα} [IsAbsoluteValue abv] :
                                          Equations
                                            instance CauSeq.Completion.instNNRatCast {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [DivisionRing β] {abv : βα} [IsAbsoluteValue abv] :
                                            Equations
                                              instance CauSeq.Completion.instRatCast {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [DivisionRing β] {abv : βα} [IsAbsoluteValue abv] :
                                              Equations
                                                @[simp]
                                                theorem CauSeq.Completion.ofRat_nnratCast {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [DivisionRing β] {abv : βα} [IsAbsoluteValue abv] (q : ℚ≥0) :
                                                ofRat q = q
                                                @[simp]
                                                theorem CauSeq.Completion.ofRat_ratCast {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [DivisionRing β] {abv : βα} [IsAbsoluteValue abv] (q : ) :
                                                ofRat q = q
                                                noncomputable instance CauSeq.Completion.instInvCauchy {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [DivisionRing β] {abv : βα} [IsAbsoluteValue abv] :
                                                Inv (Cauchy abv)
                                                Equations
                                                  theorem CauSeq.Completion.inv_zero {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [DivisionRing β] {abv : βα} [IsAbsoluteValue abv] :
                                                  0⁻¹ = 0
                                                  @[simp]
                                                  theorem CauSeq.Completion.inv_mk {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [DivisionRing β] {abv : βα} [IsAbsoluteValue abv] {f : CauSeq β abv} (hf : ¬f.LimZero) :
                                                  (mk f)⁻¹ = mk (f.inv hf)
                                                  theorem CauSeq.Completion.cau_seq_zero_ne_one {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [DivisionRing β] {abv : βα} [IsAbsoluteValue abv] :
                                                  ¬0 1
                                                  theorem CauSeq.Completion.zero_ne_one {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [DivisionRing β] {abv : βα} [IsAbsoluteValue abv] :
                                                  0 1
                                                  theorem CauSeq.Completion.inv_mul_cancel {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [DivisionRing β] {abv : βα} [IsAbsoluteValue abv] {x : Cauchy abv} :
                                                  x 0x⁻¹ * x = 1
                                                  theorem CauSeq.Completion.mul_inv_cancel {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [DivisionRing β] {abv : βα} [IsAbsoluteValue abv] {x : Cauchy abv} :
                                                  x 0x * x⁻¹ = 1
                                                  theorem CauSeq.Completion.ofRat_inv {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [DivisionRing β] {abv : βα} [IsAbsoluteValue abv] (x : β) :
                                                  noncomputable instance CauSeq.Completion.instDivInvMonoid {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [DivisionRing β] {abv : βα} [IsAbsoluteValue abv] :
                                                  Equations
                                                    theorem CauSeq.Completion.ofRat_div {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [DivisionRing β] {abv : βα} [IsAbsoluteValue abv] (x y : β) :
                                                    ofRat (x / y) = ofRat x / ofRat y
                                                    noncomputable instance CauSeq.Completion.Cauchy.divisionRing {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [DivisionRing β] {abv : βα} [IsAbsoluteValue abv] :

                                                    The Cauchy completion forms a division ring.

                                                    Equations
                                                      unsafe instance CauSeq.Completion.instReprCauchy {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [DivisionRing β] {abv : βα} [IsAbsoluteValue abv] [Repr β] :
                                                      Repr (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.

                                                      Equations
                                                        noncomputable instance CauSeq.Completion.Cauchy.field {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [Field β] {abv : βα} [IsAbsoluteValue abv] :

                                                        The Cauchy completion forms a field.

                                                        Equations
                                                          class CauSeq.IsComplete {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] (β : 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 const abv b

                                                            Every Cauchy sequence has a limit.

                                                          Instances
                                                            theorem CauSeq.complete {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [Ring β] {abv : βα} [IsAbsoluteValue abv] [IsComplete β abv] (s : CauSeq β abv) :
                                                            ∃ (b : β), s const abv b
                                                            noncomputable def CauSeq.lim {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [Ring β] {abv : βα} [IsAbsoluteValue abv] [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} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [Ring β] {abv : βα} [IsAbsoluteValue abv] [IsComplete β abv] (s : CauSeq β abv) :
                                                                s const abv s.lim
                                                                theorem CauSeq.eq_lim_of_const_equiv {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [Ring β] {abv : βα} [IsAbsoluteValue abv] [IsComplete β abv] {f : CauSeq β abv} {x : β} (h : const abv x f) :
                                                                x = f.lim
                                                                theorem CauSeq.lim_eq_of_equiv_const {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [Ring β] {abv : βα} [IsAbsoluteValue abv] [IsComplete β abv] {f : CauSeq β abv} {x : β} (h : f const abv x) :
                                                                f.lim = x
                                                                theorem CauSeq.lim_eq_lim_of_equiv {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [Ring β] {abv : βα} [IsAbsoluteValue abv] [IsComplete β abv] {f g : CauSeq β abv} (h : f g) :
                                                                f.lim = g.lim
                                                                @[simp]
                                                                theorem CauSeq.lim_const {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [Ring β] {abv : βα} [IsAbsoluteValue abv] [IsComplete β abv] (x : β) :
                                                                (const abv x).lim = x
                                                                theorem CauSeq.lim_add {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [Ring β] {abv : βα} [IsAbsoluteValue abv] [IsComplete β abv] (f g : CauSeq β abv) :
                                                                f.lim + g.lim = (f + g).lim
                                                                theorem CauSeq.lim_mul_lim {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [Ring β] {abv : βα} [IsAbsoluteValue abv] [IsComplete β abv] (f g : CauSeq β abv) :
                                                                f.lim * g.lim = (f * g).lim
                                                                theorem CauSeq.lim_mul {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [Ring β] {abv : βα} [IsAbsoluteValue abv] [IsComplete β abv] (f : CauSeq β abv) (x : β) :
                                                                f.lim * x = (f * const abv x).lim
                                                                theorem CauSeq.lim_neg {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [Ring β] {abv : βα} [IsAbsoluteValue abv] [IsComplete β abv] (f : CauSeq β abv) :
                                                                (-f).lim = -f.lim
                                                                theorem CauSeq.lim_eq_zero_iff {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [Ring β] {abv : βα} [IsAbsoluteValue abv] [IsComplete β abv] (f : CauSeq β abv) :
                                                                theorem CauSeq.lim_inv {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type u_2} [Field β] {abv : βα} [IsAbsoluteValue abv] [IsComplete β abv] {f : CauSeq β abv} (hf : ¬f.LimZero) :
                                                                (f.inv hf).lim = f.lim⁻¹
                                                                theorem CauSeq.lim_le {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [IsComplete α abs] {f : CauSeq α abs} {x : α} (h : f const abs x) :
                                                                f.lim x
                                                                theorem CauSeq.le_lim {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [IsComplete α abs] {f : CauSeq α abs} {x : α} (h : const abs x f) :
                                                                x f.lim
                                                                theorem CauSeq.lt_lim {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [IsComplete α abs] {f : CauSeq α abs} {x : α} (h : const abs x < f) :
                                                                x < f.lim
                                                                theorem CauSeq.lim_lt {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [IsComplete α abs] {f : CauSeq α abs} {x : α} (h : f < const abs x) :
                                                                f.lim < x