Merge branch 'agda:master' into oriented-graded-posets

Author: anshwad10

Cubical/Algebra/BooleanRing/Base.agda

@@ -8,7 +8,7 @@ open import Cubical.Algebra.Ring
 open import Cubical.Algebra.AbGroup.Base
 open import Cubical.Algebra.CommRing
 open import Cubical.Tactics.CommRingSolver
-
+open RingTheory
 
 private
   variable
@@ -48,6 +48,12 @@ BooleanStr→CommRingStr x = record { isCommRing = IsBooleanRing.isCommRing (Boo
 BooleanRing→CommRing : BooleanRing ℓ → CommRing ℓ
 BooleanRing→CommRing (carrier , structure ) = carrier , BooleanStr→CommRingStr structure
 
+BooleanStr→RingStr : { A : Type ℓ } → BooleanStr A → RingStr A
+BooleanStr→RingStr S = CommRingStr→RingStr (BooleanStr→CommRingStr S)
+
+BooleanRing→Ring : BooleanRing ℓ → Ring ℓ
+BooleanRing→Ring (carrier , structure ) = carrier , BooleanStr→RingStr structure
+
 module BooleanAlgebraStr (A : BooleanRing ℓ)  where
   open BooleanStr (A . snd)
   _∨_ : ⟨ A ⟩ → ⟨ A ⟩ → ⟨ A ⟩
@@ -96,8 +102,8 @@ module BooleanAlgebraStr (A : BooleanRing ℓ)  where
   ∧AnnihilL : 𝟘 ∧ x ≡ 𝟘
   ∧AnnihilL = RingTheory.0LeftAnnihilates (CommRing→Ring (BooleanRing→CommRing A)) _
 
-  -IsId : x + x ≡ 𝟘
-  -IsId {x = x} =  RingTheory.+Idempotency→0 (CommRing→Ring (BooleanRing→CommRing A)) (x + x) 2x≡4x
+  characteristic2 : x + x ≡ 𝟘
+  characteristic2 {x = x} =  RingTheory.+Idempotency→0 (CommRing→Ring (BooleanRing→CommRing A)) (x + x) 2x≡4x
     where
       2x≡4x : x + x ≡ (x + x) + (x + x)
       2x≡4x =
@@ -109,10 +115,13 @@ module BooleanAlgebraStr (A : BooleanRing ℓ)  where
           ≡⟨ cong₂ _+_ (cong₂ _+_ (·Idem x) (·Idem x)) (cong₂ _+_ (·Idem x) (·Idem x)) ⟩
         (x + x) + (x + x) ∎
 
+  -IsId : x ≡ - x
+  -IsId {x = x} = implicitInverse (BooleanRing→Ring A) x x characteristic2
+
   ∨Idem   : x ∨ x ≡ x
   ∨Idem { x = x } =
     x + x + x · x
-      ≡⟨ cong (λ y → y + x · x) -IsId ⟩
+      ≡⟨ cong (λ y → y + x · x) characteristic2 ⟩
     𝟘  + x · x
       ≡⟨ +IdL (x · x) ⟩
     x · x
@@ -124,7 +133,7 @@ module BooleanAlgebraStr (A : BooleanRing ℓ)  where
     (x + 𝟙) + (x · 𝟙)
       ≡⟨ solve! (BooleanRing→CommRing A) ⟩
     𝟙 + (x + x)
-      ≡⟨ cong (λ y → 𝟙 + y) -IsId ⟩
+      ≡⟨ cong (λ y → 𝟙 + y) characteristic2 ⟩
     𝟙 + 𝟘
       ≡⟨ +IdR 𝟙 ⟩
     𝟙 ∎
@@ -152,7 +161,7 @@ module BooleanAlgebraStr (A : BooleanRing ℓ)  where
     x + 𝟘 + 𝟘 + y · z + 𝟘 + x · y · z
       ≡⟨ cong (λ a → a + 𝟘 + 𝟘 + y · z + 𝟘 + a · y · z) (sym (·Idem x)) ⟩
     x · x + 𝟘  + 𝟘  + y · z + 𝟘 + x · x · y · z
-      ≡⟨ cong (λ a → x · x + 𝟘 + 𝟘 + y · z + a + x · x · y · z) (sym (-IsId {x = (x · y) · z})) ⟩
+      ≡⟨ cong (λ a → x · x + 𝟘 + 𝟘 + y · z + a + x · x · y · z) (sym (characteristic2 {x = (x · y) · z})) ⟩
     x · x + 𝟘 + 𝟘 + y · z + (x · y · z + x · y · z) + x · x · y · z
       ≡⟨ (cong₂ (λ a b → x · x + a + b + y · z + (x · y · z + x · y · z) + x · x · y · z)) (xa-xxa≡0 z) (xa-xxa≡0 y) ⟩
     x · x + (x · z + x · x · z) + (x · y + x · x · y) + y · z + (x · y · z + x · y · z) + x · x · y · z
@@ -163,7 +172,7 @@ module BooleanAlgebraStr (A : BooleanRing ℓ)  where
       xa-xxa≡0 : (a : ⟨ A ⟩) → 𝟘 ≡ x · a + x · x · a
       xa-xxa≡0 a =
        𝟘
-         ≡⟨ sym -IsId ⟩
+         ≡⟨ sym characteristic2 ⟩
        x · a + x · a
          ≡⟨ cong (λ y → x · a + y · a) (sym (·Idem x)) ⟩
        x · a + x · x · a ∎
@@ -178,7 +187,7 @@ module BooleanAlgebraStr (A : BooleanRing ℓ)  where
     x · x + (x · y + x · x · y)
       ≡⟨ cong (λ z → z + ((x · y) + (z · y))) (·Idem x) ⟩
     x + (x · y + x · y)
-      ≡⟨ cong (_+_ x) -IsId ⟩
+      ≡⟨ cong (_+_ x) characteristic2 ⟩
     x + 𝟘
       ≡⟨ +IdR x ⟩
     x ∎
@@ -190,7 +199,7 @@ module BooleanAlgebraStr (A : BooleanRing ℓ)  where
     x + (x · y + x · x · y)
       ≡⟨ cong (λ z → x + (x · y + z · y)) (·Idem x) ⟩
     x + (x · y + x · y)
-      ≡⟨ cong (_+_ x) -IsId ⟩
+      ≡⟨ cong (_+_ x) characteristic2 ⟩
     x + 𝟘
       ≡⟨ +IdR x ⟩
     x ∎
@@ -202,7 +211,7 @@ module BooleanAlgebraStr (A : BooleanRing ℓ)  where
     x + x · x
       ≡⟨ cong (λ y → x + y) (·Idem x) ⟩
     x + x
-      ≡⟨ -IsId ⟩
+      ≡⟨ characteristic2 ⟩
     𝟘 ∎
 
   ¬Cancels∧L : ¬ x ∧ x ≡ 𝟘
@@ -226,7 +235,7 @@ module BooleanAlgebraStr (A : BooleanRing ℓ)  where
     𝟙 + (𝟙 + x)
       ≡⟨ +Assoc 𝟙 𝟙 x ⟩
     (𝟙 + 𝟙) + x
-      ≡⟨ cong (λ y → y + x) ( -IsId {x = 𝟙}) ⟩
+      ≡⟨ cong (λ y → y + x) ( characteristic2 {x = 𝟙}) ⟩
     𝟘 + x
       ≡⟨ +IdL x ⟩
     x ∎
@@ -235,7 +244,7 @@ module BooleanAlgebraStr (A : BooleanRing ℓ)  where
   ¬0≡1 = +IdR 𝟙
 
   ¬1≡0 : ¬ 𝟙 ≡ 𝟘
-  ¬1≡0 = -IsId {x = 𝟙}
+  ¬1≡0 = characteristic2 {x = 𝟙}
 
   DeMorgan¬∨ : ¬ (x ∨ y) ≡ ¬ x ∧ ¬ y
   DeMorgan¬∨ = solve! (BooleanRing→CommRing A)
@@ -245,7 +254,7 @@ module BooleanAlgebraStr (A : BooleanRing ℓ)  where
     𝟙 + x · y
       ≡⟨ solve! (BooleanRing→CommRing A) ⟩
     𝟘 + 𝟘 + 𝟙 + x · y
-      ≡⟨ cong₂ (λ a b → ((a + b) + 𝟙) + (x · y)) (sym (-IsId {x = 𝟙 + x})) (sym (-IsId {x = y})) ⟩
+      ≡⟨ cong₂ (λ a b → ((a + b) + 𝟙) + (x · y)) (sym (characteristic2 {x = 𝟙 + x})) (sym (characteristic2 {x = y})) ⟩
     ((𝟙 + x)  + (𝟙 + x)) + (y + y)  + 𝟙 + x · y
       ≡⟨ solve! (BooleanRing→CommRing A) ⟩
     ¬ x ∨ ¬ y ∎

Cubical/Algebra/CommAlgebra/UnivariatePolyList.agda

@@ -221,11 +221,11 @@ module _ (R : CommRing ℓ) where
 
 
     {- Reforumlation in terms of the R-AlgebraHom from R[X] to A -}
-    indcuedHomEquivalence : AlgebraHom (CommAlgebra→Algebra ListPolyCommAlgebra) A ≃ ⟨ A ⟩
-    fst indcuedHomEquivalence f = fst f X
-    fst (fst (equiv-proof (snd indcuedHomEquivalence) x)) = inducedHom x
-    snd (fst (equiv-proof (snd indcuedHomEquivalence) x)) = inducedMapGenerator x
-    snd (equiv-proof (snd indcuedHomEquivalence) x) (g , gX≡x) =
+    inducedHomEquivalence : AlgebraHom (CommAlgebra→Algebra ListPolyCommAlgebra) A ≃ ⟨ A ⟩
+    fst inducedHomEquivalence f = fst f X
+    fst (fst (equiv-proof (snd inducedHomEquivalence) x)) = inducedHom x
+    snd (fst (equiv-proof (snd inducedHomEquivalence) x)) = inducedMapGenerator x
+    snd (equiv-proof (snd inducedHomEquivalence) x) (g , gX≡x) =
       Σ≡Prop (λ _ → is-set _ _) (sym (inducedHomUnique x g gX≡x))
 
     equalByUMP : (f g : AlgebraHom (CommAlgebra→Algebra ListPolyCommAlgebra) A)

Cubical/Algebra/CommRing/Ideal/Base.agda

@@ -89,6 +89,12 @@ module CommIdeal (R' : CommRing ℓ) where
  ∑Closed I {n = zero} _ _ = I .snd .contains0
  ∑Closed I {n = suc n} V h = I .snd .+Closed (h zero) (∑Closed I (V ∘ suc) (h ∘ suc))
 
+ open Exponentiation R'
+
+ ^sucClosed : (I : CommIdeal) (x : R) {n : ℕ}
+            → x ∈ I → x ^ suc n ∈ I
+ ^sucClosed I x x∈I = subst-∈ I (·Comm _ x) (·Closed (snd I) _ x∈I)
+
  0Ideal : CommIdeal
  fst 0Ideal x = (x ≡ 0r) , is-set _ _
  +Closed (snd 0Ideal) x≡0 y≡0 = cong₂ (_+_) x≡0 y≡0 ∙ +IdR _

Cubical/Algebra/CommRing/Ideal/Sum.agda

@@ -156,6 +156,9 @@ module IdealSum (R' : CommRing ℓ) where
  ·iComm⊆ I J x = map λ (n , (α , β) , ∀αi∈I , ∀βi∈J , x≡∑αβ)
                       → (n , (β , α) , ∀βi∈J , ∀αi∈I , x≡∑αβ ∙ ∑Ext (λ i → ·Comm (α i) (β i)))
 
+ ·iRincl : ∀ (I J : CommIdeal) → (I ·i J) ⊆ J
+ ·iRincl I J x x∈IJ = ·iLincl J I x (·iComm⊆ I J x x∈IJ)
+
  ·iComm : ∀ (I J : CommIdeal) → I ·i J ≡ J ·i I
  ·iComm I J = CommIdeal≡Char (·iComm⊆ I J) (·iComm⊆ J I)
 

Cubical/Algebra/CommRing/RadicalIdeal.agda

@@ -99,8 +99,12 @@ module RadicalIdeal (R' : CommRing ℓ) where
  1∈√→1∈ : ∀ (I : CommIdeal) → 1r ∈ √ I → 1r ∈ I
  1∈√→1∈ I = PT.rec (∈-isProp (fst I) _) λ (n , 1ⁿ∈I) → subst-∈ I (1ⁿ≡1 n) 1ⁿ∈I
 
+ √Resp⊆ : (I J : CommIdeal) → I ⊆ J → √ I ⊆ √ J
+ √Resp⊆ I J I⊆J x = map (map-snd λ {a} → I⊆J (x ^ a))
+
  -- important lemma for characterization of the Zariski lattice
  open KroneckerDelta (CommRing→Ring R')
+
  √FGIdealCharLImpl : {n : ℕ} (V : FinVec R n) (I : CommIdeal)
          → √ ⟨ V ⟩[ R' ] ⊆ √ I → (∀ i → V i ∈ √ I)
  √FGIdealCharLImpl V I √⟨V⟩⊆√I i = √⟨V⟩⊆√I _ (∈→∈√ ⟨ V ⟩[ R' ] (V i)
@@ -234,3 +238,10 @@ module RadicalIdeal (R' : CommRing ℓ) where
 
  √·Absorb+ : ∀ (I J : CommIdeal) → √ (I ·i (I +i J)) ≡ √ I
  √·Absorb+ I J = CommIdeal≡Char (√·Absorb+LIncl I J) (√·Absorb+RIncl I J)
+
+ √·ContrLIncl : ∀ (I J : CommIdeal) → √ (√ I ·i √ J) ⊆ √ (I ·i J)
+ √·ContrLIncl I J x = √·RContrLIncl I J x ∘ subst (x ∈_) (√·LContr I (√ J))
+
+ √Pres·LIncl : ∀ (I J : CommIdeal) → (√ I ·i √ J) ⊆ √ (I ·i J)
+ √Pres·LIncl I J x = √·ContrLIncl I J x ∘ ∈→∈√ (√ I ·i √ J) x
+

Cubical/Algebra/SymmetricGroup.agda

@@ -4,23 +4,87 @@ module Cubical.Algebra.SymmetricGroup where
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Univalence
+open import Cubical.Foundations.Structure
 open import Cubical.Data.Sigma
-open import Cubical.Data.Nat using (ℕ ; suc ; zero)
-open import Cubical.Data.Fin using (Fin ; isSetFin)
-open import Cubical.Data.Empty
-open import Cubical.Relation.Nullary using (¬_)
+open import Cubical.Data.Nat
+open import Cubical.Data.SumFin
+open import Cubical.Data.Empty as Empty
+open import Cubical.Data.Bool
+open import Cubical.Data.Unit
 
 open import Cubical.Algebra.Group
+open import Cubical.Algebra.Group.Morphisms
+open import Cubical.Algebra.Group.MorphismProperties
+open import Cubical.Algebra.Group.GroupPath
+open import Cubical.Algebra.Group.Instances.Bool
+open import Cubical.Algebra.Group.Instances.Unit
 
-private
-  variable
-    ℓ : Level
+private variable
+  ℓ ℓ' : Level
+  X Y : Type ℓ
 
-Symmetric-Group : (X : Type ℓ) → isSet X → Group ℓ
-Symmetric-Group X isSetX = makeGroup (idEquiv X) compEquiv invEquiv (isOfHLevel≃ 2 isSetX isSetX)
-  compEquiv-assoc compEquivEquivId compEquivIdEquiv invEquiv-is-rinv invEquiv-is-linv
+SymGroup : (X : Type ℓ) → isSet X → Group ℓ
+SymGroup X isSetX = makeGroup {G = X ≃ X} (idEquiv X) compEquiv invEquiv
+  (isOfHLevel≃ 2 isSetX isSetX)
+  compEquiv-assoc
+  compEquivEquivId
+  compEquivIdEquiv
+  invEquiv-is-rinv
+  invEquiv-is-linv
 
--- Finite symmetrics groups
+FinSymGroup : ℕ → Group₀
+FinSymGroup n = SymGroup (Fin n) isSetFin
 
-Sym : ℕ → Group _
-Sym n = Symmetric-Group (Fin n) isSetFin
+Sym0≃1 : GroupEquiv (FinSymGroup 0) UnitGroup₀
+Sym0≃1 = contrGroupEquivUnit $ inhProp→isContr (idEquiv _) $ isOfHLevel≃ 1 isProp⊥ isProp⊥
+
+Sym0≡1 : FinSymGroup 0 ≡ UnitGroup₀
+Sym0≡1 = uaGroup Sym0≃1
+
+Sym1≃1 : GroupEquiv (FinSymGroup 1) UnitGroup₀
+Sym1≃1 = contrGroupEquivUnit $ isOfHLevel≃ 0 isContrSumFin1 isContrSumFin1
+
+Sym1≡1 : FinSymGroup 1 ≡ UnitGroup₀
+Sym1≡1 = uaGroup Sym1≃1
+
+Sym2≃Bool : GroupEquiv (FinSymGroup 2) BoolGroup
+Sym2≃Bool = GroupIso→GroupEquiv $ invGroupIso $ ≅Bool $
+  Fin 2 ≃ Fin 2 Iso⟨ equivCompIso SumFin2≃Bool SumFin2≃Bool ⟩
+  Bool ≃ Bool   Iso⟨ invIso univalenceIso ⟩
+  Bool ≡ Bool   Iso⟨ invIso reflectIso ⟩
+  Bool          ∎Iso
+  where open BoolReflection
+
+Sym2≡Bool : FinSymGroup 2 ≡ BoolGroup
+Sym2≡Bool = uaGroup Sym2≃Bool
+
+SymUnit≃Unit : GroupEquiv (SymGroup Unit isSetUnit) UnitGroup₀
+SymUnit≃Unit = contrGroupEquivUnit $ isOfHLevel≃ 0 isContrUnit isContrUnit
+
+SymUnit≡Unit : SymGroup Unit isSetUnit ≡ UnitGroup₀
+SymUnit≡Unit = uaGroup SymUnit≃Unit
+
+SymBool≃Bool : GroupEquiv (SymGroup Bool isSetBool) BoolGroup
+SymBool≃Bool = GroupIso→GroupEquiv $ invGroupIso $ ≅Bool $
+  Bool ≃ Bool Iso⟨ invIso univalenceIso ⟩
+  Bool ≡ Bool Iso⟨ invIso reflectIso ⟩
+  Bool        ∎Iso
+  where open BoolReflection
+
+SymBool≡Bool : SymGroup Bool isSetBool ≡ BoolGroup
+SymBool≡Bool = uaGroup SymBool≃Bool
+
+module _ (n : ℕ) where
+
+  ⟨Sym⟩≃factorial : ⟨ FinSymGroup n ⟩ ≃ Fin (n !)
+  ⟨Sym⟩≃factorial = SumFin≃≃ n
+
+  ⟨Sym⟩≡factorial : ⟨ FinSymGroup n ⟩ ≡ Fin (n !)
+  ⟨Sym⟩≡factorial = ua ⟨Sym⟩≃factorial
+
+Sym-cong-≃ : ∀ isSetX isSetY → X ≃ Y → GroupEquiv (SymGroup X isSetX) (SymGroup Y isSetY)
+Sym-cong-≃ isSetX isSetY e .fst = equivComp e e
+Sym-cong-≃ isSetX isSetY e .snd = makeIsGroupHom λ g h → sym $ equivEq $ funExt λ x → cong (e .fst ∘ h .fst) (retEq e _)