Properties of OrderedCommRings

Cubical/Algebra/CommRing/Instances/Fast/Int.agda

@@ -1,8 +1,12 @@
 module Cubical.Algebra.CommRing.Instances.Fast.Int where
 
 open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Function
 
+open import Cubical.Algebra.Ring
 open import Cubical.Algebra.CommRing
+
+open import Cubical.Data.Nat as ℕ using (ℕ ; zero ; suc)
 open import Cubical.Data.Fast.Int as Int renaming (_+_ to _+ℤ_; _·_ to _·ℤ_ ; -_ to -ℤ_)
 
 open CommRingStr using (0r ; 1r ; _+_ ; _·_ ; -_ ; isCommRing)
@@ -21,3 +25,113 @@ isCommRing (snd ℤCommRing) = isCommRingℤ
     isCommRingℤ = makeIsCommRing isSetℤ Int.+Assoc +IdR
                                  -Cancel Int.+Comm Int.·Assoc
                                  Int.·IdR ·DistR+ Int.·Comm
+
+private
+  variable
+    ℓ : Level
+
+module CanonicalHomFromℤ (R : CommRing ℓ) where
+
+  private
+    module R where
+      open CommRingStr (snd R) public
+      open RingTheory (CommRing→Ring R) public
+
+  suc-fromℕ : ∀ x → R.fromℕ (suc x) ≡ R.1r R.+ R.fromℕ x
+  suc-fromℕ zero    = sym (R.+IdR R.1r)
+  suc-fromℕ (suc x) = refl
+
+  fromℕ-pres+ : (x y : ℕ) → R.fromℕ (x ℕ.+ y) ≡ R.fromℕ x R.+ R.fromℕ y
+  fromℕ-pres+ zero          y = sym (R.+IdL _)
+  fromℕ-pres+ (suc zero)    y = suc-fromℕ y
+  fromℕ-pres+ (suc (suc x)) y = cong (R.1r R.+_) (fromℕ-pres+ (suc x) y) ∙ R.+Assoc _ _ _
+
+  fromℤ-pres- : (x : ℤ) → R.fromℤ (-ℤ x) ≡ R.- R.fromℤ x
+  fromℤ-pres- (pos zero)    = sym R.0Selfinverse
+  fromℤ-pres- (pos (suc n)) = refl
+  fromℤ-pres- (negsuc n)    = sym (R.-Idempotent _)
+
+  suc-fromℤ : ∀ z → R.fromℤ (1 +ℤ z) ≡ R.1r R.+ R.fromℤ (z)
+  suc-fromℤ (pos n)          = suc-fromℕ n
+  suc-fromℤ (negsuc zero)    = sym (R.+InvR R.1r)
+  suc-fromℤ (negsuc (suc n)) =
+       sym (cong (R._+ (R.- R.fromℕ (suc n))) (R.+InvR _) ∙ R.+IdL _)
+    ∙∙ sym (R.+Assoc _ _ _)
+    ∙∙ cong (R.1r R.+_) (R.-Dist _ _)
+
+  fromℤ-pres+' : (n m : ℕ) →
+    R.fromℤ (pos n +ℤ negsuc m) ≡
+    R.fromℤ (pos n) R.+ R.fromℤ (negsuc m)
+  fromℤ-pres+' zero    m = sym (R.+IdL _)
+  fromℤ-pres+' (suc n) m =
+      (cong R.fromℤ (sym (+Assoc 1 (pos n) (negsuc m)))
+    ∙ suc-fromℤ (pos n +ℤ negsuc m))
+    ∙∙ cong (R.1r R.+_) (fromℤ-pres+' n m)
+    ∙∙ R.+Assoc _ _ _
+    ∙ cong (R._+ R.fromℤ (negsuc m))
+     (sym (suc-fromℕ n))
+
+  fromℤ-pres+ : (x y : ℤ) → R.fromℤ (x +ℤ y) ≡ R.fromℤ x R.+ R.fromℤ y
+  fromℤ-pres+ (pos n)    (pos m)    = fromℕ-pres+  n m
+  fromℤ-pres+ (pos n)    (negsuc m) = fromℤ-pres+' n m
+  fromℤ-pres+ (negsuc n) (pos m)    = fromℤ-pres+' m n ∙ R.+Comm _ _
+  fromℤ-pres+ (negsuc n) (negsuc m) =
+      cong (R.-_)
+      (cong (R.1r R.+_) (cong R.fromℕ (sym (ℕ.+-suc n m)))
+        ∙ sym (suc-fromℕ (n ℕ.+ suc m))
+        ∙ fromℕ-pres+ (suc n) (suc m))
+    ∙ sym (R.-Dist _ _)
+
+  fromℕ-pres· : (x y : ℕ) → R.fromℕ (x ℕ.· y) ≡ R.fromℕ x R.· R.fromℕ y
+  fromℕ-pres· zero y    = sym (R.0LeftAnnihilates _)
+  fromℕ-pres· (suc x) y =
+      fromℕ-pres+ y (x ℕ.· y)
+    ∙∙ cong₂ (R._+_) (sym (R.·IdL _)) (fromℕ-pres· x y)
+    ∙∙ sym (R.·DistL+ _ _ _)
+    ∙ cong (R._· R.fromℕ y) (sym (suc-fromℕ x))
+  fromℤ-pres· : (x y : ℤ) → R.fromℤ (x ·ℤ y) ≡ R.fromℤ x R.· R.fromℤ y
+  fromℤ-pres· (pos n) (pos m)    = fromℕ-pres· n m
+  fromℤ-pres· (pos n) (negsuc m) =
+      cong R.fromℤ (sym (-DistR· (pos n) (pos (suc m))))
+    ∙∙ (fromℤ-pres- (pos (n ℕ.· suc m))
+      ∙ cong R.-_ (fromℕ-pres· n (suc m)))
+    ∙∙ sym (R.-DistR· _ _)
+  fromℤ-pres· (negsuc n) (pos m) =
+      cong R.fromℤ (sym (-DistL· (pos (suc n)) (pos m)))
+    ∙∙ (fromℤ-pres- (pos ((suc n) ℕ.· m))
+      ∙ cong R.-_ (fromℕ-pres· (suc n) m))
+    ∙∙ sym (R.-DistL· _ _)
+  fromℤ-pres· (negsuc n) (negsuc m) =
+       fromℕ-pres· (suc n) (suc m)
+    ∙∙ cong₂ R._·_ (sym (R.-Idempotent _)) refl
+    ∙∙ R.-Swap· _ _
+
+  isHomFromℤ : IsCommRingHom (ℤCommRing .snd) R.fromℤ (R .snd)
+  isHomFromℤ .IsCommRingHom.pres0 = refl
+  isHomFromℤ .IsCommRingHom.pres1 = refl
+  isHomFromℤ .IsCommRingHom.pres+ = fromℤ-pres+
+  isHomFromℤ .IsCommRingHom.pres· = fromℤ-pres·
+  isHomFromℤ .IsCommRingHom.pres- = fromℤ-pres-
+
+  fromℤHom : CommRingHom ℤCommRing R
+  fst fromℤHom = R.fromℤ
+  snd fromℤHom = isHomFromℤ
+
+  module _ (φ : CommRingHom ℤCommRing R) where
+
+    open IsCommRingHom (snd φ)
+
+    isUniqueFromℕ : ∀ n → R.fromℕ n ≡ φ $cr pos n
+    isUniqueFromℕ zero            = sym pres0
+    isUniqueFromℕ (suc zero)      = sym pres1
+    isUniqueFromℕ (suc k@(suc n)) = cong₂ R._+_ (sym pres1) (isUniqueFromℕ k)
+                                  ∙ sym (pres+ 1 (pos k))
+
+    isUniqueFromℤ : ∀ n → R.fromℤ n ≡ φ $cr n
+    isUniqueFromℤ (pos n)    = isUniqueFromℕ n
+    isUniqueFromℤ (negsuc n) = cong R.-_ (isUniqueFromℕ (suc n))
+                             ∙ sym (pres- (pos (suc n)))
+
+  isContrHom[ℤCR,-] : isContr (CommRingHom ℤCommRing R)
+  fst isContrHom[ℤCR,-] = fromℤHom
+  snd isContrHom[ℤCR,-] = CommRingHom≡ ∘ funExt ∘ isUniqueFromℤ

Cubical/Algebra/OrderedCommRing.agda

@@ -1,3 +1,4 @@
 module Cubical.Algebra.OrderedCommRing where
 
 open import Cubical.Algebra.OrderedCommRing.Base public
+open import Cubical.Algebra.OrderedCommRing.Properties public

Cubical/Algebra/OrderedCommRing/Base.agda

@@ -4,20 +4,25 @@ module Cubical.Algebra.OrderedCommRing.Base where
 -}
 
 open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Function
 open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.SIP
 
+open import Cubical.Algebra.CommRing.Base
+
 import Cubical.Functions.Logic as L
 
-open import Cubical.Relation.Nullary.Base
+open import Cubical.HITs.PropositionalTruncation as PT
 
-open import Cubical.Algebra.CommRing.Base
+open import Cubical.Reflection.RecordEquiv
 
 open import Cubical.Relation.Binary.Base
-open import Cubical.Relation.Binary.Order.Poset hiding (isPseudolattice)
-open import Cubical.Relation.Binary.Order.StrictOrder
-
+open import Cubical.Relation.Binary.Order.Poset hiding (
+  isPseudolattice ; isPropIsPseudolattice)
 open import Cubical.Relation.Binary.Order.Pseudolattice
+open import Cubical.Relation.Binary.Order.StrictOrder
+open import Cubical.Relation.Nullary
 
 open BinaryRelation
 
@@ -53,6 +58,8 @@ record IsOrderedCommRing
                                                                 ; _∧l_ to _⊓_ ; _∨l_ to _⊔_) public
   open IsStrictOrder isStrictOrder hiding (is-set) renaming (is-prop-valued to is-prop-valued< ; is-trans to is-trans<) public
 
+unquoteDecl IsOrderedCommRingIsoΣ = declareRecordIsoΣ IsOrderedCommRingIsoΣ (quote IsOrderedCommRing)
+
 record OrderedCommRingStr (ℓ' : Level) (R : Type ℓ) : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
   constructor orderedcommringstr
   field
@@ -134,3 +141,26 @@ OrderedCommRing→CommRing : OrderedCommRing ℓ ℓ' → CommRing ℓ
 OrderedCommRing→CommRing R .fst = R .fst
 OrderedCommRing→CommRing R .snd = commringstr _ _ _ _ _ isCommRing where
   open OrderedCommRingStr (str R)
+
+isPropIsOrderedCommRing : {R : Type ℓ}
+                          → (0r 1r : R)
+                          → (_+_ _·_ : R → R → R) (-_ : R → R)
+                          → (_<_ _≤_ : R → R → Type ℓ')
+                          → isProp (IsOrderedCommRing 0r 1r _+_ _·_ -_ _<_ _≤_)
+isPropIsOrderedCommRing 0r 1r _+_ _·_ -_ _<_ _≤_ = isOfHLevelRetractFromIso 1
+  IsOrderedCommRingIsoΣ $
+    isPropΣ (isPropIsCommRing _ _ _ _ _) λ isCR →
+    isPropΣ (isPropIsPseudolattice _) λ isPL →
+    isPropΣ (isPropIsStrictOrder _) λ isSO →
+    isProp× (isPropΠ3 λ _ _ _ → isPL .IsPseudolattice.is-prop-valued _ _) $
+    isProp× (isPropΠ2 λ x y → isOfHLevel≃ 1
+      (IsPoset.is-prop-valued (IsPseudolattice.isPoset isPL) x y)
+      (isProp¬ (y < x))) $
+    isProp× (isPropΠ4 λ _ _ _ _ → isPL .IsPseudolattice.is-prop-valued _ _) $
+    isProp× (isPropΠ4 λ _ _ _ _ → isSO .IsStrictOrder.is-prop-valued _ _) $
+    isProp× (isPropΠ3 λ _ _ _ → PT.squash₁) $
+    isProp× (isPropΠ5 λ _ _ _ _ _ → isSO .IsStrictOrder.is-prop-valued _ _) $
+    isProp× (isPropΠ5 λ _ _ _ _ _ → isSO .IsStrictOrder.is-prop-valued _ _) $
+    isProp× (isPropΠ5 λ _ _ _ _ _ → isPL .IsPseudolattice.is-prop-valued _ _) $
+    isProp× (isPropΠ5 λ _ _ _ _ _ → isSO .IsStrictOrder.is-prop-valued _ _)
+            (isSO .IsStrictOrder.is-prop-valued _ _)

Cubical/Algebra/OrderedCommRing/Instances/Fast/Int.agda

@@ -8,15 +8,20 @@ open import Cubical.Data.Empty as ⊥
 
 open import Cubical.HITs.PropositionalTruncation
 
+open import Cubical.Data.Nat as ℕ using (ℕ ; zero ; suc)
+open import Cubical.Data.Nat.Order as ℕ using () renaming (_≤_ to _≤ℕ_ ; _<_ to _<ℕ_)
+import Cubical.Data.Nat.Order.Inductive as ℕ
 open import Cubical.Data.Fast.Int as ℤ
   renaming (_+_ to _+ℤ_ ; _-_ to _-ℤ_; -_ to -ℤ_ ; _·_ to _·ℤ_)
 open import Cubical.Data.Fast.Int.Order
   renaming (_<_ to _<ℤ_ ; _≤_ to _≤ℤ_)
 
+open import Cubical.Algebra.Ring
 open import Cubical.Algebra.CommRing
 open import Cubical.Algebra.CommRing.Instances.Fast.Int
 
 open import Cubical.Algebra.OrderedCommRing
+open import Cubical.Algebra.OrderedCommRing.Morphisms
 
 open import Cubical.Relation.Nullary
 
@@ -64,3 +69,100 @@ isOrderedCommRing (snd ℤOrderedCommRing) = isOrderedCommRingℤ
     isOrderedCommRingℤ .·MonoR≤         = λ _ _ _ → 0≤o→≤-·o
     isOrderedCommRingℤ .·MonoR<         = λ _ _ _ → 0<o→<-·o
     isOrderedCommRingℤ .0<1             = zero-<possuc
+
+private
+  variable
+    ℓ ℓ' : Level
+
+module CanonicalMonoFromℤ (R : OrderedCommRing ℓ ℓ') where
+
+  open CanonicalHomFromℤ (OrderedCommRing→CommRing R)
+  open OrderedCommRingTheory R
+
+  private
+    module R where
+      open OrderedCommRingStr (snd R) public
+      open RingTheory (OrderedCommRing→Ring R) using (fromℕ ; fromℤ) public
+
+  1≤fromℕsuc : ∀ n → R.1r R.≤ R.fromℕ (suc n)
+  1≤fromℕsuc zero    = R.is-refl R.1r
+  1≤fromℕsuc (suc n) =
+    subst (R._≤ R.fromℕ (suc (suc n))) (R.+IdL R.1r) (+Mono≤ _ _ _ _ 0≤1 (1≤fromℕsuc n))
+
+  0<fromℕsuc : ∀ n → R.0r R.< R.fromℕ (suc n)
+  0<fromℕsuc n = R.<-≤-trans _ _ _ R.0<1 (1≤fromℕsuc n)
+
+  0≤fromℕ : ∀ n → R.0r R.≤ R.fromℕ n
+  0≤fromℕ zero    = R.is-refl R.0r
+  0≤fromℕ (suc n) = R.<-≤-weaken _ _ (0<fromℕsuc n)
+
+  fromℕ-pres≤ᵗ : ∀ m n → m ℕ.≤ᵗ n → R.fromℕ m R.≤ R.fromℕ n
+  fromℕ-pres≤ᵗ zero          n             t = 0≤fromℕ n
+  fromℕ-pres≤ᵗ (suc zero)    (suc n)       t = 1≤fromℕsuc n
+  fromℕ-pres≤ᵗ (suc (suc m)) (suc (suc n)) t =
+    +MonoL≤ _ _ _ (fromℕ-pres≤ᵗ (suc m) (suc n) t)
+
+  fromℕ-pres≤ : ∀ m n → m ≤ℕ n → R.fromℕ m R.≤ R.fromℕ n
+  fromℕ-pres≤ m n = fromℕ-pres≤ᵗ m n ∘ ℕ.≤→≤ᵇ
+
+  fromℕ-pres<ᵗ : ∀ m n → m ℕ.<ᵗ n → R.fromℕ m R.< R.fromℕ n
+  fromℕ-pres<ᵗ zero          (suc n)       t = 0<fromℕsuc n
+  fromℕ-pres<ᵗ (suc zero)    (suc (suc n)) t = <SumLeftPos R.1r _ (0<fromℕsuc n)
+  fromℕ-pres<ᵗ (suc (suc m)) (suc (suc n)) t =
+    +MonoL< _ _ _ (fromℕ-pres<ᵗ (suc m) (suc n) t)
+
+  fromℕ-pres< : ∀ m n → m <ℕ n → R.fromℕ m R.< R.fromℕ n
+  fromℕ-pres< m n = fromℕ-pres<ᵗ m n ∘ ℕ.<→<ᵇ
+
+  fromℤ-pres≤ : ∀ m n → m ≤ℤ n → R.fromℤ m R.≤ R.fromℤ n
+  fromℤ-pres≤ (pos m)    (pos n)    (pos≤pos p)       = fromℕ-pres≤ᵗ m n p
+  fromℤ-pres≤ (negsuc m) (pos n)    negsuc≤pos        =
+    R.is-trans≤ _ _ _ (0≤→-≤0 _ (0≤fromℕ (suc m))) (0≤fromℕ n)
+  fromℤ-pres≤ (negsuc m) (negsuc n) (negsuc≤negsuc p) =
+    -Flip≤ _ _ (fromℕ-pres≤ᵗ (suc n) (suc m) p)
+
+  fromℤ-pres< : ∀ m n → m <ℤ n → R.fromℤ m R.< R.fromℤ n
+  fromℤ-pres< (pos m)    (pos n)    (pos<pos p)       = fromℕ-pres<ᵗ m n p
+  fromℤ-pres< (negsuc m) (pos n)    negsuc<pos        =
+    R.<-≤-trans _ _ _ (0<→-<0 _ (0<fromℕsuc m)) (0≤fromℕ n)
+  fromℤ-pres< (negsuc m) (negsuc n) (negsuc<negsuc p) =
+    -Flip< _ _ (fromℕ-pres<ᵗ (suc n) (suc m) p)
+
+  fromℤ-reflect< : ∀ m n → R.fromℤ m R.< R.fromℤ n → m <ℤ n
+  fromℤ-reflect< m n fm<fn with m ≟ n
+  ... | lt m<n = m<n
+  ... | eq m≡n = ⊥.rec (R.is-irrefl _ (subst (R._< _) (cong R.fromℤ m≡n) fm<fn))
+  ... | gt m>n = ⊥.rec (R.is-asym _ _ fm<fn (fromℤ-pres< n m m>n))
+
+  isOCRHomFromℤ : IsOrderedCommRingHom (snd ℤOrderedCommRing) R.fromℤ (snd R)
+  isOCRHomFromℤ .IsOrderedCommRingHom.isCommRingHom = isHomFromℤ
+  isOCRHomFromℤ .IsOrderedCommRingHom.pres≤         = fromℤ-pres≤
+  isOCRHomFromℤ .IsOrderedCommRingHom.reflect<      = fromℤ-reflect<
+
+  isOCRMonoFromℤ : IsOrderedCommRingMono (snd ℤOrderedCommRing) R.fromℤ (snd R)
+  isOCRMonoFromℤ .IsOrderedCommRingMono.isOrderedCommRingHom = isOCRHomFromℤ
+  isOCRMonoFromℤ .IsOrderedCommRingMono.pres<                = fromℤ-pres<
+
+  fromℤOCR : OrderedCommRingHom ℤOrderedCommRing R
+  fst fromℤOCR = R.fromℤ
+  snd fromℤOCR = isOCRHomFromℤ
+
+  fromℤOCRMono : OrderedCommRingMono ℤOrderedCommRing R
+  fst fromℤOCRMono = R.fromℤ
+  snd fromℤOCRMono = isOCRMonoFromℤ
+
+  isUniqueFromℤOCR : (φ : OrderedCommRingHom ℤOrderedCommRing R)
+                   → ∀ n → R.fromℤ n ≡ fst φ n
+  isUniqueFromℤOCR = isUniqueFromℤ ∘ OrderedCommRingHom→CommRingHom
+
+  isUniqueFromℤOCRMono : (φ : OrderedCommRingMono ℤOrderedCommRing R)
+                       → ∀ n → R.fromℤ n ≡ fst φ n
+  isUniqueFromℤOCRMono = isUniqueFromℤ ∘ OrderedCommRingMono→CommRingHom
+
+  isContrHom[ℤOCR,-] : isContr (OrderedCommRingHom ℤOrderedCommRing R)
+  fst isContrHom[ℤOCR,-] = fromℤOCR
+  snd isContrHom[ℤOCR,-] = OrderedCommRingHom≡ ∘ funExt ∘ isUniqueFromℤOCR
+
+  isContrMono[ℤOCR,-] : isContr (OrderedCommRingMono ℤOrderedCommRing R)
+  fst isContrMono[ℤOCR,-] = fromℤOCRMono
+  snd isContrMono[ℤOCR,-] = OrderedCommRingMono≡ ∘ funExt ∘ isUniqueFromℤOCRMono