Geometric sequences in commutative rings

Content created by Louis Wasserman.

Created on 2025-11-07.
Last modified on 2025-11-10.

module commutative-algebra.geometric-sequences-commutative-rings where
Imports 
open import commutative-algebra.commutative-rings
open import commutative-algebra.commutative-semirings
open import commutative-algebra.geometric-sequences-commutative-semirings
open import commutative-algebra.groups-of-units-commutative-rings
open import commutative-algebra.invertible-elements-commutative-rings
open import commutative-algebra.powers-of-elements-commutative-rings
open import commutative-algebra.sums-of-finite-sequences-of-elements-commutative-rings

open import elementary-number-theory.natural-numbers

open import foundation.action-on-identifications-binary-functions
open import foundation.action-on-identifications-functions
open import foundation.binary-transport
open import foundation.dependent-pair-types
open import foundation.function-extensionality
open import foundation.function-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.propositions
open import foundation.sets
open import foundation.universe-levels

open import group-theory.arithmetic-sequences-semigroups

open import lists.finite-sequences
open import lists.sequences

Ideas

A geometric sequence in a commutative ring is an geometric sequence in the ring’s multiplicative semigroup.

These are sequences of the form n ↦ a * rⁿ, for elements a, r in the ring.

Definitions

Geometric sequences in commutative rings

module _
  {l : Level} (R : Commutative-Ring l)
  where

  geometric-sequence-Commutative-Ring : UU l
  geometric-sequence-Commutative-Ring =
    geometric-sequence-Commutative-Semiring
      ( commutative-semiring-Commutative-Ring R)

  is-geometric-sequence-Commutative-Ring :
    sequence (type-Commutative-Ring R) → UU l
  is-geometric-sequence-Commutative-Ring =
    is-geometric-sequence-Commutative-Semiring
      ( commutative-semiring-Commutative-Ring R)

module _
  {l : Level} (R : Commutative-Ring l)
  (u : geometric-sequence-Commutative-Ring R)
  where

  seq-geometric-sequence-Commutative-Ring : ℕ → type-Commutative-Ring R
  seq-geometric-sequence-Commutative-Ring =
    seq-geometric-sequence-Commutative-Semiring
      ( commutative-semiring-Commutative-Ring R)
      ( u)

  is-geometric-seq-geometric-sequence-Commutative-Ring :
    is-geometric-sequence-Commutative-Semiring
      ( commutative-semiring-Commutative-Ring R)
      ( seq-geometric-sequence-Commutative-Ring)
  is-geometric-seq-geometric-sequence-Commutative-Ring =
    is-geometric-seq-geometric-sequence-Commutative-Semiring
      ( commutative-semiring-Commutative-Ring R)
      ( u)

  common-ratio-geometric-sequence-Commutative-Ring :
    type-Commutative-Ring R
  common-ratio-geometric-sequence-Commutative-Ring =
    common-ratio-geometric-sequence-Commutative-Semiring
      ( commutative-semiring-Commutative-Ring R)
      ( u)

  is-common-ratio-geometric-sequence-Commutative-Ring :
    ( n : ℕ) →
    ( seq-geometric-sequence-Commutative-Ring (succ-ℕ n)) ＝
    ( mul-Commutative-Ring
      ( R)
      ( seq-geometric-sequence-Commutative-Ring n)
      ( common-ratio-geometric-sequence-Commutative-Ring))
  is-common-ratio-geometric-sequence-Commutative-Ring =
    is-common-ratio-geometric-sequence-Commutative-Semiring
      ( commutative-semiring-Commutative-Ring R)
      ( u)

  initial-term-geometric-sequence-Commutative-Ring :
    type-Commutative-Ring R
  initial-term-geometric-sequence-Commutative-Ring =
    initial-term-geometric-sequence-Commutative-Semiring
      ( commutative-semiring-Commutative-Ring R)
      ( u)

The standard geometric sequences in a commutative ring

The standard geometric sequence with initial term a and common factor r is the sequence u defined by:

  • u₀ = a
  • uₙ₊₁ = uₙ * r
module _
  {l : Level} (R : Commutative-Ring l) (a r : type-Commutative-Ring R)
  where

  standard-geometric-sequence-Commutative-Ring :
    geometric-sequence-Commutative-Ring R
  standard-geometric-sequence-Commutative-Ring =
    standard-geometric-sequence-Commutative-Semiring
      ( commutative-semiring-Commutative-Ring R)
      ( a)
      ( r)

  seq-standard-geometric-sequence-Commutative-Ring :
    ℕ → type-Commutative-Ring R
  seq-standard-geometric-sequence-Commutative-Ring =
    seq-geometric-sequence-Commutative-Ring R
      standard-geometric-sequence-Commutative-Ring

  is-geometric-standard-geometric-sequence-Commutative-Ring :
    is-geometric-sequence-Commutative-Semiring
      ( commutative-semiring-Commutative-Ring R)
      ( seq-standard-geometric-sequence-Commutative-Ring)
  is-geometric-standard-geometric-sequence-Commutative-Ring =
    is-geometric-seq-geometric-sequence-Commutative-Ring R
      standard-geometric-sequence-Commutative-Ring

The geometric sequences n ↦ a * rⁿ

module _
  {l : Level} (R : Commutative-Ring l) (a r : type-Commutative-Ring R)
  where

  mul-pow-nat-Commutative-Ring : ℕ → type-Commutative-Ring R
  mul-pow-nat-Commutative-Ring n =
    mul-Commutative-Ring R a (power-Commutative-Ring R n r)

  geometric-mul-pow-nat-Commutative-Ring : geometric-sequence-Commutative-Ring R
  geometric-mul-pow-nat-Commutative-Ring =
    geometric-mul-pow-nat-Commutative-Semiring
      ( commutative-semiring-Commutative-Ring R)
      ( a)
      ( r)

  initial-term-mul-pow-nat-Commutative-Ring : type-Commutative-Ring R
  initial-term-mul-pow-nat-Commutative-Ring =
    initial-term-geometric-sequence-Commutative-Ring
      ( R)
      ( geometric-mul-pow-nat-Commutative-Ring)

  eq-initial-term-mul-pow-nat-Commutative-Ring :
    initial-term-mul-pow-nat-Commutative-Ring ＝ a
  eq-initial-term-mul-pow-nat-Commutative-Ring =
    right-unit-law-mul-Commutative-Ring R a

Properties

Any geometric sequence is homotopic to a standard geometric sequence

module _
  {l : Level} (R : Commutative-Ring l)
  (u : geometric-sequence-Commutative-Ring R)
  where

  htpy-seq-standard-geometric-sequence-Commutative-Ring :
    ( seq-geometric-sequence-Commutative-Ring R
      ( standard-geometric-sequence-Commutative-Ring R
        ( initial-term-geometric-sequence-Commutative-Ring R u)
        ( common-ratio-geometric-sequence-Commutative-Ring R u))) ~
    ( seq-geometric-sequence-Commutative-Ring R u)
  htpy-seq-standard-geometric-sequence-Commutative-Ring =
    htpy-seq-standard-geometric-sequence-Commutative-Semiring
      ( commutative-semiring-Commutative-Ring R)
      ( u)

The nth term of a geometric sequence with initial term a and common ratio r is a * rⁿ

module _
  {l : Level} (R : Commutative-Ring l) (a r : type-Commutative-Ring R)
  where

  htpy-mul-pow-standard-geometric-sequence-Commutative-Ring :
    mul-pow-nat-Commutative-Ring R a r ~
    seq-standard-geometric-sequence-Commutative-Ring R a r
  htpy-mul-pow-standard-geometric-sequence-Commutative-Ring =
    htpy-mul-pow-standard-geometric-sequence-Commutative-Semiring
      ( commutative-semiring-Commutative-Ring R)
      ( a)
      ( r)

  initial-term-standard-geometric-sequence-Commutative-Ring :
    seq-standard-geometric-sequence-Commutative-Ring R a r 0 ＝ a
  initial-term-standard-geometric-sequence-Commutative-Ring =
    ( inv (htpy-mul-pow-standard-geometric-sequence-Commutative-Ring 0)) ∙
    ( eq-initial-term-mul-pow-nat-Commutative-Ring R a r)

module _
  {l : Level} (R : Commutative-Ring l)
  (u : geometric-sequence-Commutative-Ring R)
  where

  htpy-mul-pow-geometric-sequence-Commutative-Ring :
    mul-pow-nat-Commutative-Ring
      ( R)
      ( initial-term-geometric-sequence-Commutative-Ring R u)
      ( common-ratio-geometric-sequence-Commutative-Ring R u) ~
    seq-geometric-sequence-Commutative-Ring R u
  htpy-mul-pow-geometric-sequence-Commutative-Ring n =
    ( htpy-mul-pow-standard-geometric-sequence-Commutative-Ring
      ( R)
      ( initial-term-geometric-sequence-Commutative-Ring R u)
      ( common-ratio-geometric-sequence-Commutative-Ring R u)
      ( n)) ∙
    ( htpy-seq-standard-geometric-sequence-Commutative-Semiring
      ( commutative-semiring-Commutative-Ring R)
      ( u)
      ( n))

Constant sequences are geometric with common ratio one

module _
  {l : Level} (R : Commutative-Ring l) (a : type-Commutative-Ring R)
  where

  geometric-const-sequence-Commutative-Ring :
    geometric-sequence-Commutative-Ring R
  geometric-const-sequence-Commutative-Ring =
    geometric-const-sequence-Commutative-Semiring
      ( commutative-semiring-Commutative-Ring R)
      ( a)

Finite geometric sequences

module _
  {l : Level} (R : Commutative-Ring l) (a r : type-Commutative-Ring R)
  where

  standard-geometric-fin-sequence-Commutative-Ring :
    (n : ℕ) → fin-sequence (type-Commutative-Ring R) n
  standard-geometric-fin-sequence-Commutative-Ring =
    fin-sequence-sequence
      ( seq-standard-geometric-sequence-Commutative-Ring R a r)

  sum-standard-geometric-fin-sequence-Commutative-Ring :
    (n : ℕ) → type-Commutative-Ring R
  sum-standard-geometric-fin-sequence-Commutative-Ring =
    sum-standard-geometric-fin-sequence-Commutative-Semiring
      ( commutative-semiring-Commutative-Ring R)
      ( a)
      ( r)

The sum of a finite geometric sequence

module _
  {l : Level} (R : Commutative-Ring l) (a r : type-Commutative-Ring R)
  (let _*R_ = mul-Commutative-Ring R)
  (let _+R_ = add-Commutative-Ring R)
  (let _-R_ = right-subtraction-Commutative-Ring R)
  (let zero-R = zero-Commutative-Ring R)
  (let one-R = one-Commutative-Ring R)
  where

  abstract
    compute-sum-standard-geometric-fin-sequence-succ-Commutative-Ring :
      (n : ℕ) →
      sum-standard-geometric-fin-sequence-Commutative-Ring R
        ( a)
        ( r)
        ( succ-ℕ n) ＝
      add-Commutative-Ring R
        ( a)
        ( mul-Commutative-Ring R
          ( r)
          ( sum-standard-geometric-fin-sequence-Commutative-Ring R a r n))
    compute-sum-standard-geometric-fin-sequence-succ-Commutative-Ring =
      compute-sum-standard-geometric-fin-sequence-succ-Commutative-Semiring
        ( commutative-semiring-Commutative-Ring R)
        ( a)
        ( r)

  abstract
    compute-sum-standard-geometric-fin-sequence-Commutative-Ring :
      (H :
        is-invertible-element-Commutative-Ring R
          ( right-subtraction-Commutative-Ring R (one-Commutative-Ring R) r)) →
      (n : ℕ) →
      sum-standard-geometric-fin-sequence-Commutative-Ring R a r n ＝
      mul-Commutative-Ring R
        ( mul-Commutative-Ring R
          ( a)
          ( inv-is-invertible-element-Commutative-Ring R H))
        ( right-subtraction-Commutative-Ring R
          ( one-Commutative-Ring R)
          ( power-Commutative-Ring R n r))
    compute-sum-standard-geometric-fin-sequence-Commutative-Ring
      (1/⟨1-r⟩ , H) 0 =
      inv
        ( equational-reasoning
          (a *R 1/⟨1-r⟩) *R (one-R -R one-R)
          ＝ (a *R 1/⟨1-r⟩) *R zero-R
            by
              ap-mul-Commutative-Ring R
                ( refl)
                ( right-inverse-law-add-Commutative-Ring R one-R)
          ＝ zero-R
            by right-zero-law-mul-Commutative-Ring R _)
    compute-sum-standard-geometric-fin-sequence-Commutative-Ring
      (1/⟨1-r⟩ , H) (succ-ℕ n) =
      equational-reasoning
        sum-standard-geometric-fin-sequence-Commutative-Ring R a r (succ-ℕ n)
        ＝
          sum-standard-geometric-fin-sequence-Commutative-Ring R a r n +R
          seq-standard-geometric-sequence-Commutative-Ring R a r n
          by
            cons-sum-fin-sequence-type-Commutative-Ring R
              ( n)
              ( standard-geometric-fin-sequence-Commutative-Ring R
                ( a)
                ( r)
                ( succ-ℕ n))
              ( refl)
        ＝
          ( (a *R 1/⟨1-r⟩) *R (one-R -R power-Commutative-Ring R n r)) +R
          ( a *R power-Commutative-Ring R n r)
          by
            ap-add-Commutative-Ring R
              ( compute-sum-standard-geometric-fin-sequence-Commutative-Ring
                ( 1/⟨1-r⟩ , H)
                ( n))
              ( inv
                ( htpy-mul-pow-standard-geometric-sequence-Commutative-Ring R
                  ( a)
                  ( r)
                  ( n)))
        ＝
          ( a *R (1/⟨1-r⟩ *R (one-R -R power-Commutative-Ring R n r))) +R
          ( a *R (one-R *R power-Commutative-Ring R n r))
          by
            ap-add-Commutative-Ring R
              ( associative-mul-Commutative-Ring R _ _ _)
              ( ap-mul-Commutative-Ring R
                ( refl)
                ( inv (left-unit-law-mul-Commutative-Ring R _)))
        ＝
          a *R
          ( (1/⟨1-r⟩ *R (one-R -R power-Commutative-Ring R n r)) +R
            (one-R *R power-Commutative-Ring R n r))
          by inv (left-distributive-mul-add-Commutative-Ring R a _ _)
        ＝
          a *R
          ( ( 1/⟨1-r⟩ *R (one-R -R power-Commutative-Ring R n r)) +R
            ( (1/⟨1-r⟩ *R (one-R -R r)) *R power-Commutative-Ring R n r))
            by
              ap-mul-Commutative-Ring R
                ( refl)
                ( ap-add-Commutative-Ring R
                  ( refl)
                  ( ap-mul-Commutative-Ring R (inv (pr2 H)) refl))
        ＝
          a *R
          ( ( 1/⟨1-r⟩ *R (one-R -R power-Commutative-Ring R n r)) +R
            ( 1/⟨1-r⟩ *R ((one-R -R r) *R power-Commutative-Ring R n r)))
          by
            ap-mul-Commutative-Ring R
              ( refl)
              ( ap-add-Commutative-Ring R
                ( refl)
                ( associative-mul-Commutative-Ring R _ _ _))
        ＝
          a *R
          ( 1/⟨1-r⟩ *R
            ( ( one-R -R power-Commutative-Ring R n r) +R
              ( (one-R -R r) *R power-Commutative-Ring R n r)))
          by
            ap-mul-Commutative-Ring R
              ( refl)
              ( inv (left-distributive-mul-add-Commutative-Ring R _ _ _))
        ＝
          ( a *R 1/⟨1-r⟩) *R
          ( ( one-R -R power-Commutative-Ring R n r) +R
            ( (one-R -R r) *R power-Commutative-Ring R n r))
          by inv (associative-mul-Commutative-Ring R _ _ _)
        ＝
          ( a *R 1/⟨1-r⟩) *R
          ( ( one-R -R power-Commutative-Ring R n r) +R
            ( (one-R *R power-Commutative-Ring R n r) -R
              (r *R power-Commutative-Ring R n r)))
          by
            ap-mul-Commutative-Ring R
              ( refl)
              ( ap-add-Commutative-Ring R
                ( refl)
                ( right-distributive-mul-right-subtraction-Commutative-Ring R
                  ( _)
                  ( _)
                  ( _)))
        ＝
          ( a *R 1/⟨1-r⟩) *R
          ( ( one-R -R power-Commutative-Ring R n r) +R
            ( power-Commutative-Ring R n r -R
              power-Commutative-Ring R (succ-ℕ n) r))
          by
            ap-mul-Commutative-Ring R
              ( refl)
              ( ap-add-Commutative-Ring R
                ( refl)
                ( ap-right-subtraction-Commutative-Ring R
                  ( left-unit-law-mul-Commutative-Ring R _)
                  ( inv (power-succ-Commutative-Ring' R n r))))
        ＝
          ( a *R 1/⟨1-r⟩) *R
          ( one-R -R power-Commutative-Ring R (succ-ℕ n) r)
          by
            ap-mul-Commutative-Ring R
              ( refl)
              ( add-right-subtraction-Commutative-Ring R _ _ _)

Recent changes