Skip to content

Commit 68cfbac

Browse files
lowasserlowasser
authored
Subalgebras of unital associative algebras (#1937)
This is setting up for the algebras of continuous, uniformly continuous, and differentiable real functions.
1 parent 5759a76 commit 68cfbac

6 files changed

Lines changed: 597 additions & 0 deletions

‎src/commutative-algebra.lagda.md‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ module commutative-algebra where
77
88
open import commutative-algebra.algebras-commutative-rings public
99
open import commutative-algebra.associative-algebras-commutative-rings public
10+
open import commutative-algebra.associative-subalgebras-commutative-rings public
1011
open import commutative-algebra.binomial-theorem-commutative-rings public
1112
open import commutative-algebra.binomial-theorem-commutative-semirings public
1213
open import commutative-algebra.boolean-rings public
@@ -77,8 +78,10 @@ open import commutative-algebra.radical-ideals-generated-by-subsets-commutative-
7778
open import commutative-algebra.radicals-of-ideals-commutative-rings public
7879
open import commutative-algebra.subalgebras-commutative-rings public
7980
open import commutative-algebra.subsets-algebras-commutative-rings public
81+
open import commutative-algebra.subsets-associative-algebras-commutative-rings public
8082
open import commutative-algebra.subsets-commutative-rings public
8183
open import commutative-algebra.subsets-commutative-semirings public
84+
open import commutative-algebra.subsets-unital-associative-algebras-commutative-rings public
8285
open import commutative-algebra.sums-of-finite-families-of-elements-commutative-rings public
8386
open import commutative-algebra.sums-of-finite-families-of-elements-commutative-semirings public
8487
open import commutative-algebra.sums-of-finite-sequences-of-elements-commutative-rings public
@@ -87,6 +90,7 @@ open import commutative-algebra.transporting-commutative-ring-structure-isomorph
8790
open import commutative-algebra.trivial-commutative-rings public
8891
open import commutative-algebra.unital-algebras-commutative-rings public
8992
open import commutative-algebra.unital-associative-algebras-commutative-rings public
93+
open import commutative-algebra.unital-associative-subalgebras-commutative-rings public
9094
open import commutative-algebra.zariski-locale public
9195
open import commutative-algebra.zariski-topology public
9296
```

‎src/commutative-algebra/associative-subalgebras-commutative-rings.lagda.md‎

Lines changed: 119 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,119 @@
1+
# Associative subalgebras over commutative rings
2+
3+
```agda
4+
module commutative-algebra.associative-subalgebras-commutative-rings where
5+
```
6+
7+
<details><summary>Imports</summary>
8+
9+
```agda
10+
open import commutative-algebra.algebras-commutative-rings
11+
open import commutative-algebra.associative-algebras-commutative-rings
12+
open import commutative-algebra.commutative-rings
13+
open import commutative-algebra.subalgebras-commutative-rings
14+
open import commutative-algebra.subsets-associative-algebras-commutative-rings
15+
16+
open import foundation.dependent-pair-types
17+
open import foundation.identity-types
18+
open import foundation.subtypes
19+
open import foundation.universe-levels
20+
```
21+
22+
</details>
23+
24+
## Idea
25+
26+
A
27+
[subset](commutative-algebra.subsets-associative-algebras-commutative-rings.md)
28+
of an
29+
[associative algebra](commutative-algebra.associative-algebras-commutative-rings.md)
30+
over a [commutative ring](commutative-algebra.commutative-rings.md) is a
31+
{{#concept "subalgebra" Disambiguation="of an associative algebra" Agda=associative-subalgebra-Commutative-Ring}}
32+
if it contains zero and is closed under addition, scalar multiplication, and
33+
multiplication, in which case it is itself an associative algebra.
34+
35+
## Definition
36+
37+
```agda
38+
module _
39+
{l1 l2 l3 : Level}
40+
(R : Commutative-Ring l1)
41+
(A : associative-algebra-Commutative-Ring l2 R)
42+
where
43+
44+
is-subalgebra-prop-subset-associative-algebra-Commutative-Ring :
45+
subtype (l1 ⊔ l2 ⊔ l3) (subset-associative-algebra-Commutative-Ring l3 R A)
46+
is-subalgebra-prop-subset-associative-algebra-Commutative-Ring =
47+
is-subalgebra-prop-subset-algebra-Commutative-Ring
48+
( R)
49+
( algebra-associative-algebra-Commutative-Ring R A)
50+
51+
is-subalgebra-subset-associative-algebra-Commutative-Ring :
52+
subset-associative-algebra-Commutative-Ring l3 R A → UU (l1 ⊔ l2 ⊔ l3)
53+
is-subalgebra-subset-associative-algebra-Commutative-Ring =
54+
is-in-subtype is-subalgebra-prop-subset-associative-algebra-Commutative-Ring
55+
56+
module _
57+
{l1 l2 : Level}
58+
(l3 : Level)
59+
(R : Commutative-Ring l1)
60+
(A : associative-algebra-Commutative-Ring l2 R)
61+
where
62+
63+
associative-subalgebra-Commutative-Ring : UU (l1 ⊔ l2 ⊔ lsuc l3)
64+
associative-subalgebra-Commutative-Ring =
65+
type-subtype
66+
( is-subalgebra-prop-subset-associative-algebra-Commutative-Ring
67+
{ l3 = l3}
68+
( R)
69+
( A))
70+
71+
module _
72+
{l1 l2 l3 : Level}
73+
(R : Commutative-Ring l1)
74+
(A : associative-algebra-Commutative-Ring l2 R)
75+
(SA@(S , is-subalgebra-S) :
76+
associative-subalgebra-Commutative-Ring l3 R A)
77+
where
78+
79+
algebra-associative-subalgebra-Commutative-Ring :
80+
algebra-Commutative-Ring (l2 ⊔ l3) R
81+
algebra-associative-subalgebra-Commutative-Ring =
82+
algebra-subalgebra-Commutative-Ring
83+
( R)
84+
( algebra-associative-algebra-Commutative-Ring R A)
85+
( SA)
86+
87+
type-associative-subalgebra-Commutative-Ring : UU (l2 ⊔ l3)
88+
type-associative-subalgebra-Commutative-Ring = type-subtype S
89+
90+
mul-algebra-associative-subalgebra-Commutative-Ring :
91+
type-associative-subalgebra-Commutative-Ring →
92+
type-associative-subalgebra-Commutative-Ring →
93+
type-associative-subalgebra-Commutative-Ring
94+
mul-algebra-associative-subalgebra-Commutative-Ring =
95+
mul-algebra-Commutative-Ring
96+
( R)
97+
( algebra-associative-subalgebra-Commutative-Ring)
98+
99+
abstract
100+
associative-mul-algebra-associative-subalgebra-Commutative-Ring :
101+
(a b c : type-associative-subalgebra-Commutative-Ring) →
102+
mul-algebra-associative-subalgebra-Commutative-Ring
103+
( mul-algebra-associative-subalgebra-Commutative-Ring a b)
104+
( c) ＝
105+
mul-algebra-associative-subalgebra-Commutative-Ring
106+
( a)
107+
( mul-algebra-associative-subalgebra-Commutative-Ring b c)
108+
associative-mul-algebra-associative-subalgebra-Commutative-Ring
109+
(a , _) (b , _) (c , _) =
110+
eq-type-subtype
111+
( S)
112+
( associative-mul-associative-algebra-Commutative-Ring R A a b c)
113+
114+
associative-algebra-associative-subalgebra-Commutative-Ring :
115+
associative-algebra-Commutative-Ring (l2 ⊔ l3) R
116+
associative-algebra-associative-subalgebra-Commutative-Ring =
117+
( algebra-associative-subalgebra-Commutative-Ring ,
118+
associative-mul-algebra-associative-subalgebra-Commutative-Ring)
119+
```

‎src/commutative-algebra/subsets-associative-algebras-commutative-rings.lagda.md‎

Lines changed: 134 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,134 @@
1+
# Subsets of associative algebras over commutative rings
2+
3+
```agda
4+
module commutative-algebra.subsets-associative-algebras-commutative-rings where
5+
```
6+
7+
<details><summary>Imports</summary>
8+
9+
```agda
10+
open import commutative-algebra.associative-algebras-commutative-rings
11+
open import commutative-algebra.commutative-rings
12+
open import commutative-algebra.subsets-algebras-commutative-rings
13+
14+
open import foundation.subtypes
15+
open import foundation.universe-levels
16+
```
17+
18+
</details>
19+
20+
## Idea
21+
22+
A
23+
{{#concept "subset" Disambiguation="of an associative algebra over a commutative ring" Agda=subset-associative-algebra-Commutative-Ring}}
24+
of an
25+
[associative algebra](commutative-algebra.associative-algebras-commutative-rings.md)
26+
`A` over a [commutative ring](commutative-algebra.commutative-rings.md) `R` is a
27+
[subset](foundation.subtypes.md) of the underlying type of `A`.
28+
29+
## Definition
30+
31+
```agda
32+
module _
33+
{l1 l2 : Level} (l3 : Level)
34+
(R : Commutative-Ring l1)
35+
(A : associative-algebra-Commutative-Ring l2 R)
36+
where
37+
38+
subset-associative-algebra-Commutative-Ring : UU (l2 ⊔ lsuc l3)
39+
subset-associative-algebra-Commutative-Ring =
40+
subtype l3 (type-associative-algebra-Commutative-Ring R A)
41+
```
42+
43+
## Properties
44+
45+
### The condition of a subset containing zero
46+
47+
```agda
48+
module _
49+
{l1 l2 l3 : Level}
50+
(R : Commutative-Ring l1)
51+
(A : associative-algebra-Commutative-Ring l2 R)
52+
where
53+
54+
contains-zero-prop-subset-associative-algebra-Commutative-Ring :
55+
subtype l3 (subset-associative-algebra-Commutative-Ring l3 R A)
56+
contains-zero-prop-subset-associative-algebra-Commutative-Ring =
57+
contains-zero-prop-subset-algebra-Commutative-Ring
58+
( R)
59+
( algebra-associative-algebra-Commutative-Ring R A)
60+
61+
contains-zero-subset-associative-algebra-Commutative-Ring :
62+
subset-associative-algebra-Commutative-Ring l3 R A → UU l3
63+
contains-zero-subset-associative-algebra-Commutative-Ring =
64+
is-in-subtype contains-zero-prop-subset-associative-algebra-Commutative-Ring
65+
```
66+
67+
### The condition that a subset is closed under addition
68+
69+
```agda
70+
module _
71+
{l1 l2 l3 : Level}
72+
(R : Commutative-Ring l1)
73+
(A : associative-algebra-Commutative-Ring l2 R)
74+
where
75+
76+
is-closed-under-addition-prop-subset-associative-algebra-Commutative-Ring :
77+
subtype (l2 ⊔ l3) (subset-associative-algebra-Commutative-Ring l3 R A)
78+
is-closed-under-addition-prop-subset-associative-algebra-Commutative-Ring =
79+
is-closed-under-addition-prop-subset-algebra-Commutative-Ring
80+
( R)
81+
( algebra-associative-algebra-Commutative-Ring R A)
82+
83+
is-closed-under-addition-subset-associative-algebra-Commutative-Ring :
84+
subset-associative-algebra-Commutative-Ring l3 R A → UU (l2 ⊔ l3)
85+
is-closed-under-addition-subset-associative-algebra-Commutative-Ring =
86+
is-in-subtype
87+
( is-closed-under-addition-prop-subset-associative-algebra-Commutative-Ring)
88+
```
89+
90+
### The condition that a subset is closed under scalar multiplication
91+
92+
```agda
93+
module _
94+
{l1 l2 l3 : Level}
95+
(R : Commutative-Ring l1)
96+
(A : associative-algebra-Commutative-Ring l2 R)
97+
where
98+
99+
is-closed-under-scalar-multiplication-prop-subset-associative-algebra-Commutative-Ring :
100+
subtype (l1 ⊔ l2 ⊔ l3) (subset-associative-algebra-Commutative-Ring l3 R A)
101+
is-closed-under-scalar-multiplication-prop-subset-associative-algebra-Commutative-Ring =
102+
is-closed-under-scalar-multiplication-prop-subset-algebra-Commutative-Ring
103+
( R)
104+
( algebra-associative-algebra-Commutative-Ring R A)
105+
106+
is-closed-under-scalar-multiplication-subset-associative-algebra-Commutative-Ring :
107+
subset-associative-algebra-Commutative-Ring l3 R A → UU (l1 ⊔ l2 ⊔ l3)
108+
is-closed-under-scalar-multiplication-subset-associative-algebra-Commutative-Ring =
109+
is-in-subtype
110+
( is-closed-under-scalar-multiplication-prop-subset-associative-algebra-Commutative-Ring)
111+
```
112+
113+
### The condition that a subset is closed under multiplication
114+
115+
```agda
116+
module _
117+
{l1 l2 l3 : Level}
118+
(R : Commutative-Ring l1)
119+
(A : associative-algebra-Commutative-Ring l2 R)
120+
where
121+
122+
is-closed-under-multiplication-prop-subset-associative-algebra-Commutative-Ring :
123+
subtype (l2 ⊔ l3) (subset-associative-algebra-Commutative-Ring l3 R A)
124+
is-closed-under-multiplication-prop-subset-associative-algebra-Commutative-Ring =
125+
is-closed-under-multiplication-prop-subset-algebra-Commutative-Ring
126+
( R)
127+
( algebra-associative-algebra-Commutative-Ring R A)
128+
129+
is-closed-under-multiplication-subset-associative-algebra-Commutative-Ring :
130+
subset-associative-algebra-Commutative-Ring l3 R A → UU (l2 ⊔ l3)
131+
is-closed-under-multiplication-subset-associative-algebra-Commutative-Ring =
132+
is-in-subtype
133+
( is-closed-under-multiplication-prop-subset-associative-algebra-Commutative-Ring)
134+
```

0 commit comments

Comments
 (0)