open import 1Lab.Prelude hiding (_*_ ; _+_ ; _-_)

open import Algebra.Ring.Commutative
open import Algebra.Ring.Solver
open import Algebra.Ring

open import Data.Set.Coequaliser hiding (_/_)
open import Data.Nat.Base using (_≀_)
module Algebra.Ring.Localisation where

Localisations of commutative ringsπŸ”—

The localisation of a commutative ring at a set of elements is the universal solution to forcing the elements of to become invertible, analogously to how localisations of a category universally invert a class of maps in Explicitly, it is a commutative ring equipped with a homomorphism which sends elements to invertible elements and which is initial among these.

The elements of are given by formal fractions, which we will write with and Type-theoretically, such a fraction is really a triple, since we must also consider the witness that the denominator belongs to but, since these proofs do not matter for identity of fractions, we will generally omit them in the prose.

record Fraction {β„“ β„“'} {R : Type β„“} (S : R β†’ Type β„“') : Type (β„“ βŠ” β„“') where
  no-eta-equality ; pattern
  constructor _/_[_]
  field
    num   : R
    denom : R
    has-denom : denom ∈ S
open Fraction renaming (num to ↑ ; denom to ↓)

pattern _/_ x y = x / y [ _ ]

instance
  H-Level-Fraction
    : βˆ€ {n β„“ β„“'} {R : Type β„“} {S : R β†’ Type β„“'} ⦃ _ : H-Level R n ⦄ ⦃ _ : βˆ€ {x} β†’ H-Level (S x) n ⦄
    β†’ H-Level (Fraction S) n
  H-Level-Fraction {n = n} {k} {R = R} {S} = hlevel-instance
    (retractβ†’is-hlevel {A = R Γ— βˆ«β‚š S} n
      (Ξ» (x , y , p) β†’ x / y [ p ])
      (Ξ» (x / y [ p ]) β†’ x , y , p)
      (Ξ» { (x / y [ p ]) i β†’ x / y [ p ] })
        (hlevel n))

  Inductive-Fraction
    : βˆ€ {β„“ β„“' β„“'' β„“m} {R : Type β„“} {S : R β†’ Type β„“'} {P : Fraction S β†’ Type β„“''}
    β†’ ⦃ _ : Inductive ((num : ⌞ R ⌟) (denom : ⌞ R ⌟) (has : denom ∈ S) β†’ P (num / denom [ has ])) β„“m ⦄
    β†’ Inductive ((x : Fraction S) β†’ P x) β„“m
  Inductive-Fraction ⦃ r ⦄ .Inductive.methods        = r .Inductive.methods
  Inductive-Fraction ⦃ r ⦄ .Inductive.from f (x / s [ p ]) = r .Inductive.from f x s p

Fraction-path
  : βˆ€ {β„“ β„“'} {R : Type β„“} {S : ⌞ R ⌟ β†’ Type β„“'}
  β†’ ⦃ _ : βˆ€ {x} β†’ H-Level (S x) 1 ⦄ {x y : Fraction S}
  β†’ ↑ x ≑ ↑ y β†’ ↓ x ≑ ↓ y β†’ x ≑ y
Fraction-path {S = S} {x = x / s [ p ]} {y / t [ q ] } Ξ± Ξ² i = record
  { num = Ξ± i
  ; denom = Ξ² i
  ; has-denom = is-prop→pathp (λ i → hlevel {T = S (β i)} 1) p q i
  }
module Frac {β„“} (R : CRing β„“) where
  open Explicit R
  open CRing R

To ensure that we have a well-behaved theory of fractions, we will require that is a multiplicatively closed subset of In particular, the presence of allows us to form the fractions for any thus ensuring we have a map We also require that, if and then also This will be important to define both multiplication and identity of fractions.

  record is-multiplicative {β„“'} (S : ⌞ R ⌟ β†’ Type β„“') : Type (β„“ βŠ” β„“') where
    field
      has-1 : 1r ∈ S
      has-* : βˆ€ {x y} β†’ x ∈ S β†’ y ∈ S β†’ (x * y) ∈ S

Under the assumption that is multiplicatively closed, we could attempt to mimic the usual operations on integer-valued fractions on our fractions, for example, defining the sum to be This turns out not to work too well: for example, if we then also define we would have equal to

which is not literally the zero fraction However, we still have so these fractions β€œrepresent the same quantity” β€” they both stand for zero times the formal inverse of something. We could then try to identify fractions and whenever but, in a general ring this relation fails to be transitive, so it can not be equality in a set. Therefore, we allow an β€œadjustment” by one of our formal denominators: the equivalence relation we will impose on fractions identifies whenever there exists with 

  data _β‰ˆ_ {β„“'} {S : ⌞ R ⌟ β†’ Type β„“'} (x y : Fraction S) : Type (β„“ βŠ” β„“') where
    inc : (u : ⌞ R ⌟) (u∈S : u ∈ S) β†’ u * ↑ x * ↓ y ≑ u * ↑ y * ↓ x β†’ x β‰ˆ y
    squash : is-prop (x β‰ˆ y)
  {-
  We define _β‰ˆ_ as a data type so it's injective. It could also be a
  record, but then we'd have to truncate the record in a separate step.
  -}

  instance
    Inductive-β‰ˆ
      : βˆ€ {β„“' β„“'' β„“m} {S : ⌞ R ⌟ β†’ Type β„“'} {x y : Fraction S} {P : x β‰ˆ y β†’ Type β„“''}
      β†’ ⦃ h : βˆ€ {x} β†’ H-Level (P x) 1 ⦄
      β†’ ⦃ r : Inductive ((u : ⌞ R ⌟) (u∈S : u ∈ S) (p : u * ↑ x * ↓ y ≑ u * ↑ y * ↓ x) β†’ P (inc u u∈S p)) β„“m ⦄
      β†’ Inductive ((p : x β‰ˆ y) β†’ P p) β„“m
    Inductive-β‰ˆ ⦃ h ⦄ ⦃ r ⦄ .Inductive.methods = r .Inductive.methods
    Inductive-β‰ˆ {S = S} {x} {y} {P} ⦃ h ⦄ ⦃ r ⦄ .Inductive.from f = go (r .Inductive.from f) where
      go
        : ((u : ⌞ R ⌟) (u∈S : u ∈ S) (p : u * ↑ x * ↓ y ≑ u * ↑ y * ↓ x) β†’ P (inc u u∈S p))
        β†’ βˆ€ x β†’ P x
      go m (inc u u∈S x) = m u u∈S x
      go m (squash x y i) = is-prop→pathp (λ i → hlevel {T = P (squash x y i)} 1) (go m x) (go m y) i

    H-Level-β‰ˆ : βˆ€ {β„“'} {S : ⌞ R ⌟ β†’ Type β„“'} {x y : Fraction S} {n} β†’ H-Level (x β‰ˆ y) (suc n)
    H-Level-β‰ˆ = prop-instance squash

In the literature, this is more commonly phrased as but the equivalence between that and our definition is routine.

  _β‰ˆ'_ : βˆ€ {β„“'} {S : ⌞ R ⌟ β†’ Type β„“'} β†’ Fraction S β†’ Fraction S β†’ Type _
  _β‰ˆ'_ {S = S} (x / s) (y / t) = βˆƒ[ u ∈ R ] (u ∈ S Γ— u * (x * t - y * s) ≑ 0r)
The calculation can be found in this <details> block. 
  β‰ˆβ†’β‰ˆ' : βˆ€ {β„“'} {S : ⌞ R ⌟ β†’ Type β„“'} {x y : Fraction S} β†’ x β‰ˆ y β†’ x β‰ˆ' y
  β‰ˆβ†’β‰ˆ' {x = x / s} {y = y / t} = elim! Ξ» u u∈S p β†’
    let
      prf =
        u * (x * t - y * s)   β‰‘βŸ¨ solve 5 (Ξ» u x t y s β†’ u :* (x :* t :- y :* s) ≔ u :* x :* t :- u :* y :* s) u x t y s refl ⟩
        u * x * t - u * y * s β‰‘βŸ¨ apβ‚‚ _-_ refl (sym p) ⟩
        u * x * t - u * x * t β‰‘βŸ¨ solve 1 (Ξ» x β†’ x :- x ≔ 0) (u * x * t) refl ⟩
        0r                    ∎
    in inc (u , u∈S , prf)

  β‰ˆ'β†’β‰ˆ : βˆ€ {β„“'} {S : ⌞ R ⌟ β†’ Type β„“'} {x y : Fraction S} β†’ x β‰ˆ' y β†’ x β‰ˆ y
  β‰ˆ'β†’β‰ˆ {x = x / s} {y = y / t} = elim! Ξ» u u∈S p β†’
    let
      prf =
        u * x * t - u * y * s β‰‘βŸ¨ solve 5 (Ξ» u x t y s β†’ u :* x :* t :- u :* y :* s ≔ u :* (x :* t :- y :* s)) u x t y s refl ⟩
        u * (x * t - y * s)   β‰‘βŸ¨ p ⟩
        0r                    ∎
    in inc u u∈S (zero-diff prf)
module Loc {β„“} (R : CRing β„“) (S : ⌞ R ⌟ β†’ Ξ©) (mult : Frac.is-multiplicative R (_∈ S)) where
  open Frac.is-multiplicative mult
  open Explicit R
  open CRing R
  open Frac R public

  open Congruence using (_∼_ ; has-is-prop ; reflᢜ ; _βˆ™αΆœ_ ; symᢜ)

Our next step is showing that this relation is actually an equivalence relation. The proof of transitivity is the most interesting step: we assume that and with β€œadjustments” by respectively, but we produce the equation β€” we must consider the denominator of the middle fraction to relate the two endpoints and 

  Fraction-congruence : Congruence (Fraction (_∈ S)) _
  Fraction-congruence ._∼_ = _β‰ˆ_
  Fraction-congruence .has-is-prop (_ / _) (_ / _) = hlevel 1
  Fraction-congruence .reflᢜ {x / s} = inc 1r has-1 refl
  Fraction-congruence .symᢜ {x / s} {y / t} = rec! Ξ» u u∈S p β†’ inc u u∈S (sym p)
  Fraction-congruence ._βˆ™αΆœ_ {x / s} {y / t [ r ]} {z / u} = elim!
    Ξ» v v∈S p w w∈S q β†’
      let
        prf =
          w * v * t * x * u     β‰‘βŸ¨ cring! R ⟩
          w * u * (v * x * t)   β‰‘βŸ¨ ap (w * u *_) p ⟩
          w * u * (v * y * s)   β‰‘βŸ¨ cring! R ⟩
          (w * y * u) * (v * s) β‰‘βŸ¨ apβ‚‚ _*_ q refl ⟩
          (w * z * t) * (v * s) β‰‘βŸ¨ cring! R ⟩
          w * v * t * z * s     ∎
      in
      inc (w * v * t) (has-* (has-* w∈S v∈S) r) prf
  module Fr = Congruence Fraction-congruence
  open Fraction

  private
    /-ap : βˆ€ {x y : Fraction (_∈ S)} β†’ x .num ≑ y .num β†’ x .denom ≑ y .denom β†’ Path Fr.quotient (inc x) (inc y)
    /-ap p q = ap Coeq.inc (Fraction-path p q)

We then define to be the set of fractions identified according to this relation. Since we can immediately cough up the function mapping 

  _/1 : ⌞ R ⌟ β†’ Fr.quotient
  x /1 = inc (x / 1r [ has-1 ])

To define the operations of a ring on we first define them at the level of fractions:

As mentioned above, these operations do not satisfy the laws of a ring on the set of fractions. We must therefore prove that they respect the quotient we’ve taken, and then prove that they satisfy the ring laws on the quotient.

  +f : Fraction (_∈ S) β†’ Fraction (_∈ S) β†’ Fraction (_∈ S)
  +f (x / s [ p ]) (y / t [ q ]) = (x * t + y * s) / (s * t) [ has-* p q ]

  -f : Fraction (_∈ S) β†’ Fraction (_∈ S)
  -f (x / s [ p ]) = (- x) / s [ p ]

  *f : Fraction (_∈ S) β†’ Fraction (_∈ S) β†’ Fraction (_∈ S)
  *f (x / s [ p ]) (y / t [ q ]) = (x * y) / (s * t) [ has-* p q ]
Showing that these operations descend to the quotient is entirely routine algebra; However, the calculations do get pretty long, so we’ll leave them in this <details> block. 
  -β‚—_ : Fr.quotient β†’ Fr.quotient
  -β‚—_ = Quot-elim (Ξ» _ β†’ hlevel 2) (Ξ» x β†’ inc (-f x)) -f-resp where abstract
    -f-resp : βˆ€ x y β†’ x β‰ˆ y β†’ Path Fr.quotient (inc (-f x)) (inc (-f y))
    -f-resp (x / s) (y / t) = elim! Ξ» u u∈S p β†’
      let
        prf =
          u * (- x) * t β‰‘βŸ¨ ap (_* t) *-negater βˆ™ *-negatel ⟩
          - (u * x * t) β‰‘βŸ¨ ap -_ p ⟩
          - (u * y * s) β‰‘βŸ¨ sym *-negatel βˆ™ ap (_* s) (sym *-negater) ⟩
          u * (- y) * s ∎
      in quot (inc u u∈S prf)

  _+β‚—_ : Fr.quotient β†’ Fr.quotient β†’ Fr.quotient
  _+β‚—_ = Fr.opβ‚‚-comm +f (Ξ» a b β†’ Fr.reflᢜ' (+f-comm a b)) +f-resp where abstract
    +f-comm : βˆ€ u v β†’ +f u v ≑ +f v u
    +f-comm (x / s) (y / t) = Fraction-path +-commutes *-commutes

    +f-resp : βˆ€ x u v β†’ u β‰ˆ v β†’ +f x u β‰ˆ +f x v
    +f-resp (x / s) (u / y) (v / z) = rec! Ξ» w w∈S p β†’
      let
        prf =
          w * (x * y + u * s) * (s * z)             β‰‘βŸ¨ cring! R ⟩
          w * x * y * s * z + s * s * ⌜ w * u * z ⌝ β‰‘βŸ¨ ap! p ⟩
          w * x * y * s * z + s * s * ⌜ w * v * y ⌝ β‰‘βŸ¨ cring! R ⟩
          w * (x * z + v * s) * (s * y)             ∎
      in inc w w∈S prf

  _*β‚—_ : Fr.quotient β†’ Fr.quotient β†’ Fr.quotient
  _*β‚—_ = Fr.opβ‚‚-comm *f *f-comm *f-resp where abstract
    *f-comm : βˆ€ u v β†’ *f u v β‰ˆ *f v u
    *f-comm (x / s) (y / t) = inc 1r has-1 (solve 4 (Ξ» x y t s β†’ 1 :* (x :* y) :* (t :* s) ≔ 1 :* (y :* x) :* (s :* t)) x y t s refl)

    *f-resp : βˆ€ x u v β†’ u β‰ˆ v β†’ *f x u β‰ˆ *f x v
    *f-resp (x / s) (u / y) (v / z) = rec! Ξ» w w∈S p β†’
      let
        prf =
          w * (x * u) * (s * z) β‰‘βŸ¨ cring! R ⟩
          s * x * (w * u * z)   β‰‘βŸ¨ ap (s * x *_) p ⟩
          s * x * (w * v * y)   β‰‘βŸ¨ cring! R ⟩
          w * (x * v) * (s * y) ∎
      in inc w w∈S prf
  infixl 8 _+β‚—_
  infixl 9 _*β‚—_
  infix 10 -β‚—_ _/1

  0β‚— 1β‚— : Fr.quotient
  0β‚— = 0r /1
  1β‚— = 1r /1

We choose the zero and identity elements for so that the localising map preserves them definitionally. We’re almost done with the construction; while there’s quite a bit of algebra left to do to show that we have a ring, this is almost entirely automatic. As a warm-up, we can prove that is inverted by whenever 

  /1-inverts : βˆ€ x (p : x ∈ S) β†’ inc (1r / x [ p ]) *β‚— (x /1) ≑ 1β‚—
  /1-inverts x p = quot (inc 1r has-1
    (solve 1 (Ξ» x β†’ 1 :* (1 :* x) :* 1 ≔ 1 :* 1 :* (x :* 1)) x refl))

The actual proof obligation is shown above: we have to establish that which can be shown by a naΓ―ve solver. The equations for each of the ring laws are similarly boring:

  abstract
    +β‚—-idl : βˆ€ x β†’ 0β‚— +β‚— x ≑ x
    +β‚—-idl = elim! Ξ» x s _ β†’ /-ap
      (solve 2 (Ξ» s x β†’ 0 :* s :+ x :* 1 ≔ x) s x refl)
      *-idl

    +β‚—-invr : βˆ€ x β†’ x +β‚— (-β‚— x) ≑ 0β‚—
    +β‚—-invr = elim! Ξ» x s _ β†’ quot (inc 1r has-1 (solve 2
      (Ξ» x s β†’ 1 :* (x :* s :+ (:- x) :* s) :* 1 ≔ 1 :* 0 :* (s :* s)) x s refl))

    +β‚—-assoc : βˆ€ x y z β†’ x +β‚— (y +β‚— z) ≑ (x +β‚— y) +β‚— z
    +β‚—-assoc = elim! Ξ» x s _ y t _ z u _ β†’ /-ap
      (solve 6 (Ξ» x y z s t u β†’
        x :* (t :* u) :+ (y :* u :+ z :* t) :* s
      ≔ (x :* t :+ y :* s) :* u :+ z :* (s :* t)) x y z s t u refl)
      *-associative

    +β‚—-comm : βˆ€ x y β†’ x +β‚— y ≑ y +β‚— x
    +β‚—-comm = elim! Ξ» x s _ y t _ β†’ /-ap +-commutes *-commutes

    *β‚—-idl : βˆ€ x β†’ 1β‚— *β‚— x ≑ x
    *β‚—-idl = elim! Ξ» x s s∈S β†’ quot (inc s s∈S (solve 2
      (Ξ» x s β†’ s :* (1 :* x) :* s ≔ s :* x :* (1 :* s)) x s refl))

    *β‚—-comm : βˆ€ x y β†’ x *β‚— y ≑ y *β‚— x
    *β‚—-comm = elim! Ξ» x s _ y t _ β†’ /-ap *-commutes *-commutes

    *β‚—-assoc : βˆ€ x y z β†’ x *β‚— (y *β‚— z) ≑ (x *β‚— y) *β‚— z
    *β‚—-assoc = elim! Ξ» x s _ y t _ z u _ β†’ /-ap *-associative *-associative

    *β‚—-distribl : βˆ€ x y z β†’ x *β‚— (y +β‚— z) ≑ (x *β‚— y) +β‚— (x *β‚— z)
    *β‚—-distribl = elim! Ξ» x s _ y t _ z u _ β†’
      let
        prf : 1r * (x * (y * u + z * t)) * (s * t * (s * u))
            ≑ 1r * (x * y * (s * u) + x * z * (s * t)) * (s * (t * u))
        prf = cring! R
      in quot (inc 1r has-1 prf)

Finally, these fit together to make a commutative ring.

  private
    module mr = make-ring
    open make-ring

    mk-loc : make-ring Fr.quotient
    mk-loc .ring-is-set = hlevel 2
    mk-loc .0R  = 0β‚—
    mk-loc ._+_ = _+β‚—_
    mk-loc .-_  = -β‚—_
    mk-loc .1R  = 1β‚—
    mk-loc ._*_ = _*β‚—_
    mk-loc .+-idl = +β‚—-idl
    mk-loc .+-invr = +β‚—-invr
    mk-loc .+-assoc = +β‚—-assoc
    mk-loc .+-comm = +β‚—-comm
    mk-loc .*-idl = *β‚—-idl
    mk-loc .*-idr x = *β‚—-comm x 1β‚— βˆ™ *β‚—-idl x
    mk-loc .*-assoc = *β‚—-assoc
    mk-loc .*-distribl = *β‚—-distribl
    mk-loc .*-distribr x y z =
      *β‚—-comm (y +β‚— z) x βˆ™ *β‚—-distribl x y z βˆ™ apβ‚‚ _+β‚—_ (*β‚—-comm x y) (*β‚—-comm x z)

  S⁻¹R : CRing β„“
  S⁻¹R .fst = el! Fr.quotient
  S⁻¹R .snd .CRing-on.has-ring-on = to-ring-on mk-loc
  S⁻¹R .snd .CRing-on.*-commutes {x} {y} = *β‚—-comm x y