Matrix overhaul

src/commutative-algebra.lagda.md

@@ -71,6 +71,7 @@ open import commutative-algebra.precategory-of-commutative-semirings public
 open import commutative-algebra.prime-ideals-commutative-rings public
 open import commutative-algebra.products-commutative-rings public
 open import commutative-algebra.products-ideals-commutative-rings public
+open import commutative-algebra.products-of-finite-sequences-of-elements-commutative-rings public
 open import commutative-algebra.products-radical-ideals-commutative-rings public
 open import commutative-algebra.products-subsets-commutative-rings public
 open import commutative-algebra.radical-ideals-commutative-rings public

src/commutative-algebra/products-of-finite-sequences-of-elements-commutative-rings.lagda.md

@@ -0,0 +1,41 @@
+# Products of finite sequences of elements of commutative rings
+
+```agda
+module commutative-algebra.products-of-finite-sequences-of-elements-commutative-rings where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import commutative-algebra.commutative-rings
+
+open import elementary-number-theory.natural-numbers
+
+open import foundation.universe-levels
+
+open import linear-algebra.finite-sequences-in-commutative-rings
+
+open import lists.finite-sequences
+
+open import ring-theory.products-of-finite-sequences-of-elements-rings
+```
+
+</details>
+
+## Idea
+
+The
+{{#concept "product operation" Disambiguation="over finite sequences in a commutative ring" Agda=product-fin-sequence-type-Commutative-Ring}}
+extends the binary multiplication operation on a
+[commutative ring](commutative-algebra.commutative-rings.md) `R` to any
+[finite sequence](lists.finite-sequences.md) of elements of `R`.
+
+## Definition
+
+```agda
+product-fin-sequence-type-Commutative-Ring :
+  {l : Level} (R : Commutative-Ring l) (n : ℕ) →
+  fin-sequence-type-Commutative-Ring R n → type-Commutative-Ring R
+product-fin-sequence-type-Commutative-Ring R =
+  product-fin-sequence-type-Ring (ring-Commutative-Ring R)
+```

src/foundation.lagda.md

@@ -452,6 +452,7 @@ open import foundation.similarity-preserving-maps-large-similarity-relations pub
 open import foundation.similarity-subtypes public
 open import foundation.singleton-induction public
 open import foundation.singleton-subtypes public
+open import foundation.singleton-subtypes-discrete-types public
 open import foundation.slice public
 open import foundation.small-maps public
 open import foundation.small-types public

src/foundation/binary-relations.lagda.md

@@ -32,8 +32,9 @@ open import foundation-core.torsorial-type-families
 
 ## Idea
 
-A **binary relation** on a type `A` is a family of types `R x y` depending on
-two variables `x y : A`. In the special case where each `R x y` is a
+A {{#concept "binary relation" WDID=Q130901 WD="binary relation" Agda=Relation}}
+on a type `A` is a family of types `R x y` depending on two variables `x y : A`.
+In the special case where each `R x y` is a
 [proposition](foundation-core.propositions.md), we say that the relation is
 valued in propositions. Thus, we take a general relation to mean a
 _proof-relevant_ relation.

src/foundation/singleton-subtypes-discrete-types.lagda.md

@@ -0,0 +1,65 @@
+# Singleton subtypes of discrete types
+
+```agda
+module foundation.singleton-subtypes-discrete-types where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-identifications-functions
+open import foundation.decidable-subtypes
+open import foundation.dependent-pair-types
+open import foundation.discrete-types
+open import foundation.functoriality-coproduct-types
+open import foundation.identity-types
+open import foundation.singleton-subtypes
+open import foundation.universe-levels
+
+open import foundation-core.subtypes
+open import foundation-core.transport-along-identifications
+```
+
+</details>
+
+## Idea
+
+[Singleton subtypes](foundation.singleton-subtypes.md) on
+[discrete types](foundation.discrete-types.md) are
+[decidable subtypes](foundation.decidable-subtypes.md).
+
+## Properties
+
+### Any singleton subtype of a discrete type is decidable
+
+```agda
+module _
+  {l1 l2 : Level}
+  (XD@(X , decide-eq-X) : Discrete-Type l1)
+  (S : subtype l2 X)
+  (((x , x∈S) , is-center-x) : is-singleton-subtype S)
+  where
+
+  is-decidable-is-singleton-subtype-Discrete-Type : is-decidable-subtype S
+  is-decidable-is-singleton-subtype-Discrete-Type y =
+    map-coproduct
+      ( λ x=y → tr (is-in-subtype S) x=y x∈S)
+      ( λ x≠y y∈S → x≠y (ap (inclusion-subtype S) (is-center-x (y , y∈S))))
+      ( decide-eq-X x y)
+```
+
+### The standard decidable singleton subtype associated with an element of a discrete type
+
+```agda
+module _
+  {l : Level}
+  (XD@(X , decide-eq-X) : Discrete-Type l)
+  where
+
+  decidable-standard-singleton-subtype-Discrete-Type :
+    X → decidable-subtype l X
+  decidable-standard-singleton-subtype-Discrete-Type y x =
+    ( x ＝ y ,
+      is-set-type-Discrete-Type XD x y ,
+      decide-eq-X x y)
+```

src/group-theory.lagda.md

@@ -49,6 +49,7 @@ open import group-theory.congruence-relations-monoids public
 open import group-theory.congruence-relations-semigroups public
 open import group-theory.conjugation public
 open import group-theory.conjugation-concrete-groups public
+open import group-theory.conjugation-invertible-elements-monoids public
 open import group-theory.contravariant-pushforward-concrete-group-actions public
 open import group-theory.cores-monoids public
 open import group-theory.cyclic-groups public