Skip to content

Commit ad36dd3

Browse files
lowasserlowasser
authored
Large function commutative rings (#1719)
Starting to build this out so we can do analysis on these too.
1 parent ac54453 commit ad36dd3

13 files changed

+422
-0
lines changed

‎src/commutative-algebra.lagda.md‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -39,6 +39,7 @@ open import commutative-algebra.isomorphisms-commutative-rings public
3939
open import commutative-algebra.joins-ideals-commutative-rings public
4040
open import commutative-algebra.joins-radical-ideals-commutative-rings public
4141
open import commutative-algebra.large-commutative-rings public
42+
open import commutative-algebra.large-function-commutative-rings public
4243
open import commutative-algebra.local-commutative-rings public
4344
open import commutative-algebra.maximal-ideals-commutative-rings public
4445
open import commutative-algebra.multiples-of-elements-commutative-rings public

‎src/commutative-algebra/large-function-commutative-rings.lagda.md‎

Lines changed: 42 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,42 @@
1+
# Large function commutative rings
2+
3+
```agda
4+
module commutative-algebra.large-function-commutative-rings where
5+
```
6+
7+
<details><summary>Imports</summary>
8+
9+
```agda
10+
open import commutative-algebra.large-commutative-rings
11+
12+
open import foundation.function-extensionality
13+
open import foundation.universe-levels
14+
15+
open import ring-theory.large-function-rings
16+
```
17+
18+
</details>
19+
20+
## Idea
21+
22+
Given a [large commutative ring](commutative-algebra.large-commutative-rings.md)
23+
`R` and an arbitrary type `A`, `A → R` forms a large commutative ring.
24+
25+
## Definition
26+
27+
```agda
28+
module _
29+
{l1 : Level}
30+
{α : Level → Level}
31+
{β : Level → Level → Level}
32+
(A : UU l1)
33+
(R : Large-Commutative-Ring α β)
34+
where
35+
36+
function-Large-Commutative-Ring :
37+
Large-Commutative-Ring (λ l → l1 ⊔ α l) (λ l2 l3 → l1 ⊔ β l2 l3)
38+
large-ring-Large-Commutative-Ring function-Large-Commutative-Ring =
39+
function-Large-Ring A (large-ring-Large-Commutative-Ring R)
40+
commutative-mul-Large-Commutative-Ring function-Large-Commutative-Ring f g =
41+
eq-htpy (λ a → commutative-mul-Large-Commutative-Ring R (f a) (g a))
42+
```

‎src/foundation.lagda.md‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -213,6 +213,8 @@ open import foundation.fixed-points-endofunctions public
213213
open import foundation.freely-generated-equivalence-relations public
214214
open import foundation.full-subtypes public
215215
open import foundation.function-extensionality public
216+
open import foundation.function-large-equivalence-relations public
217+
open import foundation.function-large-similarity-relations public
216218
open import foundation.function-types public
217219
open import foundation.function-types-with-apartness-relations public
218220
open import foundation.functional-correspondences public

‎src/foundation/function-large-equivalence-relations.lagda.md‎

Lines changed: 55 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,55 @@
1+
# Function large equivalence relations
2+
3+
```agda
4+
module foundation.function-large-equivalence-relations where
5+
```
6+
7+
<details><summary>Imports</summary>
8+
9+
```agda
10+
open import foundation.large-equivalence-relations
11+
open import foundation.propositions
12+
open import foundation.universe-levels
13+
```
14+
15+
</details>
16+
17+
## Idea
18+
19+
Given a [large equivalence relation](foundation.large-equivalence-relations.md)
20+
on `X` and a type `A`, there is an induced large equivalence relation on
21+
`A → X`.
22+
23+
## Definition
24+
25+
```agda
26+
module _
27+
{l1 : Level}
28+
{α : Level → Level}
29+
{β : Level → Level → Level}
30+
{X : (l : Level) → UU (α l)}
31+
(A : UU l1)
32+
(R : Large-Equivalence-Relation β X)
33+
where
34+
35+
function-Large-Equivalence-Relation :
36+
Large-Equivalence-Relation
37+
( λ l2 l3 → l1 ⊔ β l2 l3)
38+
( λ l → A → X l)
39+
sim-prop-Large-Equivalence-Relation function-Large-Equivalence-Relation f g =
40+
Π-Prop A (λ a → sim-prop-Large-Equivalence-Relation R (f a) (g a))
41+
refl-sim-Large-Equivalence-Relation function-Large-Equivalence-Relation f a =
42+
refl-sim-Large-Equivalence-Relation R (f a)
43+
symmetric-sim-Large-Equivalence-Relation function-Large-Equivalence-Relation
44+
f g f~g a =
45+
symmetric-sim-Large-Equivalence-Relation R (f a) (g a) (f~g a)
46+
transitive-sim-Large-Equivalence-Relation function-Large-Equivalence-Relation
47+
f g h g~h f~g a =
48+
transitive-sim-Large-Equivalence-Relation
49+
( R)
50+
( f a)
51+
( g a)
52+
( h a)
53+
( g~h a)
54+
( f~g a)
55+
```

‎src/foundation/function-large-similarity-relations.lagda.md‎

Lines changed: 46 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,46 @@
1+
# Function large similarity relations
2+
3+
```agda
4+
module foundation.function-large-similarity-relations where
5+
```
6+
7+
<details><summary>Imports</summary>
8+
9+
```agda
10+
open import foundation.function-extensionality
11+
open import foundation.function-large-equivalence-relations
12+
open import foundation.large-similarity-relations
13+
open import foundation.universe-levels
14+
```
15+
16+
</details>
17+
18+
## Idea
19+
20+
Given a [large similarity relation](foundation.large-similarity-relations.md) on
21+
`X` and any type `A`, there is an induced large similarity relation on `A → X`.
22+
23+
## Definition
24+
25+
```agda
26+
module _
27+
{l1 : Level}
28+
{α : Level → Level}
29+
{β : Level → Level → Level}
30+
{X : (l : Level) → UU (α l)}
31+
(A : UU l1)
32+
(R : Large-Similarity-Relation β X)
33+
where
34+
35+
function-Large-Similarity-Relation :
36+
Large-Similarity-Relation
37+
( λ l2 l3 → l1 ⊔ β l2 l3)
38+
( λ l → A → X l)
39+
large-equivalence-relation-Large-Similarity-Relation
40+
function-Large-Similarity-Relation =
41+
function-Large-Equivalence-Relation
42+
( A)
43+
( large-equivalence-relation-Large-Similarity-Relation R)
44+
eq-sim-Large-Similarity-Relation function-Large-Similarity-Relation f g f~g =
45+
eq-htpy (λ a → eq-sim-Large-Similarity-Relation R (f a) (g a) (f~g a))
46+
```

‎src/group-theory.lagda.md‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -121,6 +121,11 @@ open import group-theory.kernels-homomorphisms-concrete-groups public
121121
open import group-theory.kernels-homomorphisms-groups public
122122
open import group-theory.large-abelian-groups public
123123
open import group-theory.large-commutative-monoids public
124+
open import group-theory.large-function-abelian-groups public
125+
open import group-theory.large-function-commutative-monoids public
126+
open import group-theory.large-function-groups public
127+
open import group-theory.large-function-monoids public
128+
open import group-theory.large-function-semigroups public
124129
open import group-theory.large-groups public
125130
open import group-theory.large-monoids public
126131
open import group-theory.large-semigroups public

‎src/group-theory/large-function-abelian-groups.lagda.md‎

Lines changed: 40 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,40 @@
1+
# Large function abelian groups
2+
3+
```agda
4+
module group-theory.large-function-abelian-groups where
5+
```
6+
7+
<details><summary>Imports</summary>
8+
9+
```agda
10+
open import foundation.function-extensionality
11+
open import foundation.universe-levels
12+
13+
open import group-theory.large-abelian-groups
14+
open import group-theory.large-function-groups
15+
```
16+
17+
</details>
18+
19+
## Idea
20+
21+
Given a [large abelian group](group-theory.large-abelian-groups.md) `G` and an
22+
arbitrary type `A`, `A → G` forms a large abelian group.
23+
24+
## Definition
25+
26+
```agda
27+
module _
28+
{l1 : Level}
29+
{α : Level → Level}
30+
{β : Level → Level → Level}
31+
(A : UU l1)
32+
(G : Large-Ab α β)
33+
where
34+
35+
function-Large-Ab : Large-Ab (λ l → l1 ⊔ α l) (λ l2 l3 → l1 ⊔ β l2 l3)
36+
large-group-Large-Ab function-Large-Ab =
37+
function-Large-Group A (large-group-Large-Ab G)
38+
commutative-add-Large-Ab function-Large-Ab f g =
39+
eq-htpy (λ a → commutative-add-Large-Ab G (f a) (g a))
40+
```

‎src/group-theory/large-function-commutative-monoids.lagda.md‎

Lines changed: 42 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,42 @@
1+
# Large function commutative monoids
2+
3+
```agda
4+
module group-theory.large-function-commutative-monoids where
5+
```
6+
7+
<details><summary>Imports</summary>
8+
9+
```agda
10+
open import foundation.function-extensionality
11+
open import foundation.universe-levels
12+
13+
open import group-theory.large-commutative-monoids
14+
open import group-theory.large-function-monoids
15+
```
16+
17+
</details>
18+
19+
## Idea
20+
21+
Given a [large commutative monoid](group-theory.large-commutative-monoids.md)
22+
`M` and an arbitrary type `A`, `A → M` forms a large commutative monoid.
23+
24+
## Definition
25+
26+
```agda
27+
module _
28+
{l1 : Level}
29+
{α : Level → Level}
30+
{β : Level → Level → Level}
31+
(A : UU l1)
32+
(M : Large-Commutative-Monoid α β)
33+
where
34+
35+
function-Large-Commutative-Monoid :
36+
Large-Commutative-Monoid (λ l → l1 ⊔ α l) (λ l2 l3 → l1 ⊔ β l2 l3)
37+
large-monoid-Large-Commutative-Monoid function-Large-Commutative-Monoid =
38+
function-Large-Monoid A (large-monoid-Large-Commutative-Monoid M)
39+
commutative-mul-Large-Commutative-Monoid function-Large-Commutative-Monoid
40+
f g =
41+
eq-htpy ( λ a → commutative-mul-Large-Commutative-Monoid M (f a) (g a))
42+
```

‎src/group-theory/large-function-groups.lagda.md‎

Lines changed: 45 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,45 @@
1+
# Large function groups
2+
3+
```agda
4+
module group-theory.large-function-groups where
5+
```
6+
7+
<details><summary>Imports</summary>
8+
9+
```agda
10+
open import foundation.function-extensionality
11+
open import foundation.universe-levels
12+
13+
open import group-theory.large-function-monoids
14+
open import group-theory.large-groups
15+
```
16+
17+
</details>
18+
19+
## Idea
20+
21+
Given a [large group](group-theory.large-groups.md) `G` and an arbitrary type
22+
`A`, `A → G` forms a large group.
23+
24+
## Definition
25+
26+
```agda
27+
module _
28+
{l1 : Level}
29+
{α : Level → Level}
30+
{β : Level → Level → Level}
31+
(A : UU l1)
32+
(G : Large-Group α β)
33+
where
34+
35+
function-Large-Group : Large-Group (λ l → l1 ⊔ α l) (λ l2 l3 → l1 ⊔ β l2 l3)
36+
large-monoid-Large-Group function-Large-Group =
37+
function-Large-Monoid A (large-monoid-Large-Group G)
38+
inv-Large-Group function-Large-Group f a = inv-Large-Group G (f a)
39+
preserves-sim-inv-Large-Group function-Large-Group f g f~g a =
40+
preserves-sim-inv-Large-Group G (f a) (g a) (f~g a)
41+
left-inverse-law-mul-Large-Group function-Large-Group f =
42+
eq-htpy (λ a → left-inverse-law-mul-Large-Group G (f a))
43+
right-inverse-law-mul-Large-Group function-Large-Group f =
44+
eq-htpy (λ a → right-inverse-law-mul-Large-Group G (f a))
45+
```

‎src/group-theory/large-function-monoids.lagda.md‎

Lines changed: 54 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,54 @@
1+
# Large function monoids
2+
3+
```agda
4+
module group-theory.large-function-monoids where
5+
```
6+
7+
<details><summary>Imports</summary>
8+
9+
```agda
10+
open import foundation.function-extensionality
11+
open import foundation.function-large-similarity-relations
12+
open import foundation.universe-levels
13+
14+
open import group-theory.large-function-semigroups
15+
open import group-theory.large-monoids
16+
```
17+
18+
</details>
19+
20+
## Idea
21+
22+
Given a [large monoid](group-theory.large-monoids.md) `M` and an arbitrary type
23+
`A`, `A → M` forms a large monoid.
24+
25+
## Definition
26+
27+
```agda
28+
module _
29+
{l1 : Level}
30+
{α : Level → Level}
31+
{β : Level → Level → Level}
32+
(A : UU l1)
33+
(M : Large-Monoid α β)
34+
where
35+
36+
function-Large-Monoid :
37+
Large-Monoid (λ l → l1 ⊔ α l) (λ l2 l3 → l1 ⊔ β l2 l3)
38+
large-semigroup-Large-Monoid function-Large-Monoid =
39+
function-Large-Semigroup A (large-semigroup-Large-Monoid M)
40+
large-similarity-relation-Large-Monoid function-Large-Monoid =
41+
function-Large-Similarity-Relation
42+
( A)
43+
( large-similarity-relation-Large-Monoid M)
44+
raise-Large-Monoid function-Large-Monoid l f a = raise-Large-Monoid M l (f a)
45+
sim-raise-Large-Monoid function-Large-Monoid l2 f a =
46+
sim-raise-Large-Monoid M l2 (f a)
47+
preserves-sim-mul-Large-Monoid function-Large-Monoid f f' f~f' g g' g~g' a =
48+
preserves-sim-mul-Large-Monoid M (f a) (f' a) (f~f' a) (g a) (g' a) (g~g' a)
49+
unit-Large-Monoid function-Large-Monoid a = unit-Large-Monoid M
50+
left-unit-law-mul-Large-Monoid function-Large-Monoid f =
51+
eq-htpy (λ a → left-unit-law-mul-Large-Monoid M (f a))
52+
right-unit-law-mul-Large-Monoid function-Large-Monoid f =
53+
eq-htpy (λ a → right-unit-law-mul-Large-Monoid M (f a))
54+
```

0 commit comments

Comments
 (0)