Skip to content

Commit ef5ab32

Browse files
felixwellenfelixwellen
committed
terminal R-algebra is fp, notation
1 parent 667057b commit ef5ab32

File tree

8 files changed

+61
-72
lines changed

8 files changed

+61
-72
lines changed

‎Cubical/Algebra/CommAlgebra/FP/Base.agda‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ open import Cubical.Foundations.Isomorphism
77
open import Cubical.Foundations.Function
88
open import Cubical.Foundations.HLevels
99
open import Cubical.Foundations.Structure
10+
open import Cubical.Foundations.Powerset
1011

1112
open import Cubical.Data.FinData
1213
open import Cubical.Data.Nat
@@ -21,6 +22,7 @@ open import Cubical.Algebra.CommAlgebra.Polynomials
2122
open import Cubical.Algebra.CommAlgebra.QuotientAlgebra
2223
open import Cubical.Algebra.CommAlgebra.Ideal
2324
open import Cubical.Algebra.CommAlgebra.FGIdeal
25+
open import Cubical.Algebra.CommAlgebra.Notation
2426

2527

2628
private
@@ -48,13 +50,17 @@ module _ (R : CommRing ℓ) where
4850
opaque
4951
fpAlg : CommAlgebra R ℓ
5052
fpAlg = Polynomials n / fgIdeal
53+
open InstancesForCAlg fpAlg
5154

5255
π : CommAlgebraHom (Polynomials n) fpAlg
5356
π = quotientHom (Polynomials n) fgIdeal
5457

5558
generator : (i : Fin n) → ⟨ fpAlg ⟩ₐ
5659
generator = ⟨ π ⟩ₐ→ ∘ var
5760

61+
fgIdealZero : (x : ⟨ Polynomials n ⟩ₐ) → x ∈ fst fgIdeal → π $ca x ≡ 0r
62+
fgIdealZero x x∈I = isZeroFromIdeal {A = Polynomials n} {I = fgIdeal} x x∈I
63+
5864
computeGenerator : (i : Fin n) → π $ca (var i) ≡ generator i
5965
computeGenerator i = refl
6066

‎Cubical/Algebra/CommAlgebra/FP/Instances.agda‎

Lines changed: 15 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -33,8 +33,8 @@ open import Cubical.Algebra.CommAlgebra.QuotientAlgebra as Quot
3333
open import Cubical.Algebra.CommAlgebra.Ideal using (IdealsIn; 0Ideal)
3434
open import Cubical.Algebra.CommAlgebra.FGIdeal
3535
open import Cubical.Algebra.CommAlgebra.Instances.Initial
36-
open import Cubical.Algebra.CommAlgebra.Instances.Unit
37-
import Cubical.Algebra.CommAlgebra.Notation as CAlgNotation
36+
open import Cubical.Algebra.CommAlgebra.Instances.Terminal
37+
open import Cubical.Algebra.CommAlgebra.Notation
3838

3939
open import Cubical.Algebra.CommAlgebra.FP as FP
4040

@@ -104,33 +104,27 @@ module _ (R : CommRing ℓ) where
104104
private
105105
unitGen : FinVec ⟨ R[⊥] ⟩ₐ 1
106106
unitGen zero = 1r
107-
where open CAlgNotation R[⊥]
107+
where open InstancesForCAlg R[⊥]
108108

109109
terminalCAlgFP : FinitePresentation R
110110
terminalCAlgFP = record { n = 0 ; m = 1 ; relations = unitGen }
111111

112112
R[⊥]/⟨1⟩ : CommAlgebra R ℓ
113113
R[⊥]/⟨1⟩ = fpAlg terminalCAlgFP
114114

115-
terminalCAlgIsFP : isFP R (terminalCAlg R)
116-
terminalCAlgIsFP = ?
117-
{-
118-
119-
private
120-
unitGen : FinVec (fst R[⊥]) 1
121-
unitGen zero = 1a
122-
where open CommAlgebraStr (snd R[⊥])
123-
124-
R[⊥]/⟨1⟩ : CommAlgebra R ℓ
125-
R[⊥]/⟨1⟩ = FPAlgebra 0 unitGen
126-
127-
terminalCAlgFP : FinitePresentation (TerminalCAlg R)
128-
n terminalCAlgFP = 0
129-
m terminalCAlgFP = 1
130-
relations terminalCAlgFP = unitGen
131-
equiv terminalCAlgFP = equivFrom1≡0 R R[⊥]/⟨1⟩ (sym (⋆IdL 1a) ∙ relationsHold 0 unitGen zero)
132-
where open CommAlgebraStr (snd R[⊥]/⟨1⟩)
115+
opaque
116+
unfolding fpAlg fgIdeal
117+
terminalCAlgIsFP : isFP R (terminalCAlg R)
118+
terminalCAlgIsFP = ∣ (terminalCAlgFP ,
119+
(equivFrom1≡0 R R[⊥]/⟨1⟩
120+
(1r ≡⟨ sym pres1 ⟩
121+
(π terminalCAlgFP) $ca 1r ≡⟨ isZeroFromIdeal 1r (incInIdeal (Polynomials R 0) unitGen zero) ⟩
122+
0r ∎))) ∣₁
123+
where open InstancesForCAlg (fpAlg terminalCAlgFP)
124+
open InstancesForCAlg (Polynomials R 0)
125+
open IsCommAlgebraHom (π terminalCAlgFP .snd)
133126

127+
{-
134128
135129
{-
136130
Quotients of the base ring by finitely generated ideals are finitely presented.

‎Cubical/Algebra/CommAlgebra/FP/Properties.agda‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -25,16 +25,16 @@ open import Cubical.Algebra.CommAlgebra.Ideal
2525
open import Cubical.Algebra.CommAlgebra.FGIdeal
2626
open import Cubical.Algebra.CommAlgebra.Kernel
2727
open import Cubical.Algebra.CommAlgebra.FP.Base
28+
open import Cubical.Algebra.CommAlgebra.Notation
2829
import Cubical.Algebra.CommAlgebra.Polynomials as Poly
2930
import Cubical.Algebra.CommAlgebra.QuotientAlgebra as Quot
30-
import Cubical.Algebra.CommAlgebra.Notation as AlgNotation
3131

3232
private variable
3333
ℓ ℓ' : Level
3434

3535
module _ (R : CommRing ℓ) (fp : FinitePresentation R) (A : CommAlgebra R ℓ) where
3636
open FinitePresentation fp
37-
open AlgNotation A
37+
open InstancesForCAlg A
3838

3939
module _ (φ : FinVec ⟨ A ⟩ₐ n) (p : (i : Fin m) → Poly.inducedHom A φ $ca relations i ≡ 0r) where
4040
opaque

‎Cubical/Algebra/CommAlgebra/Instances/Initial.agda‎

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -18,9 +18,8 @@ import Cubical.Algebra.Algebra.Properties
1818

1919
open AlgebraHoms
2020

21-
private
22-
variable
23-
ℓ : Level
21+
private variable
22+
ℓ : Level
2423

2524
module _ (R : CommRing ℓ) where
2625
module _ where

‎Cubical/Algebra/CommAlgebra/Instances/Terminal.agda‎

Lines changed: 22 additions & 33 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,9 @@
11
{-# OPTIONS --safe #-}
2-
module Cubical.Algebra.CommAlgebra.Instances.Unit where
2+
{-
3+
Define terminal R-algebra as a commutative algebra and prove the universal property.
4+
The universe level of the terminal R-algebra is fixed to be the universe level of R.
5+
-}
6+
module Cubical.Algebra.CommAlgebra.Instances.Terminal where
37

48
open import Cubical.Foundations.Prelude
59
open import Cubical.Foundations.Function
@@ -12,7 +16,7 @@ open import Cubical.Data.Sigma.Properties using (Σ≡Prop)
1216
open import Cubical.Algebra.CommRing
1317
open import Cubical.Algebra.CommAlgebra.Base
1418
open import Cubical.Algebra.CommRing.Instances.Unit
15-
import Cubical.Algebra.CommAlgebra.Notation as CAlgNotation
19+
open import Cubical.Algebra.CommAlgebra.Notation
1620

1721
open import Cubical.Tactics.CommRingSolver
1822

@@ -21,44 +25,29 @@ private
2125
ℓ ℓ' ℓ'' : Level
2226

2327
module _ (R : CommRing ℓ) where
24-
terminalCAlg : CommAlgebra R ℓ'
28+
terminalCAlg : CommAlgebra R ℓ
2529
terminalCAlg = UnitCommRing , mapToUnitCommRing R
2630

2731
module _ (A : CommAlgebra R ℓ'') where
28-
terminalMap : CommAlgebraHom A (terminalCAlg {ℓ' = ℓ})
32+
terminalMap : CommAlgebraHom A terminalCAlg
2933
terminalMap = CommRingHom→CommAlgebraHom (mapToUnitCommRing (A .fst)) $ isPropMapToUnitCommRing _ _ _
3034

3135
module _ (A : CommAlgebra R ℓ'') where
32-
terminalityContr : isContr (CommAlgebraHom A (terminalCAlg {ℓ' = ℓ}))
36+
terminalityContr : isContr (CommAlgebraHom A terminalCAlg)
3337
terminalityContr = (terminalMap A) , λ f → CommAlgebraHom≡ (funExt (λ _ → refl))
3438

35-
{-
39+
isContr→EquivTerminal : isContr ⟨ A ⟩ₐ → CommAlgebraEquiv A terminalCAlg
40+
isContr→EquivTerminal isContrA =
41+
(isContr→≃Unit* isContrA) ,
42+
record { isCommRingHom = mapToUnitCommRing (A .fst) .snd ;
43+
commutes = CommRingHom≡ (funExt (λ _ → refl)) }
3644

37-
open CAlgNotation A
38-
equivFrom1≡0 : (1≡0 : 1r ≡ 0r)
45+
open InstancesForCAlg A
46+
equivFrom1≡0 : 1r ≡ (0r :> ⟨ A ⟩ₐ)
3947
→ CommAlgebraEquiv A terminalCAlg
40-
equivFrom1≡0 = ?
41-
42-
module _ (A : CommAlgebra R ℓ) where
43-
44-
terminalityContr : isContr (CommAlgebraHom A UnitCommAlgebra)
45-
terminalityContr = terminalMap , path
46-
where path : (ϕ : CommAlgebraHom A UnitCommAlgebra) → terminalMap ≡ ϕ
47-
path ϕ = Σ≡Prop (isPropIsCommAlgebraHom {M = A} {N = UnitCommAlgebra})
48-
λ i _ → isPropUnit* _ _ i
49-
50-
open CommAlgebraStr (snd A)
51-
module _ (1≡0 : 1a ≡ 0a) where
52-
53-
1≡0→isContr : isContr ⟨ A ⟩
54-
1≡0→isContr = 0a , λ a →
55-
0a ≡⟨ solve! S ⟩
56-
a · 0a ≡⟨ cong (λ b → a · b) (sym 1≡0) ⟩
57-
a · 1a ≡⟨ solve! S ⟩
58-
a ∎
59-
where S = CommAlgebra→CommRing A
60-
61-
equivFrom1≡0 : CommAlgebraEquiv A UnitCommAlgebra
62-
equivFrom1≡0 = isContr→Equiv 1≡0→isContr isContrUnit* ,
63-
snd terminalMap
64-
-}
48+
equivFrom1≡0 1≡0 = isContr→EquivTerminal (0r , λ x →
49+
0r ≡⟨ solve! A' ⟩
50+
0r · x ≡⟨ cong (λ u → u · x) (sym 1≡0) ⟩
51+
1r · x ≡⟨ solve! A' ⟩
52+
x ∎)
53+
where A' = CommAlgebra→CommRing A

‎Cubical/Algebra/CommAlgebra/Notation.agda‎

Lines changed: 10 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -9,15 +9,17 @@ open import Cubical.Foundations.Structure
99
open import Cubical.Algebra.CommRing.Base
1010
open import Cubical.Algebra.CommAlgebra.Base
1111

12-
module Cubical.Algebra.CommAlgebra.Notation {ℓ ℓ' : Level} {R : CommRing ℓ} (A : CommAlgebra R ℓ') where
12+
module Cubical.Algebra.CommAlgebra.Notation where
1313

1414
open CommAlgebraStr ⦃...⦄ public
1515
open CommRingStr ⦃...⦄ public
1616

17-
instance
18-
baseRingStr : CommRingStr ⟨ R ⟩
19-
baseRingStr = R .snd
20-
ringStrOnAlg : CommRingStr ⟨ A ⟩ₐ
21-
ringStrOnAlg = CommAlgebra→CommRingStr A
22-
algStr : CommAlgebraStr ⟨ A ⟩ₐ
23-
algStr = CommAlgebra→CommAlgebraStr A
17+
module InstancesForCAlg {ℓ ℓ' : Level} {R : CommRing ℓ} (A : CommAlgebra R ℓ') where
18+
19+
instance
20+
baseRingStr : CommRingStr ⟨ R ⟩
21+
baseRingStr = R .snd
22+
ringStrOnAlg : CommRingStr ⟨ A ⟩ₐ
23+
ringStrOnAlg = CommAlgebra→CommRingStr A
24+
algStr : CommAlgebraStr ⟨ A ⟩ₐ
25+
algStr = CommAlgebra→CommAlgebraStr A

‎Cubical/Algebra/CommAlgebra/Properties.agda‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@ open import Cubical.Data.Sigma
1212
open import Cubical.Algebra.CommRing
1313
open import Cubical.Algebra.CommAlgebra.Base
1414
open import Cubical.Algebra.CommAlgebra.Univalence
15+
open import Cubical.Algebra.CommAlgebra.Notation
1516

1617
private
1718
variable
@@ -55,8 +56,6 @@ module _
5556
{f : ⟨ A ⟩ₐ → ⟨ B ⟩ₐ}
5657
where
5758

58-
open CommAlgebraStr ⦃...⦄
59-
open CommRingStr ⦃...⦄
6059
private instance
6160
_ = CommAlgebra→CommRingStr A
6261
_ = CommAlgebra→CommRingStr B

‎Cubical/Algebra/CommAlgebra/QuotientAlgebra.agda‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@ open import Cubical.Algebra.CommRing.Ideal hiding (IdealsIn)
1818
open import Cubical.Algebra.CommAlgebra.Base
1919
open import Cubical.Algebra.CommAlgebra.Ideal
2020
open import Cubical.Algebra.CommAlgebra.Kernel
21-
open import Cubical.Algebra.CommAlgebra.Instances.Unit
21+
open import Cubical.Algebra.CommAlgebra.Instances.Terminal
2222
open import Cubical.Algebra.Ring
2323
open import Cubical.Tactics.CommRingSolver
2424

@@ -120,7 +120,7 @@ module _ {R : CommRing ℓ} (A : CommAlgebra R ℓ') (I : IdealsIn R A) where
120120
module _ {R : CommRing ℓ} (A : CommAlgebra R ℓ) where
121121
open CommRingStr (A .fst .snd)
122122

123-
oneIdealQuotient : CommAlgebraEquiv (A / (1Ideal R A)) (UnitCommAlgebra R {ℓ' = ℓ})
123+
oneIdealQuotient : CommAlgebraEquiv (A / (1Ideal R A)) (terminalCAlg R)
124124
oneIdealQuotient .fst =
125125
(withOpaqueStr $
126126
isoToEquiv (iso ⟨ terminalMap R (A / 1Ideal R A) ⟩ₐ→
@@ -171,5 +171,5 @@ module _
171171
_ = (A / I).fst .snd
172172

173173
opaque
174-
isZeroFromIdeal : (x : ⟨ A ⟩ₐ) → x ∈ (fst I) → ⟨ quotientHom A I ⟩ₐ→ x ≡ 0r
174+
isZeroFromIdeal : (x : ⟨ A ⟩ₐ) → x ∈ (fst I) → quotientHom A I $ca x ≡ 0r
175175
isZeroFromIdeal x x∈I = eq/ x 0r (subst (_∈ fst I) (solve! (CommAlgebra→CommRing A)) x∈I )

0 commit comments

Comments
 (0)