diff --git a/src/commutative-algebra.lagda.md b/src/commutative-algebra.lagda.md index 7719d0d4d2..9d4aa29857 100644 --- a/src/commutative-algebra.lagda.md +++ b/src/commutative-algebra.lagda.md @@ -16,6 +16,8 @@ open import commutative-algebra.dependent-products-commutative-semirings public open import commutative-algebra.discrete-fields public open import commutative-algebra.eisenstein-integers public open import commutative-algebra.euclidean-domains public +open import commutative-algebra.formal-power-series-commutative-rings public +open import commutative-algebra.formal-power-series-commutative-semirings public open import commutative-algebra.full-ideals-commutative-rings public open import commutative-algebra.function-commutative-rings public open import commutative-algebra.function-commutative-semirings public diff --git a/src/commutative-algebra/commutative-rings.lagda.md b/src/commutative-algebra/commutative-rings.lagda.md index 06b3e5d600..8460281728 100644 --- a/src/commutative-algebra/commutative-rings.lagda.md +++ b/src/commutative-algebra/commutative-rings.lagda.md @@ -318,6 +318,10 @@ module _ add-Commutative-Ring (neg-Commutative-Ring x) (neg-Commutative-Ring y) distributive-neg-add-Commutative-Ring = distributive-neg-add-Ab ab-Commutative-Ring + + neg-zero-Commutative-Ring : + neg-Commutative-Ring zero-Commutative-Ring ＝ zero-Commutative-Ring + neg-zero-Commutative-Ring = neg-zero-Ring ring-Commutative-Ring ``` ### Multiplication in a commutative ring diff --git a/src/commutative-algebra/commutative-semirings.lagda.md b/src/commutative-algebra/commutative-semirings.lagda.md index 78e21f5b30..257f89fa25 100644 --- a/src/commutative-algebra/commutative-semirings.lagda.md +++ b/src/commutative-algebra/commutative-semirings.lagda.md @@ -10,6 +10,7 @@ module commutative-algebra.commutative-semirings where open import elementary-number-theory.addition-natural-numbers open import elementary-number-theory.natural-numbers +open import foundation.action-on-identifications-binary-functions open import foundation.dependent-pair-types open import foundation.identity-types open import foundation.iterated-dependent-product-types @@ -176,6 +177,11 @@ module _ (x y : type-Commutative-Semiring) → type-Commutative-Semiring mul-Commutative-Semiring' = mul-Semiring' semiring-Commutative-Semiring + ap-mul-Commutative-Semiring : + {x x' y y' : type-Commutative-Semiring} (p : Id x x') (q : Id y y') → + Id (mul-Commutative-Semiring x y) (mul-Commutative-Semiring x' y') + ap-mul-Commutative-Semiring p q = ap-binary mul-Commutative-Semiring p q + one-Commutative-Semiring : type-Commutative-Semiring one-Commutative-Semiring = one-Semiring semiring-Commutative-Semiring diff --git a/src/commutative-algebra/formal-power-series-commutative-rings.lagda.md b/src/commutative-algebra/formal-power-series-commutative-rings.lagda.md new file mode 100644 index 0000000000..d57d960cb8 --- /dev/null +++ b/src/commutative-algebra/formal-power-series-commutative-rings.lagda.md @@ -0,0 +1,657 @@ +# Formal power series on commutative rings + +```agda +module commutative-algebra.formal-power-series-commutative-rings where +``` + +
Imports + +```agda +open import commutative-algebra.commutative-rings +open import commutative-algebra.commutative-semirings +open import commutative-algebra.formal-power-series-commutative-semirings + +open import elementary-number-theory.natural-numbers + +open import foundation.dependent-pair-types +open import foundation.function-extensionality +open import foundation.function-types +open import foundation.homotopies +open import foundation.identity-types +open import foundation.sets +open import foundation.unital-binary-operations +open import foundation.universe-levels + +open import group-theory.abelian-groups +open import group-theory.commutative-monoids +open import group-theory.groups +open import group-theory.monoids +open import group-theory.semigroups + +open import ring-theory.rings +open import ring-theory.semirings +``` + +
+ +## Idea + +A +{{#concept "formal power series" Agda=formal-power-series-Commutative-Ring WDID=Q1003025 WD="formal power series"}} +in a [commutative ring](commutative-algebra.commutative-rings.md) `R` is a +symbolic infinite sum over all `n : ℕ` of `cₙ xⁿ`, where `cₙ : R`. Convergence +of this sum is not relevant, but with the standard definitions of addition and +multiplication for power series, this forms a new commutative ring. + +## Definition + +```agda +module _ + {l : Level} (R : Commutative-Ring l) + where + + formal-power-series-Commutative-Ring : UU l + formal-power-series-Commutative-Ring = + formal-power-series-Commutative-Semiring + ( commutative-semiring-Commutative-Ring R) + + formal-power-series-coefficients-Commutative-Ring : + (ℕ → type-Commutative-Ring R) → + formal-power-series-Commutative-Ring + formal-power-series-coefficients-Commutative-Ring = + formal-power-series-coefficients-Commutative-Semiring + ( commutative-semiring-Commutative-Ring R) + + coefficient-formal-power-series-Commutative-Ring : + formal-power-series-Commutative-Ring → ℕ → type-Commutative-Ring R + coefficient-formal-power-series-Commutative-Ring = + coefficient-formal-power-series-Commutative-Semiring + ( commutative-semiring-Commutative-Ring R) + + coefficient-formal-power-series-coefficients-Commutative-Ring : + (c : ℕ → type-Commutative-Ring R) → + coefficient-formal-power-series-Commutative-Ring + (formal-power-series-coefficients-Commutative-Ring c) ~ c + coefficient-formal-power-series-coefficients-Commutative-Ring = + coefficient-formal-power-series-coefficients-Commutative-Semiring + ( commutative-semiring-Commutative-Ring R) + + eq-formal-power-series-coefficients-Commutative-Ring : + (p : formal-power-series-Commutative-Ring) → + p ＝ + formal-power-series-coefficients-Commutative-Ring + ( coefficient-formal-power-series-Commutative-Ring p) + eq-formal-power-series-coefficients-Commutative-Ring = + eq-formal-power-series-coefficients-Commutative-Semiring + ( commutative-semiring-Commutative-Ring R) + + eq-htpy-coefficients-formal-power-series-Commutative-Ring : + ( p q : formal-power-series-Commutative-Ring) → + ( coefficient-formal-power-series-Commutative-Ring p ~ + coefficient-formal-power-series-Commutative-Ring q) → + p ＝ q + eq-htpy-coefficients-formal-power-series-Commutative-Ring = + eq-htpy-coefficients-formal-power-series-Commutative-Semiring + ( commutative-semiring-Commutative-Ring R) + + is-set-formal-power-series-Commutative-Ring : + is-set formal-power-series-Commutative-Ring + is-set-formal-power-series-Commutative-Ring = + is-set-formal-power-series-Commutative-Semiring + ( commutative-semiring-Commutative-Ring R) + + set-formal-power-series-Commutative-Ring : Set l + set-formal-power-series-Commutative-Ring = + set-formal-power-series-Commutative-Semiring + ( commutative-semiring-Commutative-Ring R) +``` + +## Operations + +### Zero formal power series + +```agda +module _ + {l : Level} (R : Commutative-Ring l) + where + + zero-formal-power-series-Commutative-Ring : + formal-power-series-Commutative-Ring R + zero-formal-power-series-Commutative-Ring = + zero-formal-power-series-Commutative-Semiring + ( commutative-semiring-Commutative-Ring R) + + eq-coefficient-zero-formal-power-series-Commutative-Ring : + zero-formal-power-series-Commutative-Ring ＝ + formal-power-series-coefficients-Commutative-Ring + ( R) + ( λ _ → zero-Commutative-Ring R) + eq-coefficient-zero-formal-power-series-Commutative-Ring = + eq-coefficient-zero-formal-power-series-Commutative-Semiring + ( commutative-semiring-Commutative-Ring R) + + htpy-coefficient-zero-formal-power-series-Commutative-Ring : + coefficient-formal-power-series-Commutative-Ring + ( R) + ( zero-formal-power-series-Commutative-Ring) ~ + ( λ _ → zero-Commutative-Ring R) + htpy-coefficient-zero-formal-power-series-Commutative-Ring = + htpy-coefficient-zero-formal-power-series-Commutative-Semiring + ( commutative-semiring-Commutative-Ring R) +``` + +### Constant formal power series + +```agda +module _ + {l : Level} (R : Commutative-Ring l) + where + + coefficient-constant-formal-power-series-Commutative-Ring : + type-Commutative-Ring R → ℕ → type-Commutative-Ring R + coefficient-constant-formal-power-series-Commutative-Ring = + coefficient-constant-formal-power-series-Commutative-Semiring + ( commutative-semiring-Commutative-Ring R) + + coefficient-nonzero-constant-formal-power-series-Commutative-Ring : + (c : type-Commutative-Ring R) → (n : ℕ) → is-nonzero-ℕ n → + is-zero-Commutative-Ring R + ( coefficient-constant-formal-power-series-Commutative-Ring c n) + coefficient-nonzero-constant-formal-power-series-Commutative-Ring = + coefficient-nonzero-constant-formal-power-series-Commutative-Semiring + ( commutative-semiring-Commutative-Ring R) + + constant-formal-power-series-Commutative-Ring : + type-Commutative-Ring R → formal-power-series-Commutative-Ring R + constant-formal-power-series-Commutative-Ring = + constant-formal-power-series-Commutative-Semiring + ( commutative-semiring-Commutative-Ring R) + + eq-coefficient-constant-formal-power-series-Commutative-Ring : + (c : type-Commutative-Ring R) → + constant-formal-power-series-Commutative-Ring c ＝ + formal-power-series-coefficients-Commutative-Ring + ( R) + ( coefficient-constant-formal-power-series-Commutative-Ring c) + eq-coefficient-constant-formal-power-series-Commutative-Ring = + eq-coefficient-constant-formal-power-series-Commutative-Semiring + ( commutative-semiring-Commutative-Ring R) + + one-formal-power-series-Commutative-Ring : + formal-power-series-Commutative-Ring R + one-formal-power-series-Commutative-Ring = + one-formal-power-series-Commutative-Semiring + ( commutative-semiring-Commutative-Ring R) +``` + +#### The zero formal power series is the constant formal power series for zero + +```agda +module _ + {l : Level} (R : Commutative-Ring l) + where + + eq-zero-constant-formal-power-series-Commutative-Ring : + constant-formal-power-series-Commutative-Ring R (zero-Commutative-Ring R) ＝ + zero-formal-power-series-Commutative-Ring R + eq-zero-constant-formal-power-series-Commutative-Ring = + eq-zero-constant-formal-power-series-Commutative-Semiring + ( commutative-semiring-Commutative-Ring R) +``` + +### Addition + +```agda +module _ + {l : Level} (R : Commutative-Ring l) + where + + coefficient-add-formal-power-series-Commutative-Ring : + (p q : formal-power-series-Commutative-Ring R) (n : ℕ) → + type-Commutative-Ring R + coefficient-add-formal-power-series-Commutative-Ring = + coefficient-add-formal-power-series-Commutative-Semiring + ( commutative-semiring-Commutative-Ring R) + + add-formal-power-series-Commutative-Ring : + formal-power-series-Commutative-Ring R → + formal-power-series-Commutative-Ring R → + formal-power-series-Commutative-Ring R + add-formal-power-series-Commutative-Ring = + add-formal-power-series-Commutative-Semiring + ( commutative-semiring-Commutative-Ring R) + + eq-coefficient-add-formal-power-series-Commutative-Ring : + (p q : formal-power-series-Commutative-Ring R) → + add-formal-power-series-Commutative-Ring p q ＝ + formal-power-series-coefficients-Commutative-Ring + ( R) + ( coefficient-add-formal-power-series-Commutative-Ring p q) + eq-coefficient-add-formal-power-series-Commutative-Ring = + eq-coefficient-add-formal-power-series-Commutative-Semiring + ( commutative-semiring-Commutative-Ring R) + + htpy-coefficient-add-formal-power-series-Commutative-Ring : + (p q : formal-power-series-Commutative-Ring R) → + coefficient-formal-power-series-Commutative-Ring + ( R) + ( add-formal-power-series-Commutative-Ring p q) ~ + coefficient-add-formal-power-series-Commutative-Ring p q + htpy-coefficient-add-formal-power-series-Commutative-Ring = + htpy-coefficient-add-formal-power-series-Commutative-Semiring + ( commutative-semiring-Commutative-Ring R) +``` + +#### Commutativity + +```agda +module _ + {l : Level} (R : Commutative-Ring l) + where + + commutative-add-formal-power-series-Commutative-Ring : + (p q : formal-power-series-Commutative-Ring R) → + add-formal-power-series-Commutative-Ring R p q ＝ + add-formal-power-series-Commutative-Ring R q p + commutative-add-formal-power-series-Commutative-Ring = + commutative-add-formal-power-series-Commutative-Semiring + ( commutative-semiring-Commutative-Ring R) +``` + +#### Unit laws + +```agda +module _ + {l : Level} (R : Commutative-Ring l) + where + + left-unit-law-add-formal-power-series-Commutative-Ring : + (p : formal-power-series-Commutative-Ring R) → + add-formal-power-series-Commutative-Ring + ( R) + ( zero-formal-power-series-Commutative-Ring R) + ( p) ＝ p + left-unit-law-add-formal-power-series-Commutative-Ring = + left-unit-law-add-formal-power-series-Commutative-Semiring + ( commutative-semiring-Commutative-Ring R) + + right-unit-law-add-formal-power-series-Commutative-Ring : + (p : formal-power-series-Commutative-Ring R) → + add-formal-power-series-Commutative-Ring + ( R) + ( p) + ( zero-formal-power-series-Commutative-Ring R) ＝ p + right-unit-law-add-formal-power-series-Commutative-Ring = + right-unit-law-add-formal-power-series-Commutative-Semiring + ( commutative-semiring-Commutative-Ring R) +``` + +#### Associativity + +```agda +module _ + {l : Level} (R : Commutative-Ring l) + where + + associative-add-formal-power-series-Commutative-Ring : + (p q r : formal-power-series-Commutative-Ring R) → + add-formal-power-series-Commutative-Ring + ( R) + ( add-formal-power-series-Commutative-Ring R p q) + ( r) ＝ + add-formal-power-series-Commutative-Ring + ( R) + ( p) + ( add-formal-power-series-Commutative-Ring R q r) + associative-add-formal-power-series-Commutative-Ring = + associative-add-formal-power-series-Commutative-Semiring + ( commutative-semiring-Commutative-Ring R) +``` + +### Negation + +```agda +module _ + {l : Level} (R : Commutative-Ring l) + (p : formal-power-series-Commutative-Ring R) + where + + opaque + neg-formal-power-series-Commutative-Ring : + formal-power-series-Commutative-Ring R + neg-formal-power-series-Commutative-Ring = + formal-power-series-coefficients-Commutative-Ring + ( R) + ( neg-Commutative-Ring R ∘ + coefficient-formal-power-series-Commutative-Ring R p) + + htpy-coefficient-neg-formal-power-series-Commutative-Ring : + coefficient-formal-power-series-Commutative-Ring + ( R) + ( neg-formal-power-series-Commutative-Ring) ~ + neg-Commutative-Ring R ∘ + coefficient-formal-power-series-Commutative-Ring R p + htpy-coefficient-neg-formal-power-series-Commutative-Ring = + coefficient-formal-power-series-coefficients-Commutative-Ring R _ + + eq-coefficient-neg-formal-power-series-Commutative-Ring : + neg-formal-power-series-Commutative-Ring ＝ + formal-power-series-coefficients-Commutative-Ring + ( R) + ( neg-Commutative-Ring R ∘ + coefficient-formal-power-series-Commutative-Ring R p) + eq-coefficient-neg-formal-power-series-Commutative-Ring = refl +``` + +#### Inverse laws for addition + +```agda +module _ + {l : Level} (R : Commutative-Ring l) + (p : formal-power-series-Commutative-Ring R) + where + + abstract + left-inverse-law-add-formal-power-series-Commutative-Ring : + add-formal-power-series-Commutative-Ring + ( R) + ( neg-formal-power-series-Commutative-Ring R p) + ( p) ＝ + zero-formal-power-series-Commutative-Ring R + left-inverse-law-add-formal-power-series-Commutative-Ring = + eq-htpy-coefficients-formal-power-series-Commutative-Ring + ( R) + ( _) + ( _) + ( λ n → + htpy-coefficient-add-formal-power-series-Commutative-Ring R _ _ n ∙ + ap-add-Commutative-Ring + ( R) + ( htpy-coefficient-neg-formal-power-series-Commutative-Ring R p n) + ( refl) ∙ + left-inverse-law-add-Commutative-Ring R _ ∙ + inv (htpy-coefficient-zero-formal-power-series-Commutative-Ring R n)) + + right-inverse-law-add-formal-power-series-Commutative-Ring : + add-formal-power-series-Commutative-Ring + ( R) + ( p) + ( neg-formal-power-series-Commutative-Ring R p) ＝ + zero-formal-power-series-Commutative-Ring R + right-inverse-law-add-formal-power-series-Commutative-Ring = + commutative-add-formal-power-series-Commutative-Ring R _ _ ∙ + left-inverse-law-add-formal-power-series-Commutative-Ring +``` + +#### The additive Abelian group of formal power series + +```agda +module _ + {l : Level} (R : Commutative-Ring l) + where + + semigroup-add-formal-power-series-Commutative-Ring : Semigroup l + semigroup-add-formal-power-series-Commutative-Ring = + semigroup-add-formal-power-series-Commutative-Semiring + ( commutative-semiring-Commutative-Ring R) + + is-unital-add-formal-power-series-Commutative-Ring : + is-unital (add-formal-power-series-Commutative-Ring R) + is-unital-add-formal-power-series-Commutative-Ring = + is-unital-add-formal-power-series-Commutative-Semiring + ( commutative-semiring-Commutative-Ring R) + + monoid-add-formal-power-series-Commutative-Ring : Monoid l + monoid-add-formal-power-series-Commutative-Ring = + monoid-add-formal-power-series-Commutative-Semiring + ( commutative-semiring-Commutative-Ring R) + + commutative-monoid-add-formal-power-series-Commutative-Ring : + Commutative-Monoid l + commutative-monoid-add-formal-power-series-Commutative-Ring = + commutative-monoid-add-formal-power-series-Commutative-Semiring + ( commutative-semiring-Commutative-Ring R) + + group-add-formal-power-series-Commutative-Ring : Group l + group-add-formal-power-series-Commutative-Ring = + semigroup-add-formal-power-series-Commutative-Ring , + is-unital-add-formal-power-series-Commutative-Ring , + neg-formal-power-series-Commutative-Ring R , + left-inverse-law-add-formal-power-series-Commutative-Ring R , + right-inverse-law-add-formal-power-series-Commutative-Ring R + + abelian-group-add-formal-power-series-Commutative-Ring : Ab l + abelian-group-add-formal-power-series-Commutative-Ring = + group-add-formal-power-series-Commutative-Ring , + commutative-add-formal-power-series-Commutative-Ring R +``` + +### Multiplication + +```agda +module _ + {l : Level} (R : Commutative-Ring l) + (p q : formal-power-series-Commutative-Ring R) + where + + coefficient-mul-formal-power-series-Commutative-Ring : + ℕ → type-Commutative-Ring R + coefficient-mul-formal-power-series-Commutative-Ring = + coefficient-mul-formal-power-series-Commutative-Semiring + ( commutative-semiring-Commutative-Ring R) + ( p) + ( q) + + mul-formal-power-series-Commutative-Ring : + formal-power-series-Commutative-Ring R + mul-formal-power-series-Commutative-Ring = + mul-formal-power-series-Commutative-Semiring + ( commutative-semiring-Commutative-Ring R) + ( p) + ( q) + + eq-coefficient-mul-formal-power-series-Commutative-Ring : + coefficient-formal-power-series-Commutative-Ring + ( R) + ( mul-formal-power-series-Commutative-Ring) ~ + coefficient-mul-formal-power-series-Commutative-Ring + eq-coefficient-mul-formal-power-series-Commutative-Ring = + eq-coefficient-mul-formal-power-series-Commutative-Semiring + ( commutative-semiring-Commutative-Ring R) + ( p) + ( q) +``` + +#### Commutativity + +```agda +module _ + {l : Level} (R : Commutative-Ring l) + (p q : formal-power-series-Commutative-Ring R) + where + + commutative-mul-formal-power-series-Commutative-Ring : + mul-formal-power-series-Commutative-Ring R p q ＝ + mul-formal-power-series-Commutative-Ring R q p + commutative-mul-formal-power-series-Commutative-Ring = + commutative-mul-formal-power-series-Commutative-Semiring + ( commutative-semiring-Commutative-Ring R) + ( p) + ( q) +``` + +#### Associativity + +```agda +module _ + {l : Level} (R : Commutative-Ring l) + (p q r : formal-power-series-Commutative-Ring R) + where + + associative-mul-formal-power-series-Commutative-Ring : + mul-formal-power-series-Commutative-Ring + ( R) + ( mul-formal-power-series-Commutative-Ring R p q) + ( r) ＝ + mul-formal-power-series-Commutative-Ring + ( R) + ( p) + ( mul-formal-power-series-Commutative-Ring R q r) + associative-mul-formal-power-series-Commutative-Ring = + associative-mul-formal-power-series-Commutative-Semiring + ( commutative-semiring-Commutative-Ring R) + ( p) + ( q) + ( r) +``` + +#### Unit laws + +```agda +module _ + {l : Level} (R : Commutative-Ring l) + (p : formal-power-series-Commutative-Ring R) + where + + left-unit-law-mul-formal-power-series-Commutative-Ring : + mul-formal-power-series-Commutative-Ring + ( R) + ( one-formal-power-series-Commutative-Ring R) + ( p) ＝ p + left-unit-law-mul-formal-power-series-Commutative-Ring = + left-unit-law-mul-formal-power-series-Commutative-Semiring + ( commutative-semiring-Commutative-Ring R) + ( p) + + right-unit-law-mul-formal-power-series-Commutative-Ring : + mul-formal-power-series-Commutative-Ring + ( R) + ( p) + ( one-formal-power-series-Commutative-Ring R) ＝ p + right-unit-law-mul-formal-power-series-Commutative-Ring = + right-unit-law-mul-formal-power-series-Commutative-Semiring + ( commutative-semiring-Commutative-Ring R) + ( p) +``` + +#### Zero laws of multiplication + +```agda +module _ + {l : Level} (R : Commutative-Ring l) + (p : formal-power-series-Commutative-Ring R) + where + + left-zero-law-mul-formal-power-series-Commutative-Ring : + mul-formal-power-series-Commutative-Ring + ( R) + ( zero-formal-power-series-Commutative-Ring R) + ( p) ＝ + zero-formal-power-series-Commutative-Ring R + left-zero-law-mul-formal-power-series-Commutative-Ring = + left-zero-law-mul-formal-power-series-Commutative-Semiring + ( commutative-semiring-Commutative-Ring R) + ( p) + + right-zero-law-mul-formal-power-series-Commutative-Ring : + mul-formal-power-series-Commutative-Ring + ( R) + ( p) + ( zero-formal-power-series-Commutative-Ring R) ＝ + zero-formal-power-series-Commutative-Ring R + right-zero-law-mul-formal-power-series-Commutative-Ring = + right-zero-law-mul-formal-power-series-Commutative-Semiring + ( commutative-semiring-Commutative-Ring R) + ( p) +``` + +#### Distributivity of multiplication over addition + +```agda +left-distributive-mul-add-formal-power-series-Commutative-Ring : + {l : Level} (R : Commutative-Ring l) → + (p q r : formal-power-series-Commutative-Ring R) → + mul-formal-power-series-Commutative-Ring + ( R) + ( p) + ( add-formal-power-series-Commutative-Ring R q r) ＝ + add-formal-power-series-Commutative-Ring + ( R) + ( mul-formal-power-series-Commutative-Ring R p q) + ( mul-formal-power-series-Commutative-Ring R p r) +left-distributive-mul-add-formal-power-series-Commutative-Ring R = + left-distributive-mul-add-formal-power-series-Commutative-Semiring + ( commutative-semiring-Commutative-Ring R) + +right-distributive-mul-add-formal-power-series-Commutative-Ring : + {l : Level} (R : Commutative-Ring l) → + (p q r : formal-power-series-Commutative-Ring R) → + mul-formal-power-series-Commutative-Ring + ( R) + ( add-formal-power-series-Commutative-Ring R p q) + ( r) ＝ + add-formal-power-series-Commutative-Ring + ( R) + ( mul-formal-power-series-Commutative-Ring R p r) + ( mul-formal-power-series-Commutative-Ring R q r) +right-distributive-mul-add-formal-power-series-Commutative-Ring R = + right-distributive-mul-add-formal-power-series-Commutative-Semiring + ( commutative-semiring-Commutative-Ring R) +``` + +### The commutative ring of formal power series + +```agda +module _ + {l : Level} (R : Commutative-Ring l) + where + + has-associative-mul-formal-power-series-Commutative-Ring : + has-associative-mul (formal-power-series-Commutative-Ring R) + has-associative-mul-formal-power-series-Commutative-Ring = + mul-formal-power-series-Commutative-Ring R , + associative-mul-formal-power-series-Commutative-Ring R + + unit-laws-mul-formal-power-series-Commutative-Ring : + unit-laws + ( mul-formal-power-series-Commutative-Ring R) + ( one-formal-power-series-Commutative-Ring R) + unit-laws-mul-formal-power-series-Commutative-Ring = + left-unit-law-mul-formal-power-series-Commutative-Ring R , + right-unit-law-mul-formal-power-series-Commutative-Ring R + + is-unital-mul-formal-power-series-Commutative-Ring : + is-unital (mul-formal-power-series-Commutative-Ring R) + is-unital-mul-formal-power-series-Commutative-Ring = + one-formal-power-series-Commutative-Ring R , + unit-laws-mul-formal-power-series-Commutative-Ring + + semiring-formal-power-series-Commutative-Ring : Semiring l + semiring-formal-power-series-Commutative-Ring = + commutative-monoid-add-formal-power-series-Commutative-Ring R , + ( has-associative-mul-formal-power-series-Commutative-Ring , + is-unital-mul-formal-power-series-Commutative-Ring , + left-distributive-mul-add-formal-power-series-Commutative-Ring R , + right-distributive-mul-add-formal-power-series-Commutative-Ring R) , + left-zero-law-mul-formal-power-series-Commutative-Ring R , + right-zero-law-mul-formal-power-series-Commutative-Ring R + + commutative-semiring-formal-power-series-Commutative-Ring : + Commutative-Semiring l + commutative-semiring-formal-power-series-Commutative-Ring = + semiring-formal-power-series-Commutative-Ring , + commutative-mul-formal-power-series-Commutative-Ring R + + ring-formal-power-series-Commutative-Ring : Ring l + ring-formal-power-series-Commutative-Ring = + abelian-group-add-formal-power-series-Commutative-Ring R , + has-associative-mul-formal-power-series-Commutative-Ring , + is-unital-mul-formal-power-series-Commutative-Ring , + left-distributive-mul-add-formal-power-series-Commutative-Ring R , + right-distributive-mul-add-formal-power-series-Commutative-Ring R + + commutative-ring-formal-power-series-Commutative-Ring : Commutative-Ring l + commutative-ring-formal-power-series-Commutative-Ring = + ring-formal-power-series-Commutative-Ring , + commutative-mul-formal-power-series-Commutative-Ring R +``` diff --git a/src/commutative-algebra/formal-power-series-commutative-semirings.lagda.md b/src/commutative-algebra/formal-power-series-commutative-semirings.lagda.md new file mode 100644 index 0000000000..512f6773a2 --- /dev/null +++ b/src/commutative-algebra/formal-power-series-commutative-semirings.lagda.md @@ -0,0 +1,876 @@ +# Formal power series on commutative semirings + +```agda +{-# OPTIONS --lossy-unification #-} + +module commutative-algebra.formal-power-series-commutative-semirings where +``` + +
Imports + +```agda +open import commutative-algebra.commutative-semirings +open import commutative-algebra.sums-commutative-semirings + +open import elementary-number-theory.addition-natural-numbers +open import elementary-number-theory.equality-natural-numbers +open import elementary-number-theory.inequality-natural-numbers +open import elementary-number-theory.natural-numbers +open import elementary-number-theory.pairs-with-natural-sums +open import elementary-number-theory.strict-inequality-natural-numbers + +open import foundation.action-on-identifications-binary-functions +open import foundation.action-on-identifications-functions +open import foundation.coproduct-types +open import foundation.dependent-pair-types +open import foundation.empty-types +open import foundation.function-extensionality +open import foundation.function-types +open import foundation.homotopies +open import foundation.identity-types +open import foundation.sets +open import foundation.unit-type +open import foundation.unital-binary-operations +open import foundation.universe-levels + +open import group-theory.abelian-groups +open import group-theory.commutative-monoids +open import group-theory.function-commutative-monoids +open import group-theory.groups +open import group-theory.monoids +open import group-theory.semigroups + +open import ring-theory.semirings + +open import univalent-combinatorics.dependent-pair-types +``` + +
+ +## Idea + +A +{{#concept "formal power series" Agda=formal-power-series-Commutative-Semiring WDID=Q1003025 WD="formal power series"}} +in a [commutative semiring](commutative-algebra.commutative-semirings.md) `R` is +a symbolic infinite sum over all `n : ℕ` of `cₙ xⁿ`, where `cₙ : R`. Convergence +of this sum is not relevant, but with the standard definitions of addition and +multiplication for power series, this forms a new commutative semiring. + +## Definition + +```agda +module _ + {l : Level} (R : Commutative-Semiring l) + where + + opaque + formal-power-series-Commutative-Semiring : UU l + formal-power-series-Commutative-Semiring = ℕ → type-Commutative-Semiring R + + formal-power-series-coefficients-Commutative-Semiring : + (ℕ → type-Commutative-Semiring R) → + formal-power-series-Commutative-Semiring + formal-power-series-coefficients-Commutative-Semiring = id + + coefficient-formal-power-series-Commutative-Semiring : + formal-power-series-Commutative-Semiring → ℕ → type-Commutative-Semiring R + coefficient-formal-power-series-Commutative-Semiring = id + + coefficient-formal-power-series-coefficients-Commutative-Semiring : + (c : ℕ → type-Commutative-Semiring R) → + coefficient-formal-power-series-Commutative-Semiring + (formal-power-series-coefficients-Commutative-Semiring c) ~ c + coefficient-formal-power-series-coefficients-Commutative-Semiring _ _ = refl + + eq-formal-power-series-coefficients-Commutative-Semiring : + (p : formal-power-series-Commutative-Semiring) → + p ＝ + formal-power-series-coefficients-Commutative-Semiring + ( coefficient-formal-power-series-Commutative-Semiring p) + eq-formal-power-series-coefficients-Commutative-Semiring _ = refl + + eq-htpy-coefficients-formal-power-series-Commutative-Semiring : + ( p q : formal-power-series-Commutative-Semiring) → + ( coefficient-formal-power-series-Commutative-Semiring p ~ + coefficient-formal-power-series-Commutative-Semiring q) → + p ＝ q + eq-htpy-coefficients-formal-power-series-Commutative-Semiring _ _ = eq-htpy + + is-set-formal-power-series-Commutative-Semiring : + is-set formal-power-series-Commutative-Semiring + is-set-formal-power-series-Commutative-Semiring = + is-set-function-type (is-set-type-Set (set-Commutative-Semiring R)) + + set-formal-power-series-Commutative-Semiring : Set l + set-formal-power-series-Commutative-Semiring = + formal-power-series-Commutative-Semiring , + is-set-formal-power-series-Commutative-Semiring +``` + +## Operations + +### Zero formal power series + +```agda +module _ + {l : Level} (R : Commutative-Semiring l) + where + + opaque + unfolding formal-power-series-Commutative-Semiring + + zero-formal-power-series-Commutative-Semiring : + formal-power-series-Commutative-Semiring R + zero-formal-power-series-Commutative-Semiring _ = + zero-Commutative-Semiring R + + eq-coefficient-zero-formal-power-series-Commutative-Semiring : + zero-formal-power-series-Commutative-Semiring ＝ + formal-power-series-coefficients-Commutative-Semiring + ( R) + ( λ _ → zero-Commutative-Semiring R) + eq-coefficient-zero-formal-power-series-Commutative-Semiring = refl + + htpy-coefficient-zero-formal-power-series-Commutative-Semiring : + coefficient-formal-power-series-Commutative-Semiring + ( R) + ( zero-formal-power-series-Commutative-Semiring) ~ + ( λ _ → zero-Commutative-Semiring R) + htpy-coefficient-zero-formal-power-series-Commutative-Semiring _ = refl +``` + +### Constant formal power series + +```agda +module _ + {l : Level} (R : Commutative-Semiring l) + where + + coefficient-constant-formal-power-series-Commutative-Semiring : + type-Commutative-Semiring R → ℕ → type-Commutative-Semiring R + coefficient-constant-formal-power-series-Commutative-Semiring c zero-ℕ = c + coefficient-constant-formal-power-series-Commutative-Semiring c (succ-ℕ _) = + zero-Commutative-Semiring R + + coefficient-nonzero-constant-formal-power-series-Commutative-Semiring : + (c : type-Commutative-Semiring R) → (n : ℕ) → is-nonzero-ℕ n → + is-zero-Commutative-Semiring R + ( coefficient-constant-formal-power-series-Commutative-Semiring c n) + coefficient-nonzero-constant-formal-power-series-Commutative-Semiring + c zero-ℕ H = ex-falso (H refl) + coefficient-nonzero-constant-formal-power-series-Commutative-Semiring + c (succ-ℕ _) _ = refl + + opaque + unfolding formal-power-series-Commutative-Semiring + + constant-formal-power-series-Commutative-Semiring : + type-Commutative-Semiring R → formal-power-series-Commutative-Semiring R + constant-formal-power-series-Commutative-Semiring = + coefficient-constant-formal-power-series-Commutative-Semiring + + eq-coefficient-constant-formal-power-series-Commutative-Semiring : + (c : type-Commutative-Semiring R) → + constant-formal-power-series-Commutative-Semiring c ＝ + formal-power-series-coefficients-Commutative-Semiring + ( R) + ( coefficient-constant-formal-power-series-Commutative-Semiring c) + eq-coefficient-constant-formal-power-series-Commutative-Semiring c = refl + + one-formal-power-series-Commutative-Semiring : + formal-power-series-Commutative-Semiring R + one-formal-power-series-Commutative-Semiring = + constant-formal-power-series-Commutative-Semiring + ( one-Commutative-Semiring R) +``` + +#### The zero formal power series is the constant formal power series for zero + +```agda +module _ + {l : Level} (R : Commutative-Semiring l) + where + + opaque + unfolding formal-power-series-Commutative-Semiring + unfolding zero-formal-power-series-Commutative-Semiring + unfolding constant-formal-power-series-Commutative-Semiring + + eq-zero-constant-formal-power-series-Commutative-Semiring : + constant-formal-power-series-Commutative-Semiring + R (zero-Commutative-Semiring R) ＝ + zero-formal-power-series-Commutative-Semiring R + eq-zero-constant-formal-power-series-Commutative-Semiring = + eq-htpy (λ { zero-ℕ → refl ; (succ-ℕ _) → refl}) +``` + +### Addition + +```agda +module _ + {l : Level} (R : Commutative-Semiring l) + where + + coefficient-add-formal-power-series-Commutative-Semiring : + (p q : formal-power-series-Commutative-Semiring R) (n : ℕ) → + type-Commutative-Semiring R + coefficient-add-formal-power-series-Commutative-Semiring p q = + mul-function-Commutative-Monoid + ( additive-commutative-monoid-Commutative-Semiring R) + ( ℕ) + ( coefficient-formal-power-series-Commutative-Semiring R p) + ( coefficient-formal-power-series-Commutative-Semiring R q) + + opaque + unfolding formal-power-series-Commutative-Semiring + + add-formal-power-series-Commutative-Semiring : + formal-power-series-Commutative-Semiring R → + formal-power-series-Commutative-Semiring R → + formal-power-series-Commutative-Semiring R + add-formal-power-series-Commutative-Semiring = + coefficient-add-formal-power-series-Commutative-Semiring + + eq-coefficient-add-formal-power-series-Commutative-Semiring : + (p q : formal-power-series-Commutative-Semiring R) → + add-formal-power-series-Commutative-Semiring p q ＝ + formal-power-series-coefficients-Commutative-Semiring + ( R) + ( coefficient-add-formal-power-series-Commutative-Semiring p q) + eq-coefficient-add-formal-power-series-Commutative-Semiring p q = refl + + htpy-coefficient-add-formal-power-series-Commutative-Semiring : + (p q : formal-power-series-Commutative-Semiring R) → + coefficient-formal-power-series-Commutative-Semiring + ( R) + ( add-formal-power-series-Commutative-Semiring p q) ~ + coefficient-add-formal-power-series-Commutative-Semiring p q + htpy-coefficient-add-formal-power-series-Commutative-Semiring p q n = refl +``` + +#### Commutativity + +```agda +module _ + {l : Level} (R : Commutative-Semiring l) + where + + opaque + unfolding add-formal-power-series-Commutative-Semiring + + commutative-add-formal-power-series-Commutative-Semiring : + (p q : formal-power-series-Commutative-Semiring R) → + add-formal-power-series-Commutative-Semiring R p q ＝ + add-formal-power-series-Commutative-Semiring R q p + commutative-add-formal-power-series-Commutative-Semiring p q = + commutative-mul-function-Commutative-Monoid + ( additive-commutative-monoid-Commutative-Semiring R) ℕ _ _ +``` + +#### Unit laws + +```agda +module _ + {l : Level} (R : Commutative-Semiring l) + where + + opaque + unfolding add-formal-power-series-Commutative-Semiring + unfolding zero-formal-power-series-Commutative-Semiring + + left-unit-law-add-formal-power-series-Commutative-Semiring : + (p : formal-power-series-Commutative-Semiring R) → + add-formal-power-series-Commutative-Semiring + ( R) + ( zero-formal-power-series-Commutative-Semiring R) + ( p) ＝ p + left-unit-law-add-formal-power-series-Commutative-Semiring = + left-unit-law-mul-function-Commutative-Monoid + ( additive-commutative-monoid-Commutative-Semiring R) + ( ℕ) + + right-unit-law-add-formal-power-series-Commutative-Semiring : + (p : formal-power-series-Commutative-Semiring R) → + add-formal-power-series-Commutative-Semiring + ( R) + ( p) + ( zero-formal-power-series-Commutative-Semiring R) ＝ p + right-unit-law-add-formal-power-series-Commutative-Semiring = + right-unit-law-mul-function-Commutative-Monoid + ( additive-commutative-monoid-Commutative-Semiring R) + ( ℕ) +``` + +#### Associativity + +```agda +module _ + {l : Level} (R : Commutative-Semiring l) + where + + opaque + unfolding formal-power-series-Commutative-Semiring + unfolding add-formal-power-series-Commutative-Semiring + + associative-add-formal-power-series-Commutative-Semiring : + (p q r : formal-power-series-Commutative-Semiring R) → + add-formal-power-series-Commutative-Semiring + ( R) + ( add-formal-power-series-Commutative-Semiring R p q) + ( r) ＝ + add-formal-power-series-Commutative-Semiring + ( R) + ( p) + ( add-formal-power-series-Commutative-Semiring R q r) + associative-add-formal-power-series-Commutative-Semiring = + associative-mul-function-Commutative-Monoid + ( additive-commutative-monoid-Commutative-Semiring R) + ( ℕ) +``` + +#### The additive commutative monoid of formal power series + +```agda +module _ + {l : Level} (R : Commutative-Semiring l) + where + + semigroup-add-formal-power-series-Commutative-Semiring : Semigroup l + semigroup-add-formal-power-series-Commutative-Semiring = + set-formal-power-series-Commutative-Semiring R , + add-formal-power-series-Commutative-Semiring R , + associative-add-formal-power-series-Commutative-Semiring R + + is-unital-add-formal-power-series-Commutative-Semiring : + is-unital (add-formal-power-series-Commutative-Semiring R) + is-unital-add-formal-power-series-Commutative-Semiring = + zero-formal-power-series-Commutative-Semiring R , + left-unit-law-add-formal-power-series-Commutative-Semiring R , + right-unit-law-add-formal-power-series-Commutative-Semiring R + + monoid-add-formal-power-series-Commutative-Semiring : Monoid l + monoid-add-formal-power-series-Commutative-Semiring = + semigroup-add-formal-power-series-Commutative-Semiring , + is-unital-add-formal-power-series-Commutative-Semiring + + commutative-monoid-add-formal-power-series-Commutative-Semiring : + Commutative-Monoid l + commutative-monoid-add-formal-power-series-Commutative-Semiring = + monoid-add-formal-power-series-Commutative-Semiring , + commutative-add-formal-power-series-Commutative-Semiring R +``` + +### Multiplication + +```agda +module _ + {l : Level} (R : Commutative-Semiring l) + (p q : formal-power-series-Commutative-Semiring R) + where + + coefficient-mul-formal-power-series-Commutative-Semiring : + ℕ → type-Commutative-Semiring R + coefficient-mul-formal-power-series-Commutative-Semiring n = + sum-finite-Commutative-Semiring + ( R) + ( finite-type-pair-with-sum-ℕ n) + ( λ (a , b , _) → + mul-Commutative-Semiring + ( R) + ( coefficient-formal-power-series-Commutative-Semiring R p a) + ( coefficient-formal-power-series-Commutative-Semiring R q b)) + + opaque + mul-formal-power-series-Commutative-Semiring : + formal-power-series-Commutative-Semiring R + mul-formal-power-series-Commutative-Semiring = + formal-power-series-coefficients-Commutative-Semiring + ( R) + ( coefficient-mul-formal-power-series-Commutative-Semiring) + + eq-coefficient-mul-formal-power-series-Commutative-Semiring : + coefficient-formal-power-series-Commutative-Semiring + ( R) + ( mul-formal-power-series-Commutative-Semiring) ~ + coefficient-mul-formal-power-series-Commutative-Semiring + eq-coefficient-mul-formal-power-series-Commutative-Semiring = + coefficient-formal-power-series-coefficients-Commutative-Semiring R _ +``` + +#### Commutativity + +```agda +module _ + {l : Level} (R : Commutative-Semiring l) + (p q : formal-power-series-Commutative-Semiring R) + where + + opaque + unfolding mul-formal-power-series-Commutative-Semiring + unfolding formal-power-series-Commutative-Semiring + + commutative-mul-formal-power-series-Commutative-Semiring : + mul-formal-power-series-Commutative-Semiring R p q ＝ + mul-formal-power-series-Commutative-Semiring R q p + commutative-mul-formal-power-series-Commutative-Semiring = + eq-htpy-coefficients-formal-power-series-Commutative-Semiring + ( R) + ( _) + ( _) + ( λ n → + htpy-sum-finite-Commutative-Semiring R _ + ( λ _ → commutative-mul-Commutative-Semiring R _ _) ∙ + sum-aut-finite-Commutative-Semiring + ( R) + ( _) + ( aut-swap-pair-with-sum-ℕ n) + ( _)) +``` + +#### Associativity + +```agda +module _ + {l : Level} (R : Commutative-Semiring l) + (p q r : formal-power-series-Commutative-Semiring R) + where + + abstract + associative-mul-formal-power-series-Commutative-Semiring : + mul-formal-power-series-Commutative-Semiring + ( R) + ( mul-formal-power-series-Commutative-Semiring R p q) + ( r) ＝ + mul-formal-power-series-Commutative-Semiring + ( R) + ( p) + ( mul-formal-power-series-Commutative-Semiring R q r) + associative-mul-formal-power-series-Commutative-Semiring = + eq-htpy-coefficients-formal-power-series-Commutative-Semiring + ( R) + ( _) + ( _) + ( λ n → equational-reasoning + coeff ((p *fps q) *fps r) n + ＝ + sum-finite-Commutative-Semiring + ( R) + ( finite-type-pair-with-sum-ℕ n) + ( λ (a , b , _) → coeff (p *fps q) a *R coeff r b) + by + eq-coefficient-mul-formal-power-series-Commutative-Semiring + ( R) + ( p *fps q) + ( r) + ( n) + ＝ + sum-finite-Commutative-Semiring + ( R) + ( finite-type-pair-with-sum-ℕ n) + ( λ (a , b , _) → + sum-finite-Commutative-Semiring + ( R) + ( finite-type-pair-with-sum-ℕ a) + ( λ (c , d , _) → (coeff p c *R coeff q d) *R coeff r b)) + by + ap + ( sum-finite-Commutative-Semiring + ( R) + ( finite-type-pair-with-sum-ℕ n)) + ( eq-htpy + ( λ (a , b , _) → + ap-mul-Commutative-Semiring + ( R) + ( eq-coefficient-mul-formal-power-series-Commutative-Semiring + ( R) + ( p) + ( q) + ( a)) + ( refl) ∙ + right-distributive-mul-sum-finite-Commutative-Semiring + ( R) + ( _) + ( _) + ( coeff r b))) + ＝ + sum-finite-Commutative-Semiring + ( R) + ( Σ-Finite-Type + ( finite-type-pair-with-sum-ℕ n) + ( finite-type-pair-with-sum-ℕ ∘ pr1)) + ( λ ((a , b , _) , c , d , _) → + (coeff p c *R coeff q d) *R coeff r b) + by + inv + ( sum-Σ-finite-Commutative-Semiring + ( R) + ( finite-type-pair-with-sum-ℕ n) + ( finite-type-pair-with-sum-ℕ ∘ pr1) + ( _)) + ＝ + sum-finite-Commutative-Semiring + ( R) + ( Σ-Finite-Type + ( finite-type-pair-with-sum-ℕ n) + ( finite-type-pair-with-sum-ℕ ∘ pr1 ∘ pr2)) + ( λ ((a , b , _) , c , d , _) → + (coeff p c *R coeff q d) *R coeff r a) + by + sum-equiv-finite-Commutative-Semiring R _ _ + ( equiv-pair-with-sum-pr1-pr2 n) + ( _) + ＝ + sum-finite-Commutative-Semiring + ( R) + ( Σ-Finite-Type + ( finite-type-pair-with-sum-ℕ n) + ( finite-type-pair-with-sum-ℕ ∘ pr1 ∘ pr2)) + ( λ ((a , b , _) , c , d , _) → + coeff p c *R (coeff q d *R coeff r a)) + by + ap + ( sum-finite-Commutative-Semiring R _) + ( eq-htpy (λ _ → associative-mul-Commutative-Semiring R _ _ _)) + ＝ + sum-finite-Commutative-Semiring + ( R) + ( Σ-Finite-Type + ( finite-type-pair-with-sum-ℕ n) + ( finite-type-pair-with-sum-ℕ ∘ pr1 ∘ pr2)) + ( λ ((a , b , _) , c , d , _) → + coeff p a *R (coeff q c *R coeff r d)) + by + sum-aut-finite-Commutative-Semiring + ( R) + ( Σ-Finite-Type + ( finite-type-pair-with-sum-ℕ n) + ( finite-type-pair-with-sum-ℕ ∘ pr1 ∘ pr2)) + ( equiv-permute-components-triple-with-sum-pr2 n) + ( _) + ＝ + sum-finite-Commutative-Semiring + ( R) + ( finite-type-pair-with-sum-ℕ n) + ( λ (a , b , _) → + sum-finite-Commutative-Semiring + ( R) + ( finite-type-pair-with-sum-ℕ b) + ( λ (c , d , _) → coeff p a *R (coeff q c *R coeff r d))) + by + sum-Σ-finite-Commutative-Semiring + ( R) + ( finite-type-pair-with-sum-ℕ n) + ( finite-type-pair-with-sum-ℕ ∘ pr1 ∘ pr2) + ( λ (a , b , _) (c , d , _) → + coeff p a *R (coeff q c *R coeff r d)) + ＝ + sum-finite-Commutative-Semiring + ( R) + ( finite-type-pair-with-sum-ℕ n) + ( λ (a , b , _) → + coeff p a *R coeff (q *fps r) b) + by + ap + ( sum-finite-Commutative-Semiring + ( R) + ( finite-type-pair-with-sum-ℕ n)) + ( eq-htpy + ( λ (a , b , _) → + inv + ( left-distributive-mul-sum-finite-Commutative-Semiring + ( R) + ( finite-type-pair-with-sum-ℕ b) + ( coeff p a) + ( _)) ∙ + ap + ( coeff p a *R_) + ( inv + ( eq-coefficient-mul-formal-power-series-Commutative-Semiring + ( R) + ( q) + ( r) + ( b))))) + ＝ coeff (p *fps (q *fps r)) n + by + inv + ( eq-coefficient-mul-formal-power-series-Commutative-Semiring + ( R) + ( p) + ( q *fps r) + ( n))) + where + _*R_ : + type-Commutative-Semiring R → type-Commutative-Semiring R → + type-Commutative-Semiring R + _*R_ = mul-Commutative-Semiring R + _*fps_ : + formal-power-series-Commutative-Semiring R → + formal-power-series-Commutative-Semiring R → + formal-power-series-Commutative-Semiring R + _*fps_ = mul-formal-power-series-Commutative-Semiring R + coeff : + formal-power-series-Commutative-Semiring R → ℕ → + type-Commutative-Semiring R + coeff = coefficient-formal-power-series-Commutative-Semiring R +``` + +#### Unit laws + +```agda +module _ + {l : Level} (R : Commutative-Semiring l) + (p : formal-power-series-Commutative-Semiring R) + where + + abstract + htpy-left-unit-law-mul-formal-power-series-Commutative-Semiring : + (p : ℕ → type-Commutative-Semiring R) (n : ℕ) → + sum-finite-Commutative-Semiring + ( R) + ( finite-type-pair-with-sum-ℕ n) + ( λ (a , b , _) → + mul-Commutative-Semiring + ( R) + ( coefficient-constant-formal-power-series-Commutative-Semiring + ( R) + ( one-Commutative-Semiring R) + ( a)) + ( p b)) ＝ + p n + htpy-left-unit-law-mul-formal-power-series-Commutative-Semiring p n = + equational-reasoning + sum-finite-Commutative-Semiring + ( R) + ( finite-type-pair-with-sum-ℕ n) + ( λ (a , b , _) → + mul-Commutative-Semiring + ( R) + ( coefficient-constant-formal-power-series-Commutative-Semiring + ( R) + ( one-Commutative-Semiring R) + ( a)) + ( p b)) + ＝ + sum-Commutative-Semiring + ( R) + ( succ-ℕ n) + ( λ { + (inr star) → + mul-Commutative-Semiring R (one-Commutative-Semiring R) (p n) ; + (inl k) → + mul-Commutative-Semiring R (zero-Commutative-Semiring R) _}) + by + sum-finite-count-Commutative-Semiring + ( R) + ( finite-type-pair-with-sum-ℕ n) + ( count-pair-with-sum-ℕ n) + ( _) + ＝ + add-Commutative-Semiring + ( R) + ( sum-Commutative-Semiring + ( R) + ( n) + ( λ k → + mul-Commutative-Semiring R (zero-Commutative-Semiring R) _)) + ( mul-Commutative-Semiring R (one-Commutative-Semiring R) (p n)) + by + cons-sum-Commutative-Semiring R n + ( λ { + (inr star) → + mul-Commutative-Semiring + ( R) + ( one-Commutative-Semiring R) + ( p n) ; + (inl k) → + mul-Commutative-Semiring R (zero-Commutative-Semiring R) _}) + ( refl) + ＝ + add-Commutative-Semiring + ( R) + ( sum-Commutative-Semiring + ( R) + ( n) + ( λ k → zero-Commutative-Semiring R)) + ( p n) + by + ap-add-Commutative-Semiring + ( R) + ( htpy-sum-Commutative-Semiring + ( R) + ( n) + ( λ k → left-zero-law-mul-Commutative-Semiring R _)) + ( left-unit-law-mul-Commutative-Semiring R _) + ＝ + add-Commutative-Semiring + ( R) + ( zero-Commutative-Semiring R) + ( p n) + by + ap-add-Commutative-Semiring + ( R) + ( sum-zero-Commutative-Semiring R n) + ( refl) + ＝ p n by left-unit-law-add-Commutative-Semiring R _ + + opaque + unfolding mul-formal-power-series-Commutative-Semiring + unfolding constant-formal-power-series-Commutative-Semiring + + left-unit-law-mul-formal-power-series-Commutative-Semiring : + mul-formal-power-series-Commutative-Semiring + ( R) + ( one-formal-power-series-Commutative-Semiring R) + ( p) ＝ p + left-unit-law-mul-formal-power-series-Commutative-Semiring = + eq-htpy-coefficients-formal-power-series-Commutative-Semiring + ( R) + ( _) + ( _) + ( htpy-left-unit-law-mul-formal-power-series-Commutative-Semiring p) + + right-unit-law-mul-formal-power-series-Commutative-Semiring : + mul-formal-power-series-Commutative-Semiring + ( R) + ( p) + ( one-formal-power-series-Commutative-Semiring R) ＝ p + right-unit-law-mul-formal-power-series-Commutative-Semiring = + commutative-mul-formal-power-series-Commutative-Semiring + ( R) + ( p) + ( one-formal-power-series-Commutative-Semiring R) ∙ + left-unit-law-mul-formal-power-series-Commutative-Semiring +``` + +#### Zero laws of multiplication + +```agda +module _ + {l : Level} (R : Commutative-Semiring l) + (p : formal-power-series-Commutative-Semiring R) + where + + opaque + unfolding mul-formal-power-series-Commutative-Semiring + unfolding zero-formal-power-series-Commutative-Semiring + + left-zero-law-mul-formal-power-series-Commutative-Semiring : + mul-formal-power-series-Commutative-Semiring + ( R) + ( zero-formal-power-series-Commutative-Semiring R) + ( p) ＝ + zero-formal-power-series-Commutative-Semiring R + left-zero-law-mul-formal-power-series-Commutative-Semiring = + eq-htpy-coefficients-formal-power-series-Commutative-Semiring + ( R) + ( _) + ( _) + ( λ n → + htpy-sum-finite-Commutative-Semiring R _ + ( λ _ → left-zero-law-mul-Commutative-Semiring R _) ∙ + sum-zero-finite-Commutative-Semiring R _) + + right-zero-law-mul-formal-power-series-Commutative-Semiring : + mul-formal-power-series-Commutative-Semiring + ( R) + ( p) + ( zero-formal-power-series-Commutative-Semiring R) ＝ + zero-formal-power-series-Commutative-Semiring R + right-zero-law-mul-formal-power-series-Commutative-Semiring = + commutative-mul-formal-power-series-Commutative-Semiring R _ _ ∙ + left-zero-law-mul-formal-power-series-Commutative-Semiring +``` + +#### Distributivity of multiplication over addition + +```agda +opaque + unfolding formal-power-series-Commutative-Semiring + unfolding add-formal-power-series-Commutative-Semiring + unfolding mul-formal-power-series-Commutative-Semiring + + left-distributive-mul-add-formal-power-series-Commutative-Semiring : + {l : Level} (R : Commutative-Semiring l) → + (p q r : formal-power-series-Commutative-Semiring R) → + mul-formal-power-series-Commutative-Semiring + ( R) + ( p) + ( add-formal-power-series-Commutative-Semiring R q r) ＝ + add-formal-power-series-Commutative-Semiring + ( R) + ( mul-formal-power-series-Commutative-Semiring R p q) + ( mul-formal-power-series-Commutative-Semiring R p r) + left-distributive-mul-add-formal-power-series-Commutative-Semiring R p q r = + eq-htpy-coefficients-formal-power-series-Commutative-Semiring + ( R) + ( _) + ( _) + ( λ n → + htpy-sum-finite-Commutative-Semiring R _ + ( λ _ → left-distributive-mul-add-Commutative-Semiring R _ _ _) ∙ + commute-sum-two-finite-Commutative-Semiring R _ _ _) + +abstract + right-distributive-mul-add-formal-power-series-Commutative-Semiring : + {l : Level} (R : Commutative-Semiring l) → + (p q r : formal-power-series-Commutative-Semiring R) → + mul-formal-power-series-Commutative-Semiring + ( R) + ( add-formal-power-series-Commutative-Semiring R p q) + ( r) ＝ + add-formal-power-series-Commutative-Semiring + ( R) + ( mul-formal-power-series-Commutative-Semiring R p r) + ( mul-formal-power-series-Commutative-Semiring R q r) + right-distributive-mul-add-formal-power-series-Commutative-Semiring R p q r = + commutative-mul-formal-power-series-Commutative-Semiring R _ _ ∙ + left-distributive-mul-add-formal-power-series-Commutative-Semiring R r p q ∙ + ap-binary + ( add-formal-power-series-Commutative-Semiring R) + ( commutative-mul-formal-power-series-Commutative-Semiring R r p) + ( commutative-mul-formal-power-series-Commutative-Semiring R r q) +``` + +### The commutative semiring of formal power series + +```agda +module _ + {l : Level} (R : Commutative-Semiring l) + where + + has-associative-mul-formal-power-series-Commutative-Semiring : + has-associative-mul (formal-power-series-Commutative-Semiring R) + has-associative-mul-formal-power-series-Commutative-Semiring = + mul-formal-power-series-Commutative-Semiring R , + associative-mul-formal-power-series-Commutative-Semiring R + + unit-laws-mul-formal-power-series-Commutative-Semiring : + unit-laws + ( mul-formal-power-series-Commutative-Semiring R) + ( one-formal-power-series-Commutative-Semiring R) + unit-laws-mul-formal-power-series-Commutative-Semiring = + left-unit-law-mul-formal-power-series-Commutative-Semiring R , + right-unit-law-mul-formal-power-series-Commutative-Semiring R + + is-unital-mul-formal-power-series-Commutative-Semiring : + is-unital (mul-formal-power-series-Commutative-Semiring R) + is-unital-mul-formal-power-series-Commutative-Semiring = + one-formal-power-series-Commutative-Semiring R , + unit-laws-mul-formal-power-series-Commutative-Semiring + + semiring-formal-power-series-Commutative-Semiring : Semiring l + semiring-formal-power-series-Commutative-Semiring = + commutative-monoid-add-formal-power-series-Commutative-Semiring R , + ( has-associative-mul-formal-power-series-Commutative-Semiring , + is-unital-mul-formal-power-series-Commutative-Semiring , + left-distributive-mul-add-formal-power-series-Commutative-Semiring R , + right-distributive-mul-add-formal-power-series-Commutative-Semiring R) , + left-zero-law-mul-formal-power-series-Commutative-Semiring R , + right-zero-law-mul-formal-power-series-Commutative-Semiring R + + commutative-semiring-formal-power-series-Commutative-Semiring : + Commutative-Semiring l + commutative-semiring-formal-power-series-Commutative-Semiring = + semiring-formal-power-series-Commutative-Semiring , + commutative-mul-formal-power-series-Commutative-Semiring R +``` diff --git a/src/commutative-algebra/sums-commutative-rings.lagda.md b/src/commutative-algebra/sums-commutative-rings.lagda.md index f26a86e6db..c66702d06d 100644 --- a/src/commutative-algebra/sums-commutative-rings.lagda.md +++ b/src/commutative-algebra/sums-commutative-rings.lagda.md @@ -8,12 +8,18 @@ module commutative-algebra.sums-commutative-rings where ```agda open import commutative-algebra.commutative-rings +open import commutative-algebra.sums-commutative-semirings open import elementary-number-theory.addition-natural-numbers open import elementary-number-theory.natural-numbers +open import finite-group-theory.permutations-standard-finite-types + open import foundation.action-on-identifications-functions +open import foundation.automorphisms open import foundation.coproduct-types +open import foundation.empty-types +open import foundation.equivalences open import foundation.function-types open import foundation.homotopies open import foundation.identity-types @@ -26,6 +32,9 @@ open import linear-algebra.vectors-on-commutative-rings open import ring-theory.sums-rings open import univalent-combinatorics.coproduct-types +open import univalent-combinatorics.counting +open import univalent-combinatorics.dependent-pair-types +open import univalent-combinatorics.finite-types open import univalent-combinatorics.standard-finite-types ``` @@ -33,8 +42,13 @@ open import univalent-combinatorics.standard-finite-types ## Idea -The **sum operation** extends the binary addition operation on a commutative -ring `A` to any family of elements of `A` indexed by a standard finite type. +The +{{#concept "sum operation" Disambiguation="in a commutative ring" WD="sum" WDID=Q218005 Agda=sum-Commutative-Ring}} +extends the binary addition operation on a +[commutative ring](commutative-algebra.commutative-rings.md) `A` to any family +of elements of `A` indexed by a +[standard finite type](univalent-combinatorics.standard-finite-types.md), or by +a [finite type](univalent-combinatorics.finite-types.md). ## Definition @@ -43,6 +57,17 @@ sum-Commutative-Ring : {l : Level} (A : Commutative-Ring l) (n : ℕ) → (functional-vec-Commutative-Ring A n) → type-Commutative-Ring A sum-Commutative-Ring A = sum-Ring (ring-Commutative-Ring A) + +sum-count-Commutative-Ring : + {l1 l2 : Level} (R : Commutative-Ring l1) (A : UU l2) → count A → + (A → type-Commutative-Ring R) → type-Commutative-Ring R +sum-count-Commutative-Ring R = sum-count-Ring (ring-Commutative-Ring R) + +sum-finite-Commutative-Ring : + {l1 l2 : Level} (R : Commutative-Ring l1) (A : Finite-Type l2) → + (type-Finite-Type A → type-Commutative-Ring R) → type-Commutative-Ring R +sum-finite-Commutative-Ring R = + sum-finite-Commutative-Semiring (commutative-semiring-Commutative-Ring R) ``` ## Properties @@ -60,6 +85,12 @@ module _ sum-one-element-Commutative-Ring = sum-one-element-Ring (ring-Commutative-Ring A) + sum-unit-finite-Commutative-Ring : + (f : unit → type-Commutative-Ring A) → + sum-finite-Commutative-Ring A unit-Finite-Type f ＝ f star + sum-unit-finite-Commutative-Ring = + sum-unit-finite-Ring (ring-Commutative-Ring A) + sum-two-elements-Commutative-Ring : (f : functional-vec-Commutative-Ring A 2) → sum-Commutative-Ring A 2 f ＝ @@ -72,13 +103,20 @@ module _ ```agda module _ - {l : Level} (A : Commutative-Ring l) + {l : Level} (R : Commutative-Ring l) where htpy-sum-Commutative-Ring : - (n : ℕ) {f g : functional-vec-Commutative-Ring A n} → - (f ~ g) → sum-Commutative-Ring A n f ＝ sum-Commutative-Ring A n g - htpy-sum-Commutative-Ring = htpy-sum-Ring (ring-Commutative-Ring A) + (n : ℕ) {f g : functional-vec-Commutative-Ring R n} → + (f ~ g) → sum-Commutative-Ring R n f ＝ sum-Commutative-Ring R n g + htpy-sum-Commutative-Ring = htpy-sum-Ring (ring-Commutative-Ring R) + + htpy-sum-finite-Commutative-Ring : + {l2 : Level} (A : Finite-Type l2) → + {f g : type-Finite-Type A → type-Commutative-Ring R} → (f ~ g) → + sum-finite-Commutative-Ring R A f ＝ sum-finite-Commutative-Ring R A g + htpy-sum-finite-Commutative-Ring = + htpy-sum-finite-Ring (ring-Commutative-Ring R) ``` ### Sums are equal to the zero-th term plus the rest @@ -110,24 +148,41 @@ module _ ```agda module _ - {l : Level} (A : Commutative-Ring l) + {l : Level} (R : Commutative-Ring l) where left-distributive-mul-sum-Commutative-Ring : - (n : ℕ) (x : type-Commutative-Ring A) - (f : functional-vec-Commutative-Ring A n) → - mul-Commutative-Ring A x (sum-Commutative-Ring A n f) ＝ - sum-Commutative-Ring A n (λ i → mul-Commutative-Ring A x (f i)) + (n : ℕ) (x : type-Commutative-Ring R) + (f : functional-vec-Commutative-Ring R n) → + mul-Commutative-Ring R x (sum-Commutative-Ring R n f) ＝ + sum-Commutative-Ring R n (λ i → mul-Commutative-Ring R x (f i)) left-distributive-mul-sum-Commutative-Ring = - left-distributive-mul-sum-Ring (ring-Commutative-Ring A) + left-distributive-mul-sum-Ring (ring-Commutative-Ring R) right-distributive-mul-sum-Commutative-Ring : - (n : ℕ) (f : functional-vec-Commutative-Ring A n) - (x : type-Commutative-Ring A) → - mul-Commutative-Ring A (sum-Commutative-Ring A n f) x ＝ - sum-Commutative-Ring A n (λ i → mul-Commutative-Ring A (f i) x) + (n : ℕ) (f : functional-vec-Commutative-Ring R n) + (x : type-Commutative-Ring R) → + mul-Commutative-Ring R (sum-Commutative-Ring R n f) x ＝ + sum-Commutative-Ring R n (λ i → mul-Commutative-Ring R (f i) x) right-distributive-mul-sum-Commutative-Ring = - right-distributive-mul-sum-Ring (ring-Commutative-Ring A) + right-distributive-mul-sum-Ring (ring-Commutative-Ring R) + + left-distributive-mul-sum-finite-Commutative-Ring : + {l2 : Level} (A : Finite-Type l2) (x : type-Commutative-Ring R) → + (f : type-Finite-Type A → type-Commutative-Ring R) → + mul-Commutative-Ring R x (sum-finite-Commutative-Ring R A f) ＝ + sum-finite-Commutative-Ring R A (mul-Commutative-Ring R x ∘ f) + left-distributive-mul-sum-finite-Commutative-Ring = + left-distributive-mul-sum-finite-Ring (ring-Commutative-Ring R) + + right-distributive-mul-sum-finite-Commutative-Ring : + {l2 : Level} (A : Finite-Type l2) → + (f : type-Finite-Type A → type-Commutative-Ring R) → + (x : type-Commutative-Ring R) → + mul-Commutative-Ring R (sum-finite-Commutative-Ring R A f) x ＝ + sum-finite-Commutative-Ring R A (mul-Commutative-Ring' R x ∘ f) + right-distributive-mul-sum-finite-Commutative-Ring = + right-distributive-mul-sum-finite-Ring (ring-Commutative-Ring R) ``` ### Interchange law of sums and addition in a commutative ring @@ -204,13 +259,136 @@ split-sum-Commutative-Ring A n (succ-ℕ m) f = ```agda module _ - {l : Level} (A : Commutative-Ring l) + {l : Level} (R : Commutative-Ring l) where sum-zero-Commutative-Ring : (n : ℕ) → - sum-Commutative-Ring A n - ( zero-functional-vec-Commutative-Ring A n) ＝ - zero-Commutative-Ring A - sum-zero-Commutative-Ring = sum-zero-Ring (ring-Commutative-Ring A) + sum-Commutative-Ring R n + ( zero-functional-vec-Commutative-Ring R n) ＝ + zero-Commutative-Ring R + sum-zero-Commutative-Ring = sum-zero-Ring (ring-Commutative-Ring R) + + sum-zero-finite-Commutative-Ring : + {l2 : Level} (A : Finite-Type l2) → + sum-finite-Commutative-Ring R A (λ _ → zero-Commutative-Ring R) ＝ + zero-Commutative-Ring R + sum-zero-finite-Commutative-Ring = + sum-zero-finite-Ring (ring-Commutative-Ring R) +``` + +### Permutations preserve sums + +```agda +module _ + {l : Level} (A : Commutative-Ring l) + where + + preserves-sum-permutation-Commutative-Ring : + (n : ℕ) → (σ : Permutation n) → + (f : functional-vec-Commutative-Ring A n) → + sum-Commutative-Ring A n f ＝ sum-Commutative-Ring A n (f ∘ map-equiv σ) + preserves-sum-permutation-Commutative-Ring = + preserves-sum-permutation-Commutative-Semiring + ( commutative-semiring-Commutative-Ring A) +``` + +### Sums over finite types are preserved by equivalences + +```agda +module _ + {l1 l2 l3 : Level} (R : Commutative-Ring l1) + (A : Finite-Type l2) (B : Finite-Type l3) (H : equiv-Finite-Type A B) + where + + sum-equiv-finite-Commutative-Ring : + (f : type-Finite-Type A → type-Commutative-Ring R) → + sum-finite-Commutative-Ring R A f ＝ + sum-finite-Commutative-Ring R B (f ∘ map-inv-equiv H) + sum-equiv-finite-Commutative-Ring = + sum-equiv-finite-Commutative-Semiring + ( commutative-semiring-Commutative-Ring R) + ( A) + ( B) + ( H) + +module _ + {l1 l2 : Level} (R : Commutative-Ring l1) + (A : Finite-Type l2) (σ : Aut (type-Finite-Type A)) + where + + sum-aut-finite-Commutative-Ring : + (f : type-Finite-Type A → type-Commutative-Ring R) → + sum-finite-Commutative-Ring R A f ＝ + sum-finite-Commutative-Ring R A (f ∘ map-equiv σ) + sum-aut-finite-Commutative-Ring = + sum-equiv-finite-Commutative-Ring R A A (inv-equiv σ) +``` + +### Sums over finite types distribute over coproducts + +```agda +module _ + {l1 l2 l3 : Level} (R : Commutative-Ring l1) + (A : Finite-Type l2) (B : Finite-Type l3) + where + + sum-coproduct-finite-Commutative-Ring : + (f : + type-Finite-Type A + type-Finite-Type B → type-Commutative-Ring R) → + sum-finite-Commutative-Ring R (coproduct-Finite-Type A B) f ＝ + add-Commutative-Ring + ( R) + ( sum-finite-Commutative-Ring R A (f ∘ inl)) + ( sum-finite-Commutative-Ring R B (f ∘ inr)) + sum-coproduct-finite-Commutative-Ring = + sum-coproduct-finite-Ring (ring-Commutative-Ring R) A B +``` + +### Sums distribute over dependent pair types + +```agda +module _ + {l1 l2 l3 : Level} (R : Commutative-Ring l1) + (A : Finite-Type l2) (B : type-Finite-Type A → Finite-Type l3) + where + + sum-Σ-finite-Commutative-Ring : + (f : + (a : type-Finite-Type A) → + type-Finite-Type (B a) → + type-Commutative-Ring R) → + sum-finite-Commutative-Ring R (Σ-Finite-Type A B) (ind-Σ f) ＝ + sum-finite-Commutative-Ring + R A (λ a → sum-finite-Commutative-Ring R (B a) (f a)) + sum-Σ-finite-Commutative-Ring = + sum-Σ-finite-Ring (ring-Commutative-Ring R) A B +``` + +### The sum over an empty type is zero + +```agda +module _ + {l1 l2 : Level} (R : Commutative-Ring l1) (A : Finite-Type l2) + (H : is-empty (type-Finite-Type A)) + where + + sum-is-empty-finite-Commutative-Ring : + (f : type-Finite-Type A → type-Commutative-Ring R) → + is-zero-Commutative-Ring R (sum-finite-Commutative-Ring R A f) + sum-is-empty-finite-Commutative-Ring = + sum-is-empty-finite-Ring (ring-Commutative-Ring R) A H +``` + +### The sum over a finite type is the sum over any count for that type + +```agda +sum-finite-count-Commutative-Ring : + {l1 l2 : Level} (R : Commutative-Ring l1) (A : Finite-Type l2) + (cA : count (type-Finite-Type A)) + (f : type-Finite-Type A → type-Commutative-Ring R) → + sum-finite-Commutative-Ring R A f ＝ + sum-count-Commutative-Ring R (type-Finite-Type A) cA f +sum-finite-count-Commutative-Ring R = + sum-finite-count-Ring (ring-Commutative-Ring R) ``` diff --git a/src/commutative-algebra/sums-commutative-semirings.lagda.md b/src/commutative-algebra/sums-commutative-semirings.lagda.md index 16eaf02de8..d640aa1973 100644 --- a/src/commutative-algebra/sums-commutative-semirings.lagda.md +++ b/src/commutative-algebra/sums-commutative-semirings.lagda.md @@ -12,17 +12,32 @@ open import commutative-algebra.commutative-semirings open import elementary-number-theory.addition-natural-numbers open import elementary-number-theory.natural-numbers +open import finite-group-theory.permutations-standard-finite-types + +open import foundation.automorphisms +open import foundation.coproduct-types +open import foundation.empty-types +open import foundation.equivalences open import foundation.function-types open import foundation.homotopies open import foundation.identity-types +open import foundation.negated-equality +open import foundation.type-arithmetic-cartesian-product-types +open import foundation.unit-type open import foundation.universe-levels open import linear-algebra.vectors open import linear-algebra.vectors-on-commutative-semirings +open import lists.lists + open import ring-theory.sums-semirings +open import univalent-combinatorics.cartesian-product-types open import univalent-combinatorics.coproduct-types +open import univalent-combinatorics.counting +open import univalent-combinatorics.dependent-pair-types +open import univalent-combinatorics.finite-types open import univalent-combinatorics.standard-finite-types ``` @@ -30,8 +45,13 @@ open import univalent-combinatorics.standard-finite-types ## Idea -The **sum operation** extends the binary addition operation on a commutative -semiring `R` to any family of elements of `R` indexed by a standard finite type. +The +{{#concept "sum operation" Disambiguation="in a commutative semiring" WD="sum" WDID=Q218005 Agda=sum-Commutative-Semiring}} +extends the binary addition operation on a +[commutative semiring](commutative-algebra.commutative-semirings.md) `R` to any +family of elements of `R` indexed by a +[standard finite type](univalent-combinatorics.standard-finite-types.md), or by +a [finite type](univalent-combinatorics.finite-types.md). ## Definition @@ -40,6 +60,19 @@ sum-Commutative-Semiring : {l : Level} (A : Commutative-Semiring l) (n : ℕ) → (functional-vec-Commutative-Semiring A n) → type-Commutative-Semiring A sum-Commutative-Semiring A = sum-Semiring (semiring-Commutative-Semiring A) + +sum-count-Commutative-Semiring : + {l1 l2 : Level} (R : Commutative-Semiring l1) (A : UU l2) → count A → + (A → type-Commutative-Semiring R) → type-Commutative-Semiring R +sum-count-Commutative-Semiring R = + sum-count-Semiring (semiring-Commutative-Semiring R) + +sum-finite-Commutative-Semiring : + {l1 l2 : Level} (R : Commutative-Semiring l1) (A : Finite-Type l2) → + (type-Finite-Type A → type-Commutative-Semiring R) → + type-Commutative-Semiring R +sum-finite-Commutative-Semiring R = + sum-finite-Semiring (semiring-Commutative-Semiring R) ``` ## Properties @@ -57,6 +90,12 @@ module _ sum-one-element-Commutative-Semiring = sum-one-element-Semiring (semiring-Commutative-Semiring A) + sum-unit-finite-Commutative-Semiring : + (f : unit → type-Commutative-Semiring A) → + sum-finite-Commutative-Semiring A unit-Finite-Type f ＝ f star + sum-unit-finite-Commutative-Semiring = + sum-unit-finite-Semiring (semiring-Commutative-Semiring A) + sum-two-elements-Commutative-Semiring : (f : functional-vec-Commutative-Semiring A 2) → sum-Commutative-Semiring A 2 f ＝ @@ -69,14 +108,22 @@ module _ ```agda module _ - {l : Level} (A : Commutative-Semiring l) + {l : Level} (R : Commutative-Semiring l) where htpy-sum-Commutative-Semiring : - (n : ℕ) {f g : functional-vec-Commutative-Semiring A n} → - (f ~ g) → sum-Commutative-Semiring A n f ＝ sum-Commutative-Semiring A n g + (n : ℕ) {f g : functional-vec-Commutative-Semiring R n} → + (f ~ g) → sum-Commutative-Semiring R n f ＝ sum-Commutative-Semiring R n g htpy-sum-Commutative-Semiring = - htpy-sum-Semiring (semiring-Commutative-Semiring A) + htpy-sum-Semiring (semiring-Commutative-Semiring R) + + htpy-sum-finite-Commutative-Semiring : + {l2 : Level} (A : Finite-Type l2) → + {f g : type-Finite-Type A → type-Commutative-Semiring R} → (f ~ g) → + sum-finite-Commutative-Semiring R A f ＝ + sum-finite-Commutative-Semiring R A g + htpy-sum-finite-Commutative-Semiring = + htpy-sum-finite-Semiring (semiring-Commutative-Semiring R) ``` ### Sums are equal to the zero-th term plus the rest @@ -110,24 +157,41 @@ module _ ```agda module _ - {l : Level} (A : Commutative-Semiring l) + {l : Level} (R : Commutative-Semiring l) where left-distributive-mul-sum-Commutative-Semiring : - (n : ℕ) (x : type-Commutative-Semiring A) - (f : functional-vec-Commutative-Semiring A n) → - mul-Commutative-Semiring A x (sum-Commutative-Semiring A n f) ＝ - sum-Commutative-Semiring A n (λ i → mul-Commutative-Semiring A x (f i)) + (n : ℕ) (x : type-Commutative-Semiring R) + (f : functional-vec-Commutative-Semiring R n) → + mul-Commutative-Semiring R x (sum-Commutative-Semiring R n f) ＝ + sum-Commutative-Semiring R n (λ i → mul-Commutative-Semiring R x (f i)) left-distributive-mul-sum-Commutative-Semiring = - left-distributive-mul-sum-Semiring (semiring-Commutative-Semiring A) + left-distributive-mul-sum-Semiring (semiring-Commutative-Semiring R) right-distributive-mul-sum-Commutative-Semiring : - (n : ℕ) (f : functional-vec-Commutative-Semiring A n) - (x : type-Commutative-Semiring A) → - mul-Commutative-Semiring A (sum-Commutative-Semiring A n f) x ＝ - sum-Commutative-Semiring A n (λ i → mul-Commutative-Semiring A (f i) x) + (n : ℕ) (f : functional-vec-Commutative-Semiring R n) + (x : type-Commutative-Semiring R) → + mul-Commutative-Semiring R (sum-Commutative-Semiring R n f) x ＝ + sum-Commutative-Semiring R n (λ i → mul-Commutative-Semiring R (f i) x) right-distributive-mul-sum-Commutative-Semiring = - right-distributive-mul-sum-Semiring (semiring-Commutative-Semiring A) + right-distributive-mul-sum-Semiring (semiring-Commutative-Semiring R) + + left-distributive-mul-sum-finite-Commutative-Semiring : + {l2 : Level} (A : Finite-Type l2) (x : type-Commutative-Semiring R) → + (f : type-Finite-Type A → type-Commutative-Semiring R) → + mul-Commutative-Semiring R x (sum-finite-Commutative-Semiring R A f) ＝ + sum-finite-Commutative-Semiring R A (mul-Commutative-Semiring R x ∘ f) + left-distributive-mul-sum-finite-Commutative-Semiring = + left-distributive-mul-sum-finite-Semiring (semiring-Commutative-Semiring R) + + right-distributive-mul-sum-finite-Commutative-Semiring : + {l2 : Level} (A : Finite-Type l2) → + (f : type-Finite-Type A → type-Commutative-Semiring R) → + (x : type-Commutative-Semiring R) → + mul-Commutative-Semiring R (sum-finite-Commutative-Semiring R A f) x ＝ + sum-finite-Commutative-Semiring R A (mul-Commutative-Semiring' R x ∘ f) + right-distributive-mul-sum-finite-Commutative-Semiring = + right-distributive-mul-sum-finite-Semiring (semiring-Commutative-Semiring R) ``` ### Interchange law of sums and addition in a commutative semiring @@ -188,16 +252,23 @@ module _ ```agda module _ - {l : Level} (A : Commutative-Semiring l) + {l : Level} (R : Commutative-Semiring l) where sum-zero-Commutative-Semiring : (n : ℕ) → - sum-Commutative-Semiring A n - ( zero-functional-vec-Commutative-Semiring A n) ＝ - zero-Commutative-Semiring A + sum-Commutative-Semiring R n + ( zero-functional-vec-Commutative-Semiring R n) ＝ + zero-Commutative-Semiring R sum-zero-Commutative-Semiring = - sum-zero-Semiring (semiring-Commutative-Semiring A) + sum-zero-Semiring (semiring-Commutative-Semiring R) + + sum-zero-finite-Commutative-Semiring : + {l2 : Level} (A : Finite-Type l2) → + sum-finite-Commutative-Semiring R A (λ _ → zero-Commutative-Semiring R) ＝ + zero-Commutative-Semiring R + sum-zero-finite-Commutative-Semiring = + sum-zero-finite-Semiring (semiring-Commutative-Semiring R) ``` ### Splitting sums @@ -213,3 +284,204 @@ split-sum-Commutative-Semiring : split-sum-Commutative-Semiring A = split-sum-Semiring (semiring-Commutative-Semiring A) ``` + +### Permutations preserve sums + +```agda +module _ + {l : Level} (R : Commutative-Semiring l) + where + + preserves-sum-permutation-Commutative-Semiring : + (n : ℕ) → (σ : Permutation n) → + (f : functional-vec-Commutative-Semiring R n) → + sum-Commutative-Semiring R n f ＝ + sum-Commutative-Semiring R n (f ∘ map-equiv σ) + preserves-sum-permutation-Commutative-Semiring = + preserves-sum-permutation-Semiring (semiring-Commutative-Semiring R) +``` + +### Sums over finite types are preserved by equivalences + +```agda +module _ + {l1 l2 l3 : Level} (R : Commutative-Semiring l1) + (A : Finite-Type l2) (B : Finite-Type l3) (H : equiv-Finite-Type A B) + where + + sum-equiv-finite-Commutative-Semiring : + (f : type-Finite-Type A → type-Commutative-Semiring R) → + sum-finite-Commutative-Semiring R A f ＝ + sum-finite-Commutative-Semiring R B (f ∘ map-inv-equiv H) + sum-equiv-finite-Commutative-Semiring = + sum-equiv-finite-Semiring (semiring-Commutative-Semiring R) A B H + +module _ + {l1 l2 : Level} (R : Commutative-Semiring l1) + (A : Finite-Type l2) (σ : Aut (type-Finite-Type A)) + where + + sum-aut-finite-Commutative-Semiring : + (f : type-Finite-Type A → type-Commutative-Semiring R) → + sum-finite-Commutative-Semiring R A f ＝ + sum-finite-Commutative-Semiring R A (f ∘ map-equiv σ) + sum-aut-finite-Commutative-Semiring = + sum-equiv-finite-Commutative-Semiring R A A (inv-equiv σ) +``` + +### Sums over finite types distribute over coproducts + +```agda +module _ + {l1 l2 l3 : Level} (R : Commutative-Semiring l1) + (A : Finite-Type l2) (B : Finite-Type l3) + where + + sum-coproduct-finite-Commutative-Semiring : + (f : + type-Finite-Type A + type-Finite-Type B → type-Commutative-Semiring R) → + sum-finite-Commutative-Semiring R (coproduct-Finite-Type A B) f ＝ + add-Commutative-Semiring + ( R) + ( sum-finite-Commutative-Semiring R A (f ∘ inl)) + ( sum-finite-Commutative-Semiring R B (f ∘ inr)) + sum-coproduct-finite-Commutative-Semiring = + sum-coproduct-finite-Semiring (semiring-Commutative-Semiring R) A B +``` + +### Sums distribute over dependent pair types + +```agda +module _ + {l1 l2 l3 : Level} (R : Commutative-Semiring l1) + (A : Finite-Type l2) (B : type-Finite-Type A → Finite-Type l3) + where + + sum-Σ-finite-Commutative-Semiring : + (f : + (a : type-Finite-Type A) → + type-Finite-Type (B a) → + type-Commutative-Semiring R) → + sum-finite-Commutative-Semiring R (Σ-Finite-Type A B) (ind-Σ f) ＝ + sum-finite-Commutative-Semiring + R A (λ a → sum-finite-Commutative-Semiring R (B a) (f a)) + sum-Σ-finite-Commutative-Semiring = + sum-Σ-finite-Semiring (semiring-Commutative-Semiring R) A B +``` + +### The sum over an empty type is zero + +```agda +module _ + {l1 l2 : Level} (R : Commutative-Semiring l1) (A : Finite-Type l2) + (H : is-empty (type-Finite-Type A)) + where + + sum-is-empty-finite-Commutative-Semiring : + (f : type-Finite-Type A → type-Commutative-Semiring R) → + is-zero-Commutative-Semiring R (sum-finite-Commutative-Semiring R A f) + sum-is-empty-finite-Commutative-Semiring = + sum-is-empty-finite-Semiring (semiring-Commutative-Semiring R) A H +``` + +### The sum over a finite type is the sum over any count for that type + +```agda +sum-finite-count-Commutative-Semiring : + {l1 l2 : Level} (R : Commutative-Semiring l1) (A : Finite-Type l2) + (cA : count (type-Finite-Type A)) + (f : type-Finite-Type A → type-Commutative-Semiring R) → + sum-finite-Commutative-Semiring R A f ＝ + sum-count-Commutative-Semiring R (type-Finite-Type A) cA f +sum-finite-count-Commutative-Semiring R = + sum-finite-count-Semiring (semiring-Commutative-Semiring R) +``` + +### Commuting sums + +```agda +module _ + {l1 l2 : Level} (R : Commutative-Semiring l1) (A : Finite-Type l2) + where + + commute-sum-two-finite-Commutative-Semiring : + (f g : type-Finite-Type A → type-Commutative-Semiring R) → + sum-finite-Commutative-Semiring R A + (λ a → add-Commutative-Semiring R (f a) (g a)) ＝ + add-Commutative-Semiring R + (sum-finite-Commutative-Semiring R A f) + (sum-finite-Commutative-Semiring R A g) + commute-sum-two-finite-Commutative-Semiring f g = equational-reasoning + sum-finite-Commutative-Semiring R A + ( λ a → add-Commutative-Semiring R (f a) (g a)) + ＝ + sum-finite-Commutative-Semiring + ( R) + ( A) + ( λ a → sum-Commutative-Semiring R 2 (h a)) + by + htpy-sum-finite-Commutative-Semiring + ( R) + ( A) + ( λ a → inv (sum-two-elements-Commutative-Semiring R (h a))) + ＝ + sum-finite-Commutative-Semiring + ( R) + ( A) + ( λ a → + sum-finite-Commutative-Semiring R (Fin-Finite-Type 2) (h a)) + by + htpy-sum-finite-Commutative-Semiring R A + ( λ a → + inv + ( sum-finite-count-Commutative-Semiring + ( R) + ( Fin-Finite-Type 2) + ( count-Fin 2) + ( h a))) + ＝ + sum-finite-Commutative-Semiring + ( R) + ( Σ-Finite-Type A (λ _ → Fin-Finite-Type 2)) + ( ind-Σ h) + by inv (sum-Σ-finite-Commutative-Semiring R A (λ _ → Fin-Finite-Type 2) h) + ＝ + sum-finite-Commutative-Semiring + ( R) + ( Σ-Finite-Type (Fin-Finite-Type 2) (λ _ → A)) + ( λ (i , a) → h a i) + by + sum-equiv-finite-Commutative-Semiring R _ _ + ( commutative-product) + ( ind-Σ h) + ＝ + sum-finite-Commutative-Semiring + ( R) + ( Fin-Finite-Type 2) + ( λ i → sum-finite-Commutative-Semiring R A (λ a → h a i)) + by sum-Σ-finite-Commutative-Semiring R _ _ _ + ＝ + sum-Commutative-Semiring + ( R) + ( 2) + ( λ i → sum-finite-Commutative-Semiring R A (λ a → h a i)) + by + sum-finite-count-Commutative-Semiring + ( R) + ( Fin-Finite-Type 2) + ( count-Fin 2) + ( _) + ＝ + add-Commutative-Semiring + ( R) + ( sum-finite-Commutative-Semiring R A f) + ( sum-finite-Commutative-Semiring R A g) + by + sum-two-elements-Commutative-Semiring + ( R) + ( λ i → sum-finite-Commutative-Semiring R A (λ a → h a i)) + where + h : type-Finite-Type A → Fin 2 → type-Commutative-Semiring R + h a (inl (inr _)) = f a + h a (inr _) = g a +``` diff --git a/src/elementary-number-theory.lagda.md b/src/elementary-number-theory.lagda.md index 8d04d1a4f3..c751026403 100644 --- a/src/elementary-number-theory.lagda.md +++ b/src/elementary-number-theory.lagda.md @@ -136,6 +136,7 @@ open import elementary-number-theory.nonzero-integers public open import elementary-number-theory.nonzero-natural-numbers public open import elementary-number-theory.nonzero-rational-numbers public open import elementary-number-theory.ordinal-induction-natural-numbers public +open import elementary-number-theory.pairs-with-natural-sums public open import elementary-number-theory.parity-natural-numbers public open import elementary-number-theory.peano-arithmetic public open import elementary-number-theory.pisano-periods public diff --git a/src/elementary-number-theory/equality-natural-numbers.lagda.md b/src/elementary-number-theory/equality-natural-numbers.lagda.md index bb335e5e58..c3d5e54b9c 100644 --- a/src/elementary-number-theory/equality-natural-numbers.lagda.md +++ b/src/elementary-number-theory/equality-natural-numbers.lagda.md @@ -19,6 +19,7 @@ open import foundation.equivalences open import foundation.function-types open import foundation.fundamental-theorem-of-identity-types open import foundation.identity-types +open import foundation.negation open import foundation.propositions open import foundation.set-truncations open import foundation.sets @@ -93,6 +94,17 @@ pr1 (is-zero-ℕ-Prop n) = is-zero-ℕ n pr2 (is-zero-ℕ-Prop n) = is-prop-is-zero-ℕ n ``` +### The property of being nonzero + +```agda +is-prop-is-nonzero-ℕ : (n : ℕ) → is-prop (is-nonzero-ℕ n) +is-prop-is-nonzero-ℕ n = is-prop-neg + +is-nonzero-ℕ-Prop : ℕ → Prop lzero +pr1 (is-nonzero-ℕ-Prop n) = is-nonzero-ℕ n +pr2 (is-nonzero-ℕ-Prop n) = is-prop-is-nonzero-ℕ n +``` + ### The property of being one ```agda diff --git a/src/elementary-number-theory/pairs-with-natural-sums.lagda.md b/src/elementary-number-theory/pairs-with-natural-sums.lagda.md new file mode 100644 index 0000000000..96f863f4db --- /dev/null +++ b/src/elementary-number-theory/pairs-with-natural-sums.lagda.md @@ -0,0 +1,290 @@ +# Pairs of natural numbers with a given sum + +```agda +module elementary-number-theory.pairs-with-natural-sums where +``` + +
Imports + +```agda +open import elementary-number-theory.addition-natural-numbers +open import elementary-number-theory.equality-natural-numbers +open import elementary-number-theory.inequality-natural-numbers +open import elementary-number-theory.natural-numbers + +open import foundation.action-on-identifications-functions +open import foundation.automorphisms +open import foundation.cartesian-product-types +open import foundation.complements-subtypes +open import foundation.conjunction +open import foundation.contractible-types +open import foundation.coproduct-types +open import foundation.decidable-subtypes +open import foundation.dependent-pair-types +open import foundation.equality-dependent-pair-types +open import foundation.equivalences +open import foundation.function-types +open import foundation.functoriality-coproduct-types +open import foundation.identity-types +open import foundation.involutions +open import foundation.negation +open import foundation.propositions +open import foundation.retractions +open import foundation.sections +open import foundation.sets +open import foundation.subtypes +open import foundation.type-arithmetic-coproduct-types +open import foundation.unit-type +open import foundation.universe-levels + +open import logic.complements-decidable-subtypes + +open import univalent-combinatorics.counting +open import univalent-combinatorics.finite-types +open import univalent-combinatorics.standard-finite-types +``` + +
+ +## Idea + +A pair of natural numbers with a specific known sum resembles an +[integer partition](elementary-number-theory.integer-partitions.md), but is +ordered, and the components may be zero. + +## Definition + +```agda +pair-with-sum-ℕ : ℕ → UU lzero +pair-with-sum-ℕ n = Σ ℕ ( λ a → Σ ℕ (λ b → b +ℕ a ＝ n)) +``` + +## Properties + +### Equality characterization + +```agda +module _ + (n : ℕ) + where + + Eq-pair-with-sum-ℕ : pair-with-sum-ℕ n → pair-with-sum-ℕ n → UU lzero + Eq-pair-with-sum-ℕ (a , b , _) (a' , b' , _) = a ＝ a' + + is-prop-Eq-pair-with-sum-ℕ : + (x y : pair-with-sum-ℕ n) → is-prop (Eq-pair-with-sum-ℕ x y) + is-prop-Eq-pair-with-sum-ℕ (a , _) (a' , _) = + is-prop-type-Prop (Id-Prop ℕ-Set a a') + + refl-Eq-pair-with-sum-ℕ : (x : pair-with-sum-ℕ n) → Eq-pair-with-sum-ℕ x x + refl-Eq-pair-with-sum-ℕ _ = refl + + eq-Eq-pair-with-sum-ℕ : + (x y : pair-with-sum-ℕ n) → Eq-pair-with-sum-ℕ x y → x ＝ y + eq-Eq-pair-with-sum-ℕ (a , b , b+a=n) (.a , b' , b'+a=n) refl = + eq-pair-eq-fiber + ( eq-pair-Σ + ( is-injective-right-add-ℕ a (b+a=n ∙ inv b'+a=n)) + ( eq-type-Prop (Id-Prop ℕ-Set _ _))) + + abstract + is-set-pair-with-sum-ℕ : is-set (pair-with-sum-ℕ n) + is-set-pair-with-sum-ℕ = + is-set-prop-in-id + Eq-pair-with-sum-ℕ + is-prop-Eq-pair-with-sum-ℕ + refl-Eq-pair-with-sum-ℕ + eq-Eq-pair-with-sum-ℕ + + set-pair-with-sum-ℕ : Set lzero + set-pair-with-sum-ℕ = pair-with-sum-ℕ n , is-set-pair-with-sum-ℕ +``` + +### Involution of swapping the components + +```agda +module _ + (n : ℕ) + where + + swap-pair-with-sum-ℕ : pair-with-sum-ℕ n → pair-with-sum-ℕ n + swap-pair-with-sum-ℕ (a , b , b+a=n) = + (b , a , commutative-add-ℕ a b ∙ b+a=n) + + is-involution-swap-pair-with-sum-ℕ : is-involution swap-pair-with-sum-ℕ + is-involution-swap-pair-with-sum-ℕ _ = eq-Eq-pair-with-sum-ℕ n _ _ refl + + aut-swap-pair-with-sum-ℕ : Aut (pair-with-sum-ℕ n) + aut-swap-pair-with-sum-ℕ = + swap-pair-with-sum-ℕ , + is-equiv-is-involution is-involution-swap-pair-with-sum-ℕ +``` + +### Equivalence of dependent pairs further partitioning a component + +```agda +module _ + (n : ℕ) + where + + map-equiv-pair-with-sum-pr1-pr2 : + Σ (pair-with-sum-ℕ n) (pair-with-sum-ℕ ∘ pr1) → + Σ (pair-with-sum-ℕ n) (pair-with-sum-ℕ ∘ pr1 ∘ pr2) + pr1 (map-equiv-pair-with-sum-pr1-pr2 ((p , c , c+p=n) , _)) = + (c , p , commutative-add-ℕ p c ∙ c+p=n) + pr2 (map-equiv-pair-with-sum-pr1-pr2 (_ , y)) = y + + map-inv-equiv-pair-with-sum-pr1-pr2 : + Σ (pair-with-sum-ℕ n) (pair-with-sum-ℕ ∘ pr1 ∘ pr2) → + Σ (pair-with-sum-ℕ n) (pair-with-sum-ℕ ∘ pr1) + pr1 (map-inv-equiv-pair-with-sum-pr1-pr2 ((c , p , p+c=n) , _)) = + (p , c , commutative-add-ℕ c p ∙ p+c=n) + pr2 (map-inv-equiv-pair-with-sum-pr1-pr2 (_ , y)) = y + + abstract + is-section-map-inv-equiv-pair-with-sum-pr1-pr2 : + is-section + map-equiv-pair-with-sum-pr1-pr2 + map-inv-equiv-pair-with-sum-pr1-pr2 + is-section-map-inv-equiv-pair-with-sum-pr1-pr2 + x@((c , p , p+c=n) , a , b , b+a=p) = + inv + ( ind-Id + ( p+c=n) + ( λ H' H=H' → x ＝ ((c , p , H') , a , b , b+a=p)) + ( refl) + ( _) + ( eq-type-Prop (Id-Prop ℕ-Set _ _))) + + is-retraction-map-inv-equiv-pair-with-sum-pr1-pr2 : + is-retraction + map-equiv-pair-with-sum-pr1-pr2 + map-inv-equiv-pair-with-sum-pr1-pr2 + is-retraction-map-inv-equiv-pair-with-sum-pr1-pr2 + x@((p , c , c+p=n) , a , b , b+a=p) = + inv + ( ind-Id + ( c+p=n) + ( λ H' H=H' → x ＝ ((p , c , H') , a , b , b+a=p)) + ( refl) + ( _) + ( eq-type-Prop (Id-Prop ℕ-Set _ _))) + + equiv-pair-with-sum-pr1-pr2 : + Σ (pair-with-sum-ℕ n) (pair-with-sum-ℕ ∘ pr1) ≃ + Σ (pair-with-sum-ℕ n) (pair-with-sum-ℕ ∘ pr1 ∘ pr2) + equiv-pair-with-sum-pr1-pr2 = + map-equiv-pair-with-sum-pr1-pr2 , + ( map-inv-equiv-pair-with-sum-pr1-pr2 , + is-section-map-inv-equiv-pair-with-sum-pr1-pr2) , + ( map-inv-equiv-pair-with-sum-pr1-pr2 , + is-retraction-map-inv-equiv-pair-with-sum-pr1-pr2) +``` + +### Pairs with a fixed sum are a finite type + +```agda +module _ + (n : ℕ) + where + + equiv-pair-with-sum-leq-ℕ : + Σ ℕ (λ k → leq-ℕ k n) ≃ pair-with-sum-ℕ n + equiv-pair-with-sum-leq-ℕ = + ( λ (k , k≤n) → k , subtraction-leq-ℕ k n k≤n) , + ((λ (k , l , l+k=n) → k , leq-subtraction-ℕ k n l l+k=n) , + λ (k , l , l+k=n) → + let + (l' , l'+k=n) = + subtraction-leq-ℕ k n (leq-subtraction-ℕ k n l l+k=n) + in + eq-pair-eq-fiber + ( eq-pair-Σ + ( is-injective-right-add-ℕ k (l'+k=n ∙ inv l+k=n)) + ( eq-type-Prop (Id-Prop ℕ-Set (l +ℕ k) n)))) , + (( λ (k , l , l+k=n) → k , leq-subtraction-ℕ k n l l+k=n) , + (λ (k , k≤n) → eq-pair-eq-fiber (eq-type-Prop (leq-ℕ-Prop k n)))) + + count-pair-with-sum-ℕ : count (pair-with-sum-ℕ n) + count-pair-with-sum-ℕ = + succ-ℕ n , equiv-pair-with-sum-leq-ℕ ∘e equiv-fin-succ-leq-ℕ n + + finite-type-pair-with-sum-ℕ : Finite-Type lzero + finite-type-pair-with-sum-ℕ = + pair-with-sum-ℕ n , + is-finite-count count-pair-with-sum-ℕ +``` + +### Permuting components in a triple of sums + +```agda +module _ + (n : ℕ) + where + + map-equiv-permute-components-triple-with-sum-pr2 : + Σ (pair-with-sum-ℕ n) (pair-with-sum-ℕ ∘ pr1 ∘ pr2) → + Σ (pair-with-sum-ℕ n) (pair-with-sum-ℕ ∘ pr1 ∘ pr2) + map-equiv-permute-components-triple-with-sum-pr2 + ((c , p , p+c=n) , a , b , b+a=p) = + ( b , a +ℕ c , + ( equational-reasoning + (a +ℕ c) +ℕ b + ＝ b +ℕ (a +ℕ c) by commutative-add-ℕ (a +ℕ c) b + ＝ (b +ℕ a) +ℕ c by inv (associative-add-ℕ b a c) + ＝ p +ℕ c by ap (_+ℕ c) b+a=p + ＝ n by p+c=n)) , + c , a , refl + + map-inv-equiv-permute-components-triple-with-sum-pr2 : + Σ (pair-with-sum-ℕ n) (pair-with-sum-ℕ ∘ pr1 ∘ pr2) → + Σ (pair-with-sum-ℕ n) (pair-with-sum-ℕ ∘ pr1 ∘ pr2) + map-inv-equiv-permute-components-triple-with-sum-pr2 + ((c , p , p+c=n) , a , b , b+a=p) = + ( a , c +ℕ b , + ( equational-reasoning + (c +ℕ b) +ℕ a + ＝ c +ℕ (b +ℕ a) by associative-add-ℕ c b a + ＝ c +ℕ p by ap (c +ℕ_) b+a=p + ＝ p +ℕ c by commutative-add-ℕ c p + ＝ n by p+c=n)) , + b , c , refl + + abstract + is-section-map-inv-equiv-permute-components-triple-with-sum-pr2 : + is-section + map-equiv-permute-components-triple-with-sum-pr2 + map-inv-equiv-permute-components-triple-with-sum-pr2 + is-section-map-inv-equiv-permute-components-triple-with-sum-pr2 + x@((c , .(b +ℕ a) , p+c=n) , a , b , refl) = + inv + ( ind-Id + ( p+c=n) + ( λ H' H=H' → x ＝ ((c , b +ℕ a , H') , a , b , refl)) + ( refl) + ( _) + ( eq-type-Prop (Id-Prop ℕ-Set _ _))) + + is-retraction-map-inv-equiv-permute-components-triple-with-sum-pr2 : + is-retraction + map-equiv-permute-components-triple-with-sum-pr2 + map-inv-equiv-permute-components-triple-with-sum-pr2 + is-retraction-map-inv-equiv-permute-components-triple-with-sum-pr2 + x@((c , .(b +ℕ a) , p+c=n) , a , b , refl) = + inv + ( ind-Id + ( p+c=n) + ( λ H' H=H' → x ＝ ((c , b +ℕ a , H') , a , b , refl)) + ( refl) + ( _) + ( eq-type-Prop (Id-Prop ℕ-Set _ _))) + + equiv-permute-components-triple-with-sum-pr2 : + Aut (Σ (pair-with-sum-ℕ n) (pair-with-sum-ℕ ∘ pr1 ∘ pr2)) + equiv-permute-components-triple-with-sum-pr2 = + map-equiv-permute-components-triple-with-sum-pr2 , + ( ( map-inv-equiv-permute-components-triple-with-sum-pr2 , + is-section-map-inv-equiv-permute-components-triple-with-sum-pr2) , + ( map-inv-equiv-permute-components-triple-with-sum-pr2 , + is-retraction-map-inv-equiv-permute-components-triple-with-sum-pr2)) +``` diff --git a/src/elementary-number-theory/strict-inequality-natural-numbers.lagda.md b/src/elementary-number-theory/strict-inequality-natural-numbers.lagda.md index 623bc26c65..95445f132a 100644 --- a/src/elementary-number-theory/strict-inequality-natural-numbers.lagda.md +++ b/src/elementary-number-theory/strict-inequality-natural-numbers.lagda.md @@ -20,12 +20,16 @@ open import foundation.coproduct-types open import foundation.decidable-types open import foundation.dependent-pair-types open import foundation.empty-types +open import foundation.equality-dependent-pair-types +open import foundation.equivalences open import foundation.function-types open import foundation.functoriality-coproduct-types open import foundation.identity-types open import foundation.negated-equality open import foundation.negation open import foundation.propositions +open import foundation.retractions +open import foundation.sections open import foundation.transport-along-identifications open import foundation.unit-type open import foundation.universe-levels @@ -308,6 +312,19 @@ le-succ-leq-ℕ zero-ℕ y H = star le-succ-leq-ℕ (succ-ℕ x) (succ-ℕ y) H = le-succ-leq-ℕ x y H ``` +### There is an equivalence between natural numbers less than `succ-ℕ n` and natural numbers less than or equal to `n` + +```agda +equiv-le-succ-ℕ-leq-ℕ : + (n : ℕ) → Σ ℕ (λ k → le-ℕ k (succ-ℕ n)) ≃ Σ ℕ (λ k → leq-ℕ k n) +equiv-le-succ-ℕ-leq-ℕ n = + ( λ (k , kImports ```agda +open import foundation.action-on-identifications-functions +open import foundation.coproduct-types open import foundation.decidable-subtypes open import foundation.dependent-pair-types +open import foundation.disjoint-subtypes open import foundation.disjunction +open import foundation.empty-types +open import foundation.equivalences +open import foundation.functoriality-dependent-pair-types open import foundation.large-locale-of-subtypes +open import foundation.logical-equivalences open import foundation.powersets open import foundation.propositional-truncations +open import foundation.propositions +open import foundation.type-arithmetic-coproduct-types open import foundation.universe-levels open import foundation-core.subtypes @@ -101,3 +110,56 @@ module _ ( union-family-of-subtypes B x) ( λ (i , q) → unit-trunc-Prop (i , H i x q)) ``` + +### The union of disjoint subtypes is equivalent to their coproduct + +```agda +module _ + {l1 l2 l3 : Level} {X : UU l1} (A : subtype l2 X) (B : subtype l3 X) + (H : disjoint-subtype A B) + where + + all-elements-equal-coproduct-disjoint-prop : + (x : X) → all-elements-equal (type-Prop (A x) + type-Prop (B x)) + all-elements-equal-coproduct-disjoint-prop x (inl _) (inl _) = + ap inl (eq-type-Prop (A x)) + all-elements-equal-coproduct-disjoint-prop x (inr _) (inr _) = + ap inr (eq-type-Prop (B x)) + all-elements-equal-coproduct-disjoint-prop x (inl ax) (inr bx) = + ex-falso (H x (ax , bx)) + all-elements-equal-coproduct-disjoint-prop x (inr bx) (inl ax) = + ex-falso (H x (ax , bx)) + + is-prop-coproduct-disjoint-prop : + (x : X) → is-prop (type-Prop (A x) + type-Prop (B x)) + is-prop-coproduct-disjoint-prop x = + is-prop-all-elements-equal (all-elements-equal-coproduct-disjoint-prop x) + + subtype-coproduct-disjoint-subtype : subtype (l2 ⊔ l3) X + subtype-coproduct-disjoint-subtype x = + type-Prop (A x) + type-Prop (B x) , is-prop-coproduct-disjoint-prop x + + iff-disjunction-coproduct-disjoint-subtype : + (x : X) → type-iff-Prop (A x ∨ B x) (subtype-coproduct-disjoint-subtype x) + pr1 (iff-disjunction-coproduct-disjoint-subtype x) = + elim-disjunction (subtype-coproduct-disjoint-subtype x) inl inr + pr2 (iff-disjunction-coproduct-disjoint-subtype x) = + rec-coproduct inl-disjunction inr-disjunction + + equiv-union-subtype-coproduct-disjoint-subtype : + type-subtype (union-subtype A B) ≃ + type-subtype subtype-coproduct-disjoint-subtype + equiv-union-subtype-coproduct-disjoint-subtype = + equiv-tot + ( λ x → + equiv-iff' + ( A x ∨ B x) + ( subtype-coproduct-disjoint-subtype x) + ( iff-disjunction-coproduct-disjoint-subtype x)) + + equiv-union-coproduct-disjoint-subtype : + type-subtype (union-subtype A B) ≃ type-subtype A + type-subtype B + equiv-union-coproduct-disjoint-subtype = + left-distributive-Σ-coproduct X (is-in-subtype A) (is-in-subtype B) ∘e + equiv-union-subtype-coproduct-disjoint-subtype +``` diff --git a/src/group-theory.lagda.md b/src/group-theory.lagda.md index 6d7a7e8e31..4273264e24 100644 --- a/src/group-theory.lagda.md +++ b/src/group-theory.lagda.md @@ -157,6 +157,7 @@ open import group-theory.principal-group-actions public open import group-theory.principal-torsors-concrete-groups public open import group-theory.products-of-elements-monoids public open import group-theory.products-of-tuples-of-elements-commutative-monoids public +open import group-theory.products-of-tuples-of-elements-monoids public open import group-theory.pullbacks-subgroups public open import group-theory.pullbacks-subsemigroups public open import group-theory.quotient-groups public diff --git a/src/group-theory/function-commutative-monoids.lagda.md b/src/group-theory/function-commutative-monoids.lagda.md index 57b44087dc..a86b1a44b5 100644 --- a/src/group-theory/function-commutative-monoids.lagda.md +++ b/src/group-theory/function-commutative-monoids.lagda.md @@ -20,7 +20,7 @@ open import group-theory.monoids ## Idea -Given a commutative monoid `M` and a type `X`, the function commuative monoid +Given a commutative monoid `M` and a type `X`, the function commutative monoid `M^X` consists of functions from `X` to the underlying type of `M`. The multiplicative operation and the unit are given pointwise. diff --git a/src/group-theory/products-of-tuples-of-elements-commutative-monoids.lagda.md b/src/group-theory/products-of-tuples-of-elements-commutative-monoids.lagda.md index 120ca6b54c..4ad9969f5e 100644 --- a/src/group-theory/products-of-tuples-of-elements-commutative-monoids.lagda.md +++ b/src/group-theory/products-of-tuples-of-elements-commutative-monoids.lagda.md @@ -1,22 +1,57 @@ # Products of tuples of elements in commutative monoids ```agda +{-# OPTIONS --lossy-unification #-} + module group-theory.products-of-tuples-of-elements-commutative-monoids where ```
Imports ```agda +open import elementary-number-theory.addition-natural-numbers open import elementary-number-theory.natural-numbers +open import finite-group-theory.permutations-standard-finite-types +open import finite-group-theory.transpositions-standard-finite-types + +open import foundation.action-on-identifications-functions +open import foundation.cartesian-product-types open import foundation.coproduct-types +open import foundation.dependent-pair-types +open import foundation.empty-types +open import foundation.equivalences +open import foundation.function-extensionality open import foundation.function-types +open import foundation.functoriality-coproduct-types +open import foundation.functoriality-dependent-pair-types +open import foundation.homotopies +open import foundation.identity-types +open import foundation.negated-equality +open import foundation.propositional-truncations +open import foundation.sets +open import foundation.type-arithmetic-coproduct-types +open import foundation.type-arithmetic-empty-type +open import foundation.type-arithmetic-unit-type open import foundation.unit-type +open import foundation.universal-property-propositional-truncation-into-sets open import foundation.universe-levels +open import foundation.whiskering-homotopies-composition open import group-theory.commutative-monoids +open import group-theory.monoids +open import group-theory.products-of-tuples-of-elements-monoids + +open import linear-algebra.vectors-on-commutative-monoids +open import lists.lists + +open import univalent-combinatorics.coproduct-types open import univalent-combinatorics.counting +open import univalent-combinatorics.counting-dependent-pair-types +open import univalent-combinatorics.dependent-pair-types +open import univalent-combinatorics.double-counting +open import univalent-combinatorics.finite-types open import univalent-combinatorics.standard-finite-types ``` @@ -24,60 +59,856 @@ open import univalent-combinatorics.standard-finite-types ## Idea -Given an unordered `n`-tuple of elements in a commutative monoid, we can define -their product. +The product operation extends the binary multiplication operation on a +[commutative monoid](group-theory.commutative-monoids.md) `M` to any family of +elements of `M` indexed by a +[standard finite type](univalent-combinatorics.standard-finite-types.md), or to +any [finite type](univalent-combinatorics.finite-types.md). ## Definition -### Products of ordered n-tuples of elements in commutative monoids +```agda +mul-fin-Commutative-Monoid : + {l : Level} (M : Commutative-Monoid l) (n : ℕ) → + (functional-vec-Commutative-Monoid M n) → type-Commutative-Monoid M +mul-fin-Commutative-Monoid M = + mul-fin-Monoid (monoid-Commutative-Monoid M) +``` + +## Properties + +### Products of one and two elements ```agda module _ {l : Level} (M : Commutative-Monoid l) where - mul-fin-Commutative-Monoid : - (n : ℕ) → (Fin n → type-Commutative-Monoid M) → type-Commutative-Monoid M - mul-fin-Commutative-Monoid zero-ℕ x = unit-Commutative-Monoid M - mul-fin-Commutative-Monoid (succ-ℕ n) x = + mul-one-element-Commutative-Monoid : + (f : functional-vec-Commutative-Monoid M 1) → + mul-fin-Commutative-Monoid M 1 f ＝ + head-functional-vec-Commutative-Monoid M 0 f + mul-one-element-Commutative-Monoid = + mul-one-element-Monoid (monoid-Commutative-Monoid M) + + mul-two-elements-Commutative-Monoid : + (f : functional-vec-Commutative-Monoid M 2) → + mul-fin-Commutative-Monoid M 2 f ＝ + mul-Commutative-Monoid M (f (zero-Fin 1)) (f (one-Fin 1)) + mul-two-elements-Commutative-Monoid = + mul-two-elements-Monoid (monoid-Commutative-Monoid M) +``` + +### Products are homotopy invariant + +```agda +module _ + {l : Level} (M : Commutative-Monoid l) + where + + htpy-mul-fin-Commutative-Monoid : + (n : ℕ) {f g : functional-vec-Commutative-Monoid M n} → + (f ~ g) → + mul-fin-Commutative-Monoid M n f ＝ mul-fin-Commutative-Monoid M n g + htpy-mul-fin-Commutative-Monoid = + htpy-mul-fin-Monoid (monoid-Commutative-Monoid M) +``` + +### Products are equal to the zero-th term plus the rest + +```agda +module _ + {l : Level} (M : Commutative-Monoid l) + where + + cons-mul-fin-Commutative-Monoid : + (n : ℕ) (f : functional-vec-Commutative-Monoid M (succ-ℕ n)) → + {x : type-Commutative-Monoid M} → + head-functional-vec-Commutative-Monoid M n f ＝ x → + mul-fin-Commutative-Monoid M (succ-ℕ n) f ＝ + mul-Commutative-Monoid M (mul-fin-Commutative-Monoid M n (f ∘ inl-Fin n)) x + cons-mul-fin-Commutative-Monoid = + cons-mul-fin-Monoid (monoid-Commutative-Monoid M) + + snoc-mul-fin-Commutative-Monoid : + (n : ℕ) (f : functional-vec-Commutative-Monoid M (succ-ℕ n)) → + {x : type-Commutative-Monoid M} → f (zero-Fin n) ＝ x → + mul-fin-Commutative-Monoid M (succ-ℕ n) f ＝ mul-Commutative-Monoid M - ( mul-fin-Commutative-Monoid n (x ∘ inl)) - ( x (inr star)) + ( x) + ( mul-fin-Commutative-Monoid M n (f ∘ inr-Fin n)) + snoc-mul-fin-Commutative-Monoid = + snoc-mul-fin-Monoid (monoid-Commutative-Monoid M) +``` + +### Extending a product of elements in a monoid + +```agda +module _ + {l : Level} (M : Commutative-Monoid l) + where + + extend-mul-fin-Commutative-Monoid : + (n : ℕ) (f : functional-vec-Commutative-Monoid M n) → + mul-fin-Commutative-Monoid M + ( succ-ℕ n) + ( cons-functional-vec-Commutative-Monoid + ( M) + ( n) + ( unit-Commutative-Monoid M) f) ＝ + mul-fin-Commutative-Monoid M n f + extend-mul-fin-Commutative-Monoid = + extend-mul-fin-Monoid (monoid-Commutative-Monoid M) +``` + +### Shifting a product of elements in a monoid + +```agda +module _ + {l : Level} (M : Commutative-Monoid l) + where + + shift-mul-fin-Commutative-Monoid : + (n : ℕ) (f : functional-vec-Commutative-Monoid M n) → + mul-fin-Commutative-Monoid M + ( succ-ℕ n) + ( snoc-functional-vec-Commutative-Monoid M n f + ( unit-Commutative-Monoid M)) ＝ + mul-fin-Commutative-Monoid M n f + shift-mul-fin-Commutative-Monoid = + shift-mul-fin-Monoid (monoid-Commutative-Monoid M) +``` + +### A product of units is the unit - mul-count-Commutative-Monoid : - {l2 : Level} {A : UU l2} → count A → - (A → type-Commutative-Monoid M) → type-Commutative-Monoid M - mul-count-Commutative-Monoid e x = +```agda +module _ + {l : Level} (M : Commutative-Monoid l) + where + + mul-fin-unit-Commutative-Monoid : + (n : ℕ) → mul-fin-Commutative-Monoid - ( number-of-elements-count e) - ( x ∘ map-equiv-count e) + ( M) + ( n) + ( zero-functional-vec-Commutative-Monoid M n) ＝ + unit-Commutative-Monoid M + mul-fin-unit-Commutative-Monoid = + mul-fin-unit-Monoid (monoid-Commutative-Monoid M) +``` + +### Splitting products + +```agda +split-mul-fin-Commutative-Monoid : + {l : Level} (M : Commutative-Monoid l) + (n m : ℕ) (f : functional-vec-Commutative-Monoid M (n +ℕ m)) → + mul-fin-Commutative-Monoid M (n +ℕ m) f ＝ + mul-Commutative-Monoid M + ( mul-fin-Commutative-Monoid M n (f ∘ inl-coproduct-Fin n m)) + ( mul-fin-Commutative-Monoid M m (f ∘ inr-coproduct-Fin n m)) +split-mul-fin-Commutative-Monoid M = + split-mul-fin-Monoid (monoid-Commutative-Monoid M) +``` + +### Permutations preserve products + +```agda +module _ + {l : Level} (M : Commutative-Monoid l) + where + + abstract + preserves-product-adjacent-transposition-mul-fin-Commutative-Monoid : + (n : ℕ) → (k : Fin n) → + (f : functional-vec-Commutative-Monoid M (succ-ℕ n)) → + mul-fin-Commutative-Monoid M (succ-ℕ n) f ＝ + mul-fin-Commutative-Monoid + M (succ-ℕ n) (f ∘ map-adjacent-transposition-Fin n k) + preserves-product-adjacent-transposition-mul-fin-Commutative-Monoid + (succ-ℕ n) (inl x) f = + ap-mul-Commutative-Monoid + ( M) + ( preserves-product-adjacent-transposition-mul-fin-Commutative-Monoid + ( n) + ( x) + ( f ∘ inl-Fin (succ-ℕ n))) + ( refl) + preserves-product-adjacent-transposition-mul-fin-Commutative-Monoid + (succ-ℕ n) (inr star) f = right-swap-mul-Commutative-Monoid M _ _ _ + + preserves-product-permutation-list-adjacent-transpositions-Commutative-Monoid : + (n : ℕ) → (L : list (Fin n)) → + (f : functional-vec-Commutative-Monoid M (succ-ℕ n)) → + mul-fin-Commutative-Monoid M (succ-ℕ n) f ＝ + mul-fin-Commutative-Monoid + M (succ-ℕ n) (f ∘ map-permutation-list-adjacent-transpositions n L) + preserves-product-permutation-list-adjacent-transpositions-Commutative-Monoid + n nil f = refl + preserves-product-permutation-list-adjacent-transpositions-Commutative-Monoid + n (cons x L) f = + preserves-product-adjacent-transposition-mul-fin-Commutative-Monoid + ( n) + ( x) + ( f) ∙ + preserves-product-permutation-list-adjacent-transpositions-Commutative-Monoid + ( n) + ( L) + ( f ∘ map-adjacent-transposition-Fin n x) + + preserves-product-transposition-Commutative-Monoid : + (n : ℕ) (i j : Fin (succ-ℕ n)) (neq : i ≠ j) → + (f : functional-vec-Commutative-Monoid M (succ-ℕ n)) → + mul-fin-Commutative-Monoid M (succ-ℕ n) f ＝ + mul-fin-Commutative-Monoid + M (succ-ℕ n) (f ∘ map-transposition-Fin (succ-ℕ n) i j neq) + preserves-product-transposition-Commutative-Monoid n i j i≠j f = + preserves-product-permutation-list-adjacent-transpositions-Commutative-Monoid + ( n) + ( list-adjacent-transpositions-transposition-Fin n i j) + ( f) ∙ + ap + ( λ g → mul-fin-Commutative-Monoid M (succ-ℕ n) (f ∘ map-equiv g)) + ( eq-permutation-list-adjacent-transpositions-transposition-Fin + ( n) + ( i) + ( j) + ( i≠j)) + + preserves-product-permutation-list-standard-transpositions-Commutative-Monoid : + (n : ℕ) → (L : list (Σ (Fin n × Fin n) ( λ (i , j) → i ≠ j))) → + (f : functional-vec-Commutative-Monoid M n) → + mul-fin-Commutative-Monoid M n f ＝ + mul-fin-Commutative-Monoid + M n (f ∘ map-equiv (permutation-list-standard-transpositions-Fin n L)) + preserves-product-permutation-list-standard-transpositions-Commutative-Monoid + zero-ℕ _ _ = refl + preserves-product-permutation-list-standard-transpositions-Commutative-Monoid + (succ-ℕ n) nil f = refl + preserves-product-permutation-list-standard-transpositions-Commutative-Monoid + (succ-ℕ n) (cons ((i , j) , i≠j) L) f = + preserves-product-transposition-Commutative-Monoid n i j i≠j f ∙ + preserves-product-permutation-list-standard-transpositions-Commutative-Monoid + ( succ-ℕ n) + ( L) + ( f ∘ map-transposition-Fin (succ-ℕ n) i j i≠j) + + preserves-product-permutation-Commutative-Monoid : + (n : ℕ) → (σ : Permutation n) → + (f : functional-vec-Commutative-Monoid M n) → + mul-fin-Commutative-Monoid M n f ＝ + mul-fin-Commutative-Monoid M n (f ∘ map-equiv σ) + preserves-product-permutation-Commutative-Monoid n σ f = + preserves-product-permutation-list-standard-transpositions-Commutative-Monoid + ( n) + ( list-standard-transpositions-permutation-Fin n σ) + ( f) ∙ + ap + ( λ τ → mul-fin-Commutative-Monoid M n (f ∘ map-equiv τ)) + ( eq-permutation-list-standard-transpositions-Fin n σ) +``` + +### Products for a count for a type + +```agda +mul-count-Commutative-Monoid : + {l1 l2 : Level} (M : Commutative-Monoid l1) (A : UU l2) → + count A → (A → type-Commutative-Monoid M) → type-Commutative-Monoid M +mul-count-Commutative-Monoid M A (n , Fin-n≃A) f = + mul-fin-Commutative-Monoid M n (f ∘ map-equiv Fin-n≃A) +``` + +### Products for a count for a type are homotopy invariant + +```agda +module _ + {l1 l2 : Level} (M : Commutative-Monoid l1) (A : UU l2) + where + + htpy-mul-count-Commutative-Monoid : + (c : count A) → + {f g : A → type-Commutative-Monoid M} → (f ~ g) → + mul-count-Commutative-Monoid M A c f ＝ + mul-count-Commutative-Monoid M A c g + htpy-mul-count-Commutative-Monoid (nA , _) H = + htpy-mul-fin-Commutative-Monoid M nA (λ i → H _) +``` + +### Two counts for the same set produce equal products + +```agda +module _ + {l1 l2 : Level} (M : Commutative-Monoid l1) (A : UU l2) + where + + abstract + eq-mul-count-equiv-Commutative-Monoid : + (n : ℕ) → (equiv1 equiv2 : Fin n ≃ A) → + (f : A → type-Commutative-Monoid M) → + mul-count-Commutative-Monoid M A (n , equiv1) f ＝ + mul-count-Commutative-Monoid M A (n , equiv2) f + eq-mul-count-equiv-Commutative-Monoid n equiv1 equiv2 f = + equational-reasoning + mul-fin-Commutative-Monoid M n (f ∘ map-equiv equiv1) + ＝ + mul-fin-Commutative-Monoid + ( M) + ( n) + ( (f ∘ map-equiv equiv1) ∘ (map-inv-equiv equiv1 ∘ map-equiv equiv2)) + by + preserves-product-permutation-Commutative-Monoid + ( M) + ( n) + ( inv-equiv equiv1 ∘e equiv2) + ( f ∘ map-equiv equiv1) + ＝ mul-fin-Commutative-Monoid M n (f ∘ map-equiv equiv2) + by + ap + ( λ g → mul-fin-Commutative-Monoid M n (f ∘ (g ∘ map-equiv equiv2))) + ( eq-htpy (is-section-map-inv-equiv equiv1)) + + eq-mul-count-Commutative-Monoid : + (f : A → type-Commutative-Monoid M) (c1 c2 : count A) → + mul-count-Commutative-Monoid M A c1 f ＝ + mul-count-Commutative-Monoid M A c2 f + eq-mul-count-Commutative-Monoid f c1@(n , e1) c2@(_ , e2) + with double-counting c1 c2 + ... | refl = eq-mul-count-equiv-Commutative-Monoid n e1 e2 f +``` + +### Products over finite types + +```agda +module _ + {l1 l2 : Level} (M : Commutative-Monoid l1) (A : Finite-Type l2) + where + + mul-finite-Commutative-Monoid : + (f : type-Finite-Type A → type-Commutative-Monoid M) → + type-Commutative-Monoid M + mul-finite-Commutative-Monoid f = + map-universal-property-set-quotient-trunc-Prop + ( set-Commutative-Monoid M) + ( λ c → mul-count-Commutative-Monoid M (type-Finite-Type A) c f) + ( eq-mul-count-Commutative-Monoid M (type-Finite-Type A) f) + ( is-finite-type-Finite-Type A) +``` + +### The product over a finite type is its product over any count for the type + +```agda +module _ + {l1 l2 l3 : Level} (M : Commutative-Monoid l1) + (A : UU l2) (B : UU l3) (H : A ≃ B) + where + + abstract + mul-equiv-count-Commutative-Monoid : + (cA : count A) (cB : count B) (f : A → type-Commutative-Monoid M) → + mul-count-Commutative-Monoid M A cA f ＝ + mul-count-Commutative-Monoid M B cB (f ∘ map-inv-equiv H) + mul-equiv-count-Commutative-Monoid + cA@(nA , Fin-nA≃A) cB@(_ , Fin-nB≃B) f + with double-counting-equiv cA cB H + ... | refl = + preserves-product-permutation-Commutative-Monoid + ( M) + ( nA) + ( inv-equiv Fin-nA≃A ∘e inv-equiv H ∘e Fin-nB≃B) + ( _) ∙ + htpy-mul-fin-Commutative-Monoid + ( M) + ( nA) + ( λ i → ap f (is-section-map-inv-equiv Fin-nA≃A _)) + +module _ + {l1 l2 : Level} (M : Commutative-Monoid l1) + (A : Finite-Type l2) (cA : count (type-Finite-Type A)) + where + + abstract + mul-finite-count-Commutative-Monoid : + (f : type-Finite-Type A → type-Commutative-Monoid M) → + mul-finite-Commutative-Monoid M A f ＝ + mul-count-Commutative-Monoid M (type-Finite-Type A) cA f + mul-finite-count-Commutative-Monoid f = + equational-reasoning + mul-finite-Commutative-Monoid M A f + ＝ + mul-finite-Commutative-Monoid + ( M) + ( type-Finite-Type A , unit-trunc-Prop cA) + ( f) + by + ap + ( λ c → + mul-finite-Commutative-Monoid + ( M) + ( type-Finite-Type A , c) + ( f)) + ( all-elements-equal-type-trunc-Prop + ( is-finite-type-Finite-Type A) + ( unit-trunc-Prop cA)) + ＝ mul-count-Commutative-Monoid M (type-Finite-Type A) cA f + by + htpy-universal-property-set-quotient-trunc-Prop + ( set-Commutative-Monoid M) + ( λ c → + mul-count-Commutative-Monoid M (type-Finite-Type A) c f) + ( eq-mul-count-Commutative-Monoid M (type-Finite-Type A) f) + ( cA) +``` + +### The product over an empty type is the unit + +```agda +module _ + {l1 l2 : Level} (M : Commutative-Monoid l1) (A : Finite-Type l2) + (H : is-empty (type-Finite-Type A)) + where + + abstract + mul-is-empty-finite-Commutative-Monoid : + (f : type-Finite-Type A → type-Commutative-Monoid M) → + is-unit-Commutative-Monoid M (mul-finite-Commutative-Monoid M A f) + mul-is-empty-finite-Commutative-Monoid = + mul-finite-count-Commutative-Monoid M A (count-is-empty H) +``` -{- - compute-permutation-mul-fin-Commutative-Monoid : - (n : ℕ) (e : Fin n ≃ Fin n) (x : Fin n → type-Commutative-Monoid M) → - Id ( mul-fin-Commutative-Monoid n (x ∘ map-equiv e)) - ( mul-fin-Commutative-Monoid n x) - compute-permutation-mul-fin-Commutative-Monoid zero-ℕ e x = refl - compute-permutation-mul-fin-Commutative-Monoid (succ-ℕ n) e x = {!!} +### The product of units is the unit + +```agda +module _ + {l1 l2 : Level} (M : Commutative-Monoid l1) (A : Finite-Type l2) + where + + mul-finite-unit-Commutative-Monoid : + is-unit-Commutative-Monoid + ( M) + ( mul-finite-Commutative-Monoid + ( M) + ( A) + ( λ _ → unit-Commutative-Monoid M)) + mul-finite-unit-Commutative-Monoid = + let + open + do-syntax-trunc-Prop + (is-unit-prop-Commutative-Monoid + ( M) + ( mul-finite-Commutative-Monoid + ( M) + ( A) + ( λ _ → unit-Commutative-Monoid M))) + in do + cA ← is-finite-type-Finite-Type A + mul-finite-count-Commutative-Monoid M A cA _ ∙ + mul-fin-unit-Commutative-Monoid M _ +``` + +### Products over a finite type are homotopy invariant + +```agda +module _ + {l1 l2 : Level} (M : Commutative-Monoid l1) (A : Finite-Type l2) + where + + abstract + htpy-mul-finite-Commutative-Monoid : + {f g : type-Finite-Type A → type-Commutative-Monoid M} → + f ~ g → + mul-finite-Commutative-Monoid M A f ＝ mul-finite-Commutative-Monoid M A g + htpy-mul-finite-Commutative-Monoid {f} {g} H = + let + open + do-syntax-trunc-Prop + ( Id-Prop + ( set-Commutative-Monoid M) + ( mul-finite-Commutative-Monoid M A f) + ( mul-finite-Commutative-Monoid M A g)) + in do + cA ← is-finite-type-Finite-Type A + equational-reasoning + mul-finite-Commutative-Monoid M A f + ＝ mul-count-Commutative-Monoid M (type-Finite-Type A) cA f + by mul-finite-count-Commutative-Monoid M A cA f + ＝ mul-count-Commutative-Monoid M (type-Finite-Type A) cA g + by htpy-mul-count-Commutative-Monoid M (type-Finite-Type A) cA H + ＝ mul-finite-Commutative-Monoid M A g + by inv (mul-finite-count-Commutative-Monoid M A cA g) +``` + +### Products over finite types are preserved by equivalences + +```agda +module _ + {l1 l2 l3 : Level} (M : Commutative-Monoid l1) + (A : Finite-Type l2) (B : Finite-Type l3) + (H : equiv-Finite-Type A B) + where + + abstract + mul-equiv-finite-Commutative-Monoid : + (f : type-Finite-Type A → type-Commutative-Monoid M) → + mul-finite-Commutative-Monoid M A f ＝ + mul-finite-Commutative-Monoid M B (f ∘ map-inv-equiv H) + mul-equiv-finite-Commutative-Monoid f = + let + open + do-syntax-trunc-Prop + ( Id-Prop + ( set-Commutative-Monoid M) + ( mul-finite-Commutative-Monoid M A f) + ( mul-finite-Commutative-Monoid M B (f ∘ map-inv-equiv H))) + in do + cA ← is-finite-type-Finite-Type A + cB ← is-finite-type-Finite-Type B + equational-reasoning + mul-finite-Commutative-Monoid M A f + ＝ + mul-count-Commutative-Monoid M (type-Finite-Type A) cA f + by mul-finite-count-Commutative-Monoid M A cA f + ＝ + mul-count-Commutative-Monoid + ( M) + ( type-Finite-Type B) + ( cB) + ( f ∘ map-inv-equiv H) + by + mul-equiv-count-Commutative-Monoid + ( M) + ( type-Finite-Type A) + ( type-Finite-Type B) + ( H) + ( cA) + ( cB) + ( f) + ＝ mul-finite-Commutative-Monoid M B (f ∘ map-inv-equiv H) + by inv (mul-finite-count-Commutative-Monoid M B cB _) +``` + +### Products over finite types distribute over coproducts + +```agda +module _ + {l1 l2 l3 : Level} (M : Commutative-Monoid l1) + (A : Finite-Type l2) (B : Finite-Type l3) + where + + abstract + mul-coproduct-finite-Commutative-Monoid : + (f : + type-Finite-Type A + type-Finite-Type B → type-Commutative-Monoid M) → + mul-finite-Commutative-Monoid M (coproduct-Finite-Type A B) f ＝ + mul-Commutative-Monoid + ( M) + ( mul-finite-Commutative-Monoid M A (f ∘ inl)) + ( mul-finite-Commutative-Monoid M B (f ∘ inr)) + mul-coproduct-finite-Commutative-Monoid f = + let + open + do-syntax-trunc-Prop + ( Id-Prop + ( set-Commutative-Monoid M) + ( mul-finite-Commutative-Monoid + ( M) + ( coproduct-Finite-Type A B) + ( f)) + ( mul-Commutative-Monoid + ( M) + ( mul-finite-Commutative-Monoid M A (f ∘ inl)) + ( mul-finite-Commutative-Monoid M B (f ∘ inr)))) + in do + cA@(nA , Fin-nA≃A) ← is-finite-type-Finite-Type A + cB@(nB , Fin-nB≃B) ← is-finite-type-Finite-Type B + equational-reasoning + mul-finite-Commutative-Monoid M (coproduct-Finite-Type A B) f + ＝ + mul-fin-Commutative-Monoid + ( M) + ( nA +ℕ nB) + ( f ∘ map-equiv-count (count-coproduct cA cB)) + by + mul-finite-count-Commutative-Monoid + ( M) + ( coproduct-Finite-Type A B) + ( count-coproduct cA cB) + ( f) + ＝ + mul-Commutative-Monoid M + ( mul-fin-Commutative-Monoid + ( M) + ( nA) + ( f ∘ + map-equiv-count (count-coproduct cA cB) ∘ + inl-coproduct-Fin nA nB)) + ( mul-fin-Commutative-Monoid + ( M) + ( nB) + ( f ∘ + map-equiv-count (count-coproduct cA cB) ∘ + inr-coproduct-Fin nA nB)) + by + split-mul-fin-Commutative-Monoid + ( M) + ( nA) + ( nB) + ( f ∘ map-equiv-count (count-coproduct cA cB)) + ＝ + mul-Commutative-Monoid + ( M) + ( mul-fin-Commutative-Monoid + ( M) + ( nA) + ( f ∘ inl ∘ map-equiv-count cA)) + ( mul-fin-Commutative-Monoid + ( M) + ( nB) + ( f ∘ inr ∘ map-equiv-count cB)) + by + ap-mul-Commutative-Monoid + ( M) + ( ap + ( λ g → mul-fin-Commutative-Monoid M nA (f ∘ g)) + ( eq-htpy + ( map-equiv-count-coproduct-inl-coproduct-Fin cA cB))) + ( ap + ( λ g → mul-fin-Commutative-Monoid M nB (f ∘ g)) + ( eq-htpy + ( map-equiv-count-coproduct-inr-coproduct-Fin cA cB))) + ＝ + mul-Commutative-Monoid + ( M) + ( mul-finite-Commutative-Monoid M A (f ∘ inl)) + ( mul-finite-Commutative-Monoid M B (f ∘ inr)) + by + inv + ( ap-mul-Commutative-Monoid + ( M) + ( mul-finite-count-Commutative-Monoid + ( M) + ( A) + ( cA) + ( f ∘ inl)) + ( mul-finite-count-Commutative-Monoid + ( M) + ( B) + ( cB) + ( f ∘ inr))) +``` + +### Products distribute over dependent pair types + +```agda +module _ + {l : Level} (M : Commutative-Monoid l) + where + + abstract + mul-fin-finite-Σ-Commutative-Monoid : + (n : ℕ) → + {l2 : Level} → + (B : Fin n → Finite-Type l2) → + (f : (k : Fin n) → type-Finite-Type (B k) → type-Commutative-Monoid M) → + mul-fin-Commutative-Monoid M n + (λ k → mul-finite-Commutative-Monoid M (B k) (f k)) ＝ + mul-finite-Commutative-Monoid + M (Σ-Finite-Type (Fin-Finite-Type n) B) (ind-Σ f) + mul-fin-finite-Σ-Commutative-Monoid zero-ℕ B f = + inv + ( mul-is-empty-finite-Commutative-Monoid + ( M) + ( Σ-Finite-Type (Fin-Finite-Type zero-ℕ) B) + ( λ ()) + ( ind-Σ f)) + mul-fin-finite-Σ-Commutative-Monoid (succ-ℕ n) B f = + equational-reasoning + mul-fin-Commutative-Monoid + ( M) + ( succ-ℕ n) + ( λ k → mul-finite-Commutative-Monoid M (B k) (f k)) + ＝ + mul-Commutative-Monoid + ( M) + ( mul-fin-Commutative-Monoid + ( M) + ( n) + ( λ k → + mul-finite-Commutative-Monoid + ( M) + ( B (inl k)) + ( f (inl k)))) + ( mul-finite-Commutative-Monoid + ( M) + ( B (inr star)) + ( f (inr star))) + by + cons-mul-fin-Commutative-Monoid + ( M) + ( n) + ( λ k → mul-finite-Commutative-Monoid M (B k) (f k)) + ( refl) + ＝ + mul-Commutative-Monoid + ( M) + ( mul-finite-Commutative-Monoid + ( M) + ( Σ-Finite-Type (Fin-Finite-Type n) (B ∘ inl)) + ( ind-Σ (f ∘ inl))) + ( mul-finite-Commutative-Monoid + ( M) + ( B (inr star)) + ( f (inr star))) + by + ap-mul-Commutative-Monoid + ( M) + ( mul-fin-finite-Σ-Commutative-Monoid + ( n) + ( B ∘ inl) + ( f ∘ inl)) + ( refl) + ＝ + mul-finite-Commutative-Monoid + ( M) + ( coproduct-Finite-Type + ( Σ-Finite-Type (Fin-Finite-Type n) (B ∘ inl)) + ( B (inr star))) + ( rec-coproduct (ind-Σ (f ∘ inl)) (f (inr star))) + by + inv + ( mul-coproduct-finite-Commutative-Monoid + ( M) + ( Σ-Finite-Type (Fin-Finite-Type n) (B ∘ inl)) + ( B (inr star)) + ( rec-coproduct (ind-Σ (f ∘ inl)) (f (inr star)))) + ＝ + mul-finite-Commutative-Monoid + ( M) + ( Σ-Finite-Type (Fin-Finite-Type (succ-ℕ n)) B) + ( rec-coproduct (ind-Σ (f ∘ inl)) (f (inr star)) ∘ + map-coproduct + ( id) + ( map-left-unit-law-Σ (type-Finite-Type ∘ B ∘ inr)) ∘ + map-right-distributive-Σ-coproduct + ( Fin n) + ( unit) + ( type-Finite-Type ∘ B)) + by + mul-equiv-finite-Commutative-Monoid + ( M) + ( coproduct-Finite-Type + ( Σ-Finite-Type (Fin-Finite-Type n) (B ∘ inl)) + ( B (inr star))) + (Σ-Finite-Type (Fin-Finite-Type (succ-ℕ n)) B) + ( inv-equiv + ( equiv-coproduct + ( id-equiv) + ( left-unit-law-Σ (type-Finite-Type ∘ B ∘ inr)) ∘e + right-distributive-Σ-coproduct + ( Fin n) + ( unit) + ( type-Finite-Type ∘ B))) + _ + ＝ + mul-finite-Commutative-Monoid + ( M) + ( Σ-Finite-Type (Fin-Finite-Type (succ-ℕ n)) B) + ( ind-Σ f) + by + htpy-mul-finite-Commutative-Monoid + ( M) + ( Σ-Finite-Type (Fin-Finite-Type (succ-ℕ n)) B) + ( λ { (inl k , b) → refl ; (inr k , b) → refl}) + +module _ + {l1 l2 l3 : Level} (M : Commutative-Monoid l1) + (A : Finite-Type l2) (B : type-Finite-Type A → Finite-Type l3) + where - compute-mul-double-counting-Commutative-Monoid : - {l2 : Level} {A : UU l2} (e1 : count A) (e2 : count A) → - (x : A → type-Commutative-Monoid M) → - Id (mul-count-Commutative-Monoid e1 x) (mul-count-Commutative-Monoid e2 x) - compute-mul-double-counting-Commutative-Monoid e1 e2 x = {!!} --} + abstract + mul-Σ-finite-Commutative-Monoid : + (f : + (a : type-Finite-Type A) → + type-Finite-Type (B a) → + type-Commutative-Monoid M) → + mul-finite-Commutative-Monoid M (Σ-Finite-Type A B) (ind-Σ f) ＝ + mul-finite-Commutative-Monoid + ( M) + ( A) + ( λ a → mul-finite-Commutative-Monoid M (B a) (f a)) + mul-Σ-finite-Commutative-Monoid f = + let + open + do-syntax-trunc-Prop + ( Id-Prop + ( set-Commutative-Monoid M) + ( mul-finite-Commutative-Monoid M (Σ-Finite-Type A B) (ind-Σ f)) + ( mul-finite-Commutative-Monoid + ( M) + ( A) + ( λ a → mul-finite-Commutative-Monoid M (B a) (f a)))) + in do + cA@(nA , Fin-nA≃A) ← is-finite-type-Finite-Type A + equational-reasoning + mul-finite-Commutative-Monoid M (Σ-Finite-Type A B) (ind-Σ f) + ＝ + mul-finite-Commutative-Monoid + ( M) + ( Σ-Finite-Type (Fin-Finite-Type nA) (B ∘ map-equiv Fin-nA≃A)) + ( ind-Σ (f ∘ map-equiv Fin-nA≃A)) + by + mul-equiv-finite-Commutative-Monoid + ( M) + ( Σ-Finite-Type A B) + ( Σ-Finite-Type (Fin-Finite-Type nA) (B ∘ map-equiv Fin-nA≃A)) + ( inv-equiv + ( equiv-Σ-equiv-base (type-Finite-Type ∘ B) Fin-nA≃A)) + ( _) + ＝ + mul-count-Commutative-Monoid + ( M) + ( type-Finite-Type A) + ( cA) + ( λ a → mul-finite-Commutative-Monoid M (B a) (f a)) + by + inv + ( mul-fin-finite-Σ-Commutative-Monoid + ( M) + ( nA) + ( B ∘ map-equiv Fin-nA≃A) + ( f ∘ map-equiv Fin-nA≃A)) + ＝ + mul-finite-Commutative-Monoid + ( M) + ( A) + ( λ a → mul-finite-Commutative-Monoid M (B a) (f a)) + by inv (mul-finite-count-Commutative-Monoid M A cA _) ``` -### Products of unordered n-tuples of elements in commutative monoids +### Products over the unit type ```agda module _ {l : Level} (M : Commutative-Monoid l) where -{- - mul-tuple-Commutative-Monoid : - {n : ℕ} → unordered-tuple-Commutative-Monoid n M → type-Commutative-Monoid M - mul-tuple-Commutative-Monoid {n} (pair I x) = {!!} --} + abstract + mul-unit-finite-Commutative-Monoid : + (f : unit → type-Commutative-Monoid M) → + mul-finite-Commutative-Monoid M unit-Finite-Type f ＝ f star + mul-unit-finite-Commutative-Monoid f = + equational-reasoning + mul-finite-Commutative-Monoid M unit-Finite-Type f + ＝ + mul-count-Commutative-Monoid + ( M) + ( unit) + ( count-unit) + ( f) + by + mul-finite-count-Commutative-Monoid + ( M) + ( unit-Finite-Type) + ( count-unit) + ( f) + ＝ f star by mul-one-element-Commutative-Monoid M _ ``` diff --git a/src/group-theory/products-of-tuples-of-elements-monoids.lagda.md b/src/group-theory/products-of-tuples-of-elements-monoids.lagda.md new file mode 100644 index 0000000000..68964b6a1f --- /dev/null +++ b/src/group-theory/products-of-tuples-of-elements-monoids.lagda.md @@ -0,0 +1,201 @@ +# Products of tuples of elements in monoids + +```agda +module group-theory.products-of-tuples-of-elements-monoids where +``` + +
Imports + +```agda +open import elementary-number-theory.addition-natural-numbers +open import elementary-number-theory.natural-numbers + +open import foundation.action-on-identifications-functions +open import foundation.coproduct-types +open import foundation.function-types +open import foundation.homotopies +open import foundation.identity-types +open import foundation.unit-type +open import foundation.universe-levels +open import foundation.whiskering-homotopies-composition + +open import group-theory.monoids + +open import linear-algebra.vectors-on-monoids + +open import univalent-combinatorics.coproduct-types +open import univalent-combinatorics.standard-finite-types +``` + +
+ +## Idea + +The product operation extends the binary multiplication operation on a +[monoid](group-theory.monoids.md) `M` to any family of elements of `M` indexed +by a [standard finite type](univalent-combinatorics.standard-finite-types.md). + +## Definition + +```agda +mul-fin-Monoid : + {l : Level} (M : Monoid l) (n : ℕ) → + (functional-vec-Monoid M n) → type-Monoid M +mul-fin-Monoid M zero-ℕ f = unit-Monoid M +mul-fin-Monoid M (succ-ℕ n) f = + mul-Monoid M + ( mul-fin-Monoid M n (f ∘ inl-Fin n)) + ( f (inr star)) +``` + +## Properties + +### Products of one and two elements + +```agda +module _ + {l : Level} (M : Monoid l) + where + + mul-one-element-Monoid : + (f : functional-vec-Monoid M 1) → + mul-fin-Monoid M 1 f ＝ head-functional-vec-Monoid M 0 f + mul-one-element-Monoid f = + left-unit-law-mul-Monoid M (f (inr star)) + + mul-two-elements-Monoid : + (f : functional-vec-Monoid M 2) → + mul-fin-Monoid M 2 f ＝ mul-Monoid M (f (zero-Fin 1)) (f (one-Fin 1)) + mul-two-elements-Monoid f = + ( associative-mul-Monoid M + (unit-Monoid M) (f (zero-Fin 1)) (f (one-Fin 1))) ∙ + ( left-unit-law-mul-Monoid M + ( mul-Monoid M (f (zero-Fin 1)) (f (one-Fin 1)))) +``` + +### Products are homotopy invariant + +```agda +module _ + {l : Level} (M : Monoid l) + where + + htpy-mul-fin-Monoid : + (n : ℕ) {f g : functional-vec-Monoid M n} → + (f ~ g) → mul-fin-Monoid M n f ＝ mul-fin-Monoid M n g + htpy-mul-fin-Monoid zero-ℕ H = refl + htpy-mul-fin-Monoid (succ-ℕ n) H = + ap-mul-Monoid M + ( htpy-mul-fin-Monoid n (H ·r inl-Fin n)) + ( H (inr star)) +``` + +### Products are equal to the zero-th term times the rest + +```agda +module _ + {l : Level} (M : Monoid l) + where + + cons-mul-fin-Monoid : + (n : ℕ) (f : functional-vec-Monoid M (succ-ℕ n)) → + {x : type-Monoid M} → head-functional-vec-Monoid M n f ＝ x → + mul-fin-Monoid M (succ-ℕ n) f ＝ + mul-Monoid M (mul-fin-Monoid M n (f ∘ inl-Fin n)) x + cons-mul-fin-Monoid n f refl = refl + + snoc-mul-fin-Monoid : + (n : ℕ) (f : functional-vec-Monoid M (succ-ℕ n)) → + {x : type-Monoid M} → f (zero-Fin n) ＝ x → + mul-fin-Monoid M (succ-ℕ n) f ＝ + mul-Monoid M + ( x) + ( mul-fin-Monoid M n (f ∘ inr-Fin n)) + snoc-mul-fin-Monoid zero-ℕ f refl = + ( mul-one-element-Monoid M f) ∙ + ( inv (right-unit-law-mul-Monoid M (f (zero-Fin 0)))) + snoc-mul-fin-Monoid (succ-ℕ n) f refl = + ( ap + ( mul-Monoid' M (head-functional-vec-Monoid M (succ-ℕ n) f)) + ( snoc-mul-fin-Monoid n (f ∘ inl-Fin (succ-ℕ n)) refl)) ∙ + ( associative-mul-Monoid M + ( f (zero-Fin (succ-ℕ n))) + ( mul-fin-Monoid M n (f ∘ (inr-Fin (succ-ℕ n) ∘ inl-Fin n))) + ( head-functional-vec-Monoid M (succ-ℕ n) f)) +``` + +### Extending a product of elements in a monoid + +```agda +module _ + {l : Level} (M : Monoid l) + where + + extend-mul-fin-Monoid : + (n : ℕ) (f : functional-vec-Monoid M n) → + mul-fin-Monoid M + ( succ-ℕ n) + ( cons-functional-vec-Monoid M n (unit-Monoid M) f) ＝ + mul-fin-Monoid M n f + extend-mul-fin-Monoid n f = + right-unit-law-mul-Monoid M (mul-fin-Monoid M n f) +``` + +### Shifting a product of elements in a monoid + +```agda +module _ + {l : Level} (M : Monoid l) + where + + shift-mul-fin-Monoid : + (n : ℕ) (f : functional-vec-Monoid M n) → + mul-fin-Monoid M + ( succ-ℕ n) + ( snoc-functional-vec-Monoid M n f + ( unit-Monoid M)) ＝ + mul-fin-Monoid M n f + shift-mul-fin-Monoid zero-ℕ f = + left-unit-law-mul-Monoid M (unit-Monoid M) + shift-mul-fin-Monoid (succ-ℕ n) f = + ap + ( mul-Monoid' M + ( head-functional-vec-Monoid M n f)) + ( shift-mul-fin-Monoid n + ( tail-functional-vec-Monoid M n f)) +``` + +### A product of units is the unit + +```agda +module _ + {l : Level} (M : Monoid l) + where + + abstract + mul-fin-unit-Monoid : + (n : ℕ) → + mul-fin-Monoid M n (zero-functional-vec-Monoid M n) ＝ unit-Monoid M + mul-fin-unit-Monoid zero-ℕ = refl + mul-fin-unit-Monoid (succ-ℕ n) = + right-unit-law-mul-Monoid M _ ∙ mul-fin-unit-Monoid n +``` + +### Splitting products + +```agda +split-mul-fin-Monoid : + {l : Level} (M : Monoid l) + (n m : ℕ) (f : functional-vec-Monoid M (n +ℕ m)) → + mul-fin-Monoid M (n +ℕ m) f ＝ + mul-Monoid M + ( mul-fin-Monoid M n (f ∘ inl-coproduct-Fin n m)) + ( mul-fin-Monoid M m (f ∘ inr-coproduct-Fin n m)) +split-mul-fin-Monoid M n zero-ℕ f = + inv (right-unit-law-mul-Monoid M (mul-fin-Monoid M n f)) +split-mul-fin-Monoid M n (succ-ℕ m) f = + ( ap + ( mul-Monoid' M (f (inr star))) + ( split-mul-fin-Monoid M n m (f ∘ inl))) ∙ + ( associative-mul-Monoid M _ _ _) +``` diff --git a/src/linear-algebra.lagda.md b/src/linear-algebra.lagda.md index 883be1c3fa..f3c4499d73 100644 --- a/src/linear-algebra.lagda.md +++ b/src/linear-algebra.lagda.md @@ -18,9 +18,11 @@ open import linear-algebra.scalar-multiplication-vectors public open import linear-algebra.scalar-multiplication-vectors-on-rings public open import linear-algebra.transposition-matrices public open import linear-algebra.vectors public +open import linear-algebra.vectors-on-commutative-monoids public open import linear-algebra.vectors-on-commutative-rings public open import linear-algebra.vectors-on-commutative-semirings public open import linear-algebra.vectors-on-euclidean-domains public +open import linear-algebra.vectors-on-monoids public open import linear-algebra.vectors-on-rings public open import linear-algebra.vectors-on-semirings public ``` diff --git a/src/linear-algebra/vectors-on-commutative-monoids.lagda.md b/src/linear-algebra/vectors-on-commutative-monoids.lagda.md new file mode 100644 index 0000000000..04439a10a3 --- /dev/null +++ b/src/linear-algebra/vectors-on-commutative-monoids.lagda.md @@ -0,0 +1,240 @@ +# Vectors on commutative monoids + +```agda +module linear-algebra.vectors-on-commutative-monoids where +``` + +
Imports + +```agda +open import elementary-number-theory.natural-numbers + +open import foundation.action-on-identifications-binary-functions +open import foundation.dependent-pair-types +open import foundation.function-extensionality +open import foundation.identity-types +open import foundation.universe-levels + +open import group-theory.commutative-monoids +open import group-theory.monoids +open import group-theory.semigroups + +open import linear-algebra.constant-vectors +open import linear-algebra.functoriality-vectors +open import linear-algebra.vectors +open import linear-algebra.vectors-on-monoids +``` + +
+ +## Idea + +Given a [commutative monoid](group-theory.commutative-monoids.md) `M`, the type +`vec n M` of `n`-dimensional `M`-[vectors](linear-algebra.vectors.md) is a +commutative monoid given by componentwise addition. + +We use additive terminology for vectors, as is standard in linear algebra +contexts, despite using multiplicative terminology for monoids. + +## Definitions + +### Listed vectors on commutative monoids + +```agda +module _ + {l : Level} (M : Commutative-Monoid l) + where + + vec-Commutative-Monoid : ℕ → UU l + vec-Commutative-Monoid = vec-Monoid (monoid-Commutative-Monoid M) + + head-vec-Commutative-Monoid : + {n : ℕ} → vec-Commutative-Monoid (succ-ℕ n) → type-Commutative-Monoid M + head-vec-Commutative-Monoid = head-vec-Monoid (monoid-Commutative-Monoid M) + + tail-vec-Commutative-Monoid : + {n : ℕ} → vec-Commutative-Monoid (succ-ℕ n) → vec-Commutative-Monoid n + tail-vec-Commutative-Monoid = tail-vec-Monoid (monoid-Commutative-Monoid M) + + snoc-vec-Commutative-Monoid : + {n : ℕ} → vec-Commutative-Monoid n → type-Commutative-Monoid M → + vec-Commutative-Monoid (succ-ℕ n) + snoc-vec-Commutative-Monoid = snoc-vec-Monoid (monoid-Commutative-Monoid M) +``` + +### Functional vectors on commutative monoids + +```agda +module _ + {l : Level} (M : Commutative-Monoid l) + where + + functional-vec-Commutative-Monoid : ℕ → UU l + functional-vec-Commutative-Monoid = + functional-vec-Monoid (monoid-Commutative-Monoid M) + + head-functional-vec-Commutative-Monoid : + (n : ℕ) → functional-vec-Commutative-Monoid (succ-ℕ n) → + type-Commutative-Monoid M + head-functional-vec-Commutative-Monoid = + head-functional-vec-Monoid (monoid-Commutative-Monoid M) + + tail-functional-vec-Commutative-Monoid : + (n : ℕ) → functional-vec-Commutative-Monoid (succ-ℕ n) → + functional-vec-Commutative-Monoid n + tail-functional-vec-Commutative-Monoid = + tail-functional-vec-Monoid (monoid-Commutative-Monoid M) + + cons-functional-vec-Commutative-Monoid : + (n : ℕ) → type-Commutative-Monoid M → + functional-vec-Commutative-Monoid n → + functional-vec-Commutative-Monoid (succ-ℕ n) + cons-functional-vec-Commutative-Monoid = + cons-functional-vec-Monoid (monoid-Commutative-Monoid M) + + snoc-functional-vec-Commutative-Monoid : + (n : ℕ) → functional-vec-Commutative-Monoid n → + type-Commutative-Monoid M → functional-vec-Commutative-Monoid (succ-ℕ n) + snoc-functional-vec-Commutative-Monoid = + snoc-functional-vec-Monoid (monoid-Commutative-Monoid M) +``` + +### Zero vectors of a commutative monoid + +#### The zero listed vector + +```agda +module _ + {l : Level} (M : Commutative-Monoid l) + where + + zero-vec-Commutative-Monoid : {n : ℕ} → vec-Commutative-Monoid M n + zero-vec-Commutative-Monoid = constant-vec (unit-Commutative-Monoid M) +``` + +#### The zero functional vector + +```agda +module _ + {l : Level} (M : Commutative-Monoid l) + where + + zero-functional-vec-Commutative-Monoid : + (n : ℕ) → functional-vec-Commutative-Monoid M n + zero-functional-vec-Commutative-Monoid n i = unit-Commutative-Monoid M +``` + +### Pointwise addition of vectors on a commutative monoid + +#### Pointwise addition of listed vectors on a commutative monoid + +```agda +module _ + {l : Level} (M : Commutative-Monoid l) + where + + add-vec-Commutative-Monoid : + {n : ℕ} → vec-Commutative-Monoid M n → vec-Commutative-Monoid M n → + vec-Commutative-Monoid M n + add-vec-Commutative-Monoid = + add-vec-Monoid (monoid-Commutative-Monoid M) + + associative-add-vec-Commutative-Monoid : + {n : ℕ} (v1 v2 v3 : vec-Commutative-Monoid M n) → + add-vec-Commutative-Monoid (add-vec-Commutative-Monoid v1 v2) v3 ＝ + add-vec-Commutative-Monoid v1 (add-vec-Commutative-Monoid v2 v3) + associative-add-vec-Commutative-Monoid = + associative-add-vec-Monoid (monoid-Commutative-Monoid M) + + vec-Commutative-Monoid-Semigroup : ℕ → Semigroup l + vec-Commutative-Monoid-Semigroup = + vec-Monoid-Semigroup (monoid-Commutative-Monoid M) + + left-unit-law-add-vec-Commutative-Monoid : + {n : ℕ} (v : vec-Commutative-Monoid M n) → + add-vec-Commutative-Monoid (zero-vec-Commutative-Monoid M) v ＝ v + left-unit-law-add-vec-Commutative-Monoid = + left-unit-law-add-vec-Monoid (monoid-Commutative-Monoid M) + + right-unit-law-add-vec-Commutative-Monoid : + {n : ℕ} (v : vec-Commutative-Monoid M n) → + add-vec-Commutative-Monoid v (zero-vec-Commutative-Monoid M) ＝ v + right-unit-law-add-vec-Commutative-Monoid = + right-unit-law-add-vec-Monoid (monoid-Commutative-Monoid M) + + vec-Commutative-Monoid-Monoid : ℕ → Monoid l + vec-Commutative-Monoid-Monoid = + vec-Monoid-Monoid (monoid-Commutative-Monoid M) + + commutative-add-vec-Commutative-Monoid : + {n : ℕ} (v w : vec-Commutative-Monoid M n) → + add-vec-Commutative-Monoid v w ＝ add-vec-Commutative-Monoid w v + commutative-add-vec-Commutative-Monoid empty-vec empty-vec = refl + commutative-add-vec-Commutative-Monoid (x ∷ v1) (y ∷ v2) = + ap-binary _∷_ + (commutative-mul-Commutative-Monoid M x y) + (commutative-add-vec-Commutative-Monoid v1 v2) + + vec-Commutative-Monoid-Commutative-Monoid : ℕ → Commutative-Monoid l + vec-Commutative-Monoid-Commutative-Monoid n = + vec-Commutative-Monoid-Monoid n , + commutative-add-vec-Commutative-Monoid +``` + +#### Pointwise addition of functional vectors on a commutative monoid + +```agda +module _ + {l : Level} (M : Commutative-Monoid l) + where + + add-functional-vec-Commutative-Monoid : + (n : ℕ) (v w : functional-vec-Commutative-Monoid M n) → + functional-vec-Commutative-Monoid M n + add-functional-vec-Commutative-Monoid = + add-functional-vec-Monoid (monoid-Commutative-Monoid M) + + associative-add-functional-vec-Commutative-Monoid : + (n : ℕ) (v1 v2 v3 : functional-vec-Commutative-Monoid M n) → + ( add-functional-vec-Commutative-Monoid n + ( add-functional-vec-Commutative-Monoid n v1 v2) v3) ＝ + ( add-functional-vec-Commutative-Monoid n v1 + ( add-functional-vec-Commutative-Monoid n v2 v3)) + associative-add-functional-vec-Commutative-Monoid = + associative-add-functional-vec-Monoid (monoid-Commutative-Monoid M) + + functional-vec-Commutative-Monoid-Semigroup : ℕ → Semigroup l + functional-vec-Commutative-Monoid-Semigroup = + functional-vec-Monoid-Semigroup (monoid-Commutative-Monoid M) + + left-unit-law-add-functional-vec-Commutative-Monoid : + (n : ℕ) (v : functional-vec-Commutative-Monoid M n) → + add-functional-vec-Commutative-Monoid n + ( zero-functional-vec-Commutative-Monoid M n) v ＝ v + left-unit-law-add-functional-vec-Commutative-Monoid = + left-unit-law-add-functional-vec-Monoid (monoid-Commutative-Monoid M) + + right-unit-law-add-functional-vec-Commutative-Monoid : + (n : ℕ) (v : functional-vec-Commutative-Monoid M n) → + add-functional-vec-Commutative-Monoid n v + ( zero-functional-vec-Commutative-Monoid M n) ＝ v + right-unit-law-add-functional-vec-Commutative-Monoid = + right-unit-law-add-functional-vec-Monoid (monoid-Commutative-Monoid M) + + functional-vec-Commutative-Monoid-Monoid : ℕ → Monoid l + functional-vec-Commutative-Monoid-Monoid = + functional-vec-Monoid-Monoid (monoid-Commutative-Monoid M) + + commutative-add-functional-vec-Commutative-Monoid : + (n : ℕ) (v w : functional-vec-Commutative-Monoid M n) → + add-functional-vec-Commutative-Monoid n v w ＝ + add-functional-vec-Commutative-Monoid n w v + commutative-add-functional-vec-Commutative-Monoid _ _ _ = + eq-htpy (λ k → commutative-mul-Commutative-Monoid M _ _) + + functional-vec-Commutative-Monoid-Commutative-Monoid : + ℕ → Commutative-Monoid l + functional-vec-Commutative-Monoid-Commutative-Monoid n = + functional-vec-Commutative-Monoid-Monoid n , + commutative-add-functional-vec-Commutative-Monoid n +``` diff --git a/src/linear-algebra/vectors-on-monoids.lagda.md b/src/linear-algebra/vectors-on-monoids.lagda.md new file mode 100644 index 0000000000..eb934ccacd --- /dev/null +++ b/src/linear-algebra/vectors-on-monoids.lagda.md @@ -0,0 +1,213 @@ +# Vectors on monoids + +```agda +module linear-algebra.vectors-on-monoids where +``` + +
Imports + +```agda +open import elementary-number-theory.natural-numbers + +open import foundation.action-on-identifications-binary-functions +open import foundation.dependent-pair-types +open import foundation.function-extensionality +open import foundation.identity-types +open import foundation.universe-levels + +open import group-theory.monoids +open import group-theory.semigroups + +open import linear-algebra.constant-vectors +open import linear-algebra.functoriality-vectors +open import linear-algebra.vectors +``` + +
+ +## Idea + +Given a [monoid](group-theory.monoids.md) `M`, the type `vec n M` of +`n`-dimensional `M`-[vectors](linear-algebra.vectors.md) is a monoid given by +componentwise multiplication. + +We use additive terminology for vectors, as is standard in linear algebra +contexts, despite using multiplicative terminology for monoids. + +## Definitions + +### Listed vectors on monoids + +```agda +module _ + {l : Level} (M : Monoid l) + where + + vec-Monoid : ℕ → UU l + vec-Monoid = vec (type-Monoid M) + + head-vec-Monoid : {n : ℕ} → vec-Monoid (succ-ℕ n) → type-Monoid M + head-vec-Monoid v = head-vec v + + tail-vec-Monoid : {n : ℕ} → vec-Monoid (succ-ℕ n) → vec-Monoid n + tail-vec-Monoid v = tail-vec v + + snoc-vec-Monoid : + {n : ℕ} → vec-Monoid n → type-Monoid M → vec-Monoid (succ-ℕ n) + snoc-vec-Monoid v r = snoc-vec v r +``` + +### Functional vectors on monoids + +```agda +module _ + {l : Level} (M : Monoid l) + where + + functional-vec-Monoid : ℕ → UU l + functional-vec-Monoid = functional-vec (type-Monoid M) + + head-functional-vec-Monoid : + (n : ℕ) → functional-vec-Monoid (succ-ℕ n) → type-Monoid M + head-functional-vec-Monoid n v = head-functional-vec n v + + tail-functional-vec-Monoid : + (n : ℕ) → functional-vec-Monoid (succ-ℕ n) → functional-vec-Monoid n + tail-functional-vec-Monoid = tail-functional-vec + + cons-functional-vec-Monoid : + (n : ℕ) → type-Monoid M → + functional-vec-Monoid n → functional-vec-Monoid (succ-ℕ n) + cons-functional-vec-Monoid = cons-functional-vec + + snoc-functional-vec-Monoid : + (n : ℕ) → functional-vec-Monoid n → type-Monoid M → + functional-vec-Monoid (succ-ℕ n) + snoc-functional-vec-Monoid = snoc-functional-vec +``` + +### The zero vector + +#### The listed zero vector + +```agda +module _ + {l : Level} (M : Monoid l) + where + + zero-vec-Monoid : {n : ℕ} → vec-Monoid M n + zero-vec-Monoid = constant-vec (unit-Monoid M) +``` + +#### The functional zero vector + +```agda +module _ + {l : Level} (M : Monoid l) + where + + zero-functional-vec-Monoid : (n : ℕ) → functional-vec-Monoid M n + zero-functional-vec-Monoid n i = unit-Monoid M +``` + +### Pointwise addition of vectors on a monoid + +#### Pointwise addition of listed vectors on a monoid + +```agda +module _ + {l : Level} (M : Monoid l) + where + + add-vec-Monoid : + {n : ℕ} → vec-Monoid M n → vec-Monoid M n → vec-Monoid M n + add-vec-Monoid = binary-map-vec (mul-Monoid M) + + associative-add-vec-Monoid : + {n : ℕ} (v1 v2 v3 : vec-Monoid M n) → + add-vec-Monoid (add-vec-Monoid v1 v2) v3 ＝ + add-vec-Monoid v1 (add-vec-Monoid v2 v3) + associative-add-vec-Monoid empty-vec empty-vec empty-vec = refl + associative-add-vec-Monoid (x ∷ v1) (y ∷ v2) (z ∷ v3) = + ap-binary _∷_ + ( associative-mul-Monoid M x y z) + ( associative-add-vec-Monoid v1 v2 v3) + + vec-Monoid-Semigroup : ℕ → Semigroup l + pr1 (vec-Monoid-Semigroup n) = vec-Set (set-Monoid M) n + pr1 (pr2 (vec-Monoid-Semigroup n)) = add-vec-Monoid + pr2 (pr2 (vec-Monoid-Semigroup n)) = associative-add-vec-Monoid + + left-unit-law-add-vec-Monoid : + {n : ℕ} (v : vec-Monoid M n) → + add-vec-Monoid (zero-vec-Monoid M) v ＝ v + left-unit-law-add-vec-Monoid empty-vec = refl + left-unit-law-add-vec-Monoid (x ∷ v) = + ap-binary _∷_ + ( left-unit-law-mul-Monoid M x) + ( left-unit-law-add-vec-Monoid v) + + right-unit-law-add-vec-Monoid : + {n : ℕ} (v : vec-Monoid M n) → + add-vec-Monoid v (zero-vec-Monoid M) ＝ v + right-unit-law-add-vec-Monoid empty-vec = refl + right-unit-law-add-vec-Monoid (x ∷ v) = + ap-binary _∷_ + ( right-unit-law-mul-Monoid M x) + ( right-unit-law-add-vec-Monoid v) + + vec-Monoid-Monoid : ℕ → Monoid l + pr1 (vec-Monoid-Monoid n) = vec-Monoid-Semigroup n + pr1 (pr2 (vec-Monoid-Monoid n)) = zero-vec-Monoid M + pr1 (pr2 (pr2 (vec-Monoid-Monoid n))) = left-unit-law-add-vec-Monoid + pr2 (pr2 (pr2 (vec-Monoid-Monoid n))) = right-unit-law-add-vec-Monoid +``` + +#### Pointwise addition of functional vectors on a monoid + +```agda +module _ + {l : Level} (M : Monoid l) + where + + add-functional-vec-Monoid : + (n : ℕ) (v w : functional-vec-Monoid M n) → functional-vec-Monoid M n + add-functional-vec-Monoid n = binary-map-functional-vec n (mul-Monoid M) + + associative-add-functional-vec-Monoid : + (n : ℕ) (v1 v2 v3 : functional-vec-Monoid M n) → + ( add-functional-vec-Monoid n (add-functional-vec-Monoid n v1 v2) v3) ＝ + ( add-functional-vec-Monoid n v1 (add-functional-vec-Monoid n v2 v3)) + associative-add-functional-vec-Monoid n v1 v2 v3 = + eq-htpy (λ i → associative-mul-Monoid M (v1 i) (v2 i) (v3 i)) + + functional-vec-Monoid-Semigroup : ℕ → Semigroup l + pr1 (functional-vec-Monoid-Semigroup n) = + functional-vec-Set (set-Monoid M) n + pr1 (pr2 (functional-vec-Monoid-Semigroup n)) = + add-functional-vec-Monoid n + pr2 (pr2 (functional-vec-Monoid-Semigroup n)) = + associative-add-functional-vec-Monoid n + + left-unit-law-add-functional-vec-Monoid : + (n : ℕ) (v : functional-vec-Monoid M n) → + add-functional-vec-Monoid n (zero-functional-vec-Monoid M n) v ＝ v + left-unit-law-add-functional-vec-Monoid n v = + eq-htpy (λ i → left-unit-law-mul-Monoid M (v i)) + + right-unit-law-add-functional-vec-Monoid : + (n : ℕ) (v : functional-vec-Monoid M n) → + add-functional-vec-Monoid n v (zero-functional-vec-Monoid M n) ＝ v + right-unit-law-add-functional-vec-Monoid n v = + eq-htpy (λ i → right-unit-law-mul-Monoid M (v i)) + + functional-vec-Monoid-Monoid : ℕ → Monoid l + pr1 (functional-vec-Monoid-Monoid n) = + functional-vec-Monoid-Semigroup n + pr1 (pr2 (functional-vec-Monoid-Monoid n)) = + zero-functional-vec-Monoid M n + pr1 (pr2 (pr2 (functional-vec-Monoid-Monoid n))) = + left-unit-law-add-functional-vec-Monoid n + pr2 (pr2 (pr2 (functional-vec-Monoid-Monoid n))) = + right-unit-law-add-functional-vec-Monoid n +``` diff --git a/src/linear-algebra/vectors-on-semirings.lagda.md b/src/linear-algebra/vectors-on-semirings.lagda.md index c66387088a..788dfd5770 100644 --- a/src/linear-algebra/vectors-on-semirings.lagda.md +++ b/src/linear-algebra/vectors-on-semirings.lagda.md @@ -22,6 +22,7 @@ open import group-theory.semigroups open import linear-algebra.constant-vectors open import linear-algebra.functoriality-vectors open import linear-algebra.vectors +open import linear-algebra.vectors-on-commutative-monoids open import ring-theory.semirings ``` @@ -42,7 +43,7 @@ module _ where vec-Semiring : ℕ → UU l - vec-Semiring = vec (type-Semiring R) + vec-Semiring = vec-Commutative-Monoid (additive-commutative-monoid-Semiring R) head-vec-Semiring : {n : ℕ} → vec-Semiring (succ-ℕ n) → type-Semiring R head-vec-Semiring v = head-vec v @@ -63,7 +64,8 @@ module _ where functional-vec-Semiring : ℕ → UU l - functional-vec-Semiring = functional-vec (type-Semiring R) + functional-vec-Semiring = + functional-vec-Commutative-Monoid (additive-commutative-monoid-Semiring R) head-functional-vec-Semiring : (n : ℕ) → functional-vec-Semiring (succ-ℕ n) → type-Semiring R @@ -94,7 +96,8 @@ module _ where zero-vec-Semiring : {n : ℕ} → vec-Semiring R n - zero-vec-Semiring = constant-vec (zero-Semiring R) + zero-vec-Semiring = + zero-vec-Commutative-Monoid (additive-commutative-monoid-Semiring R) ``` #### The zero functional vector @@ -119,59 +122,51 @@ module _ add-vec-Semiring : {n : ℕ} → vec-Semiring R n → vec-Semiring R n → vec-Semiring R n - add-vec-Semiring = binary-map-vec (add-Semiring R) + add-vec-Semiring = + add-vec-Commutative-Monoid (additive-commutative-monoid-Semiring R) associative-add-vec-Semiring : {n : ℕ} (v1 v2 v3 : vec-Semiring R n) → add-vec-Semiring (add-vec-Semiring v1 v2) v3 ＝ add-vec-Semiring v1 (add-vec-Semiring v2 v3) - associative-add-vec-Semiring empty-vec empty-vec empty-vec = refl - associative-add-vec-Semiring (x ∷ v1) (y ∷ v2) (z ∷ v3) = - ap-binary _∷_ - ( associative-add-Semiring R x y z) - ( associative-add-vec-Semiring v1 v2 v3) + associative-add-vec-Semiring = + associative-add-vec-Commutative-Monoid + ( additive-commutative-monoid-Semiring R) vec-Semiring-Semigroup : ℕ → Semigroup l - pr1 (vec-Semiring-Semigroup n) = vec-Set (set-Semiring R) n - pr1 (pr2 (vec-Semiring-Semigroup n)) = add-vec-Semiring - pr2 (pr2 (vec-Semiring-Semigroup n)) = associative-add-vec-Semiring + vec-Semiring-Semigroup = + vec-Commutative-Monoid-Semigroup (additive-commutative-monoid-Semiring R) left-unit-law-add-vec-Semiring : {n : ℕ} (v : vec-Semiring R n) → add-vec-Semiring (zero-vec-Semiring R) v ＝ v - left-unit-law-add-vec-Semiring empty-vec = refl - left-unit-law-add-vec-Semiring (x ∷ v) = - ap-binary _∷_ - ( left-unit-law-add-Semiring R x) - ( left-unit-law-add-vec-Semiring v) + left-unit-law-add-vec-Semiring = + left-unit-law-add-vec-Commutative-Monoid + ( additive-commutative-monoid-Semiring R) right-unit-law-add-vec-Semiring : {n : ℕ} (v : vec-Semiring R n) → add-vec-Semiring v (zero-vec-Semiring R) ＝ v - right-unit-law-add-vec-Semiring empty-vec = refl - right-unit-law-add-vec-Semiring (x ∷ v) = - ap-binary _∷_ - ( right-unit-law-add-Semiring R x) - ( right-unit-law-add-vec-Semiring v) + right-unit-law-add-vec-Semiring = + right-unit-law-add-vec-Commutative-Monoid + ( additive-commutative-monoid-Semiring R) vec-Semiring-Monoid : ℕ → Monoid l - pr1 (vec-Semiring-Monoid n) = vec-Semiring-Semigroup n - pr1 (pr2 (vec-Semiring-Monoid n)) = zero-vec-Semiring R - pr1 (pr2 (pr2 (vec-Semiring-Monoid n))) = left-unit-law-add-vec-Semiring - pr2 (pr2 (pr2 (vec-Semiring-Monoid n))) = right-unit-law-add-vec-Semiring + vec-Semiring-Monoid = + vec-Commutative-Monoid-Monoid + ( additive-commutative-monoid-Semiring R) commutative-add-vec-Semiring : {n : ℕ} (v w : vec-Semiring R n) → add-vec-Semiring v w ＝ add-vec-Semiring w v - commutative-add-vec-Semiring empty-vec empty-vec = refl - commutative-add-vec-Semiring (x ∷ v) (y ∷ w) = - ap-binary _∷_ - ( commutative-add-Semiring R x y) - ( commutative-add-vec-Semiring v w) + commutative-add-vec-Semiring = + commutative-add-vec-Commutative-Monoid + ( additive-commutative-monoid-Semiring R) vec-Semiring-Commutative-Monoid : ℕ → Commutative-Monoid l - pr1 (vec-Semiring-Commutative-Monoid n) = vec-Semiring-Monoid n - pr2 (vec-Semiring-Commutative-Monoid n) = commutative-add-vec-Semiring + vec-Semiring-Commutative-Monoid = + vec-Commutative-Monoid-Commutative-Monoid + ( additive-commutative-monoid-Semiring R) ``` #### Pointwise addition of functional vectors on a ring @@ -183,54 +178,51 @@ module _ add-functional-vec-Semiring : (n : ℕ) (v w : functional-vec-Semiring R n) → functional-vec-Semiring R n - add-functional-vec-Semiring n = binary-map-functional-vec n (add-Semiring R) + add-functional-vec-Semiring = + add-functional-vec-Commutative-Monoid + ( additive-commutative-monoid-Semiring R) associative-add-functional-vec-Semiring : (n : ℕ) (v1 v2 v3 : functional-vec-Semiring R n) → ( add-functional-vec-Semiring n (add-functional-vec-Semiring n v1 v2) v3) ＝ ( add-functional-vec-Semiring n v1 (add-functional-vec-Semiring n v2 v3)) - associative-add-functional-vec-Semiring n v1 v2 v3 = - eq-htpy (λ i → associative-add-Semiring R (v1 i) (v2 i) (v3 i)) + associative-add-functional-vec-Semiring = + associative-add-functional-vec-Commutative-Monoid + ( additive-commutative-monoid-Semiring R) functional-vec-Semiring-Semigroup : ℕ → Semigroup l - pr1 (functional-vec-Semiring-Semigroup n) = - functional-vec-Set (set-Semiring R) n - pr1 (pr2 (functional-vec-Semiring-Semigroup n)) = - add-functional-vec-Semiring n - pr2 (pr2 (functional-vec-Semiring-Semigroup n)) = - associative-add-functional-vec-Semiring n + functional-vec-Semiring-Semigroup = + functional-vec-Commutative-Monoid-Semigroup + ( additive-commutative-monoid-Semiring R) left-unit-law-add-functional-vec-Semiring : (n : ℕ) (v : functional-vec-Semiring R n) → add-functional-vec-Semiring n (zero-functional-vec-Semiring R n) v ＝ v - left-unit-law-add-functional-vec-Semiring n v = - eq-htpy (λ i → left-unit-law-add-Semiring R (v i)) + left-unit-law-add-functional-vec-Semiring = + left-unit-law-add-functional-vec-Commutative-Monoid + ( additive-commutative-monoid-Semiring R) right-unit-law-add-functional-vec-Semiring : (n : ℕ) (v : functional-vec-Semiring R n) → add-functional-vec-Semiring n v (zero-functional-vec-Semiring R n) ＝ v - right-unit-law-add-functional-vec-Semiring n v = - eq-htpy (λ i → right-unit-law-add-Semiring R (v i)) + right-unit-law-add-functional-vec-Semiring = + right-unit-law-add-functional-vec-Commutative-Monoid + ( additive-commutative-monoid-Semiring R) functional-vec-Semiring-Monoid : ℕ → Monoid l - pr1 (functional-vec-Semiring-Monoid n) = - functional-vec-Semiring-Semigroup n - pr1 (pr2 (functional-vec-Semiring-Monoid n)) = - zero-functional-vec-Semiring R n - pr1 (pr2 (pr2 (functional-vec-Semiring-Monoid n))) = - left-unit-law-add-functional-vec-Semiring n - pr2 (pr2 (pr2 (functional-vec-Semiring-Monoid n))) = - right-unit-law-add-functional-vec-Semiring n + functional-vec-Semiring-Monoid = + functional-vec-Commutative-Monoid-Monoid + ( additive-commutative-monoid-Semiring R) commutative-add-functional-vec-Semiring : (n : ℕ) (v w : functional-vec-Semiring R n) → add-functional-vec-Semiring n v w ＝ add-functional-vec-Semiring n w v - commutative-add-functional-vec-Semiring n v w = - eq-htpy (λ i → commutative-add-Semiring R (v i) (w i)) + commutative-add-functional-vec-Semiring = + commutative-add-functional-vec-Commutative-Monoid + ( additive-commutative-monoid-Semiring R) functional-vec-Semiring-Commutative-Monoid : ℕ → Commutative-Monoid l - pr1 (functional-vec-Semiring-Commutative-Monoid n) = - functional-vec-Semiring-Monoid n - pr2 (functional-vec-Semiring-Commutative-Monoid n) = - commutative-add-functional-vec-Semiring n + functional-vec-Semiring-Commutative-Monoid = + functional-vec-Commutative-Monoid-Commutative-Monoid + ( additive-commutative-monoid-Semiring R) ``` diff --git a/src/logic/complements-decidable-subtypes.lagda.md b/src/logic/complements-decidable-subtypes.lagda.md index ae2a775f33..ee474aa92e 100644 --- a/src/logic/complements-decidable-subtypes.lagda.md +++ b/src/logic/complements-decidable-subtypes.lagda.md @@ -13,7 +13,9 @@ open import foundation.decidable-propositions open import foundation.decidable-subtypes open import foundation.decidable-types open import foundation.dependent-pair-types +open import foundation.disjoint-subtypes open import foundation.double-negation-stable-propositions +open import foundation.equivalences open import foundation.evaluation-functions open import foundation.full-subtypes open import foundation.involutions @@ -51,6 +53,16 @@ complement-decidable-subtype P x = neg-Decidable-Prop (P x) ## Properties +### The complement of a decidable subtype is disjoint from the subtype + +```agda +disjoint-complement-decidable-subtype : + {l1 l2 : Level} {A : UU l1} (P : decidable-subtype l2 A) → + disjoint-decidable-subtype P (complement-decidable-subtype P) +disjoint-complement-decidable-subtype P = + disjoint-complement-subtype (subtype-decidable-subtype P) +``` + ### Taking complements is an involution on decidable subtypes ```agda @@ -98,3 +110,26 @@ module _ ( subtype-decidable-subtype P) ( is-decidable-decidable-subtype P) ``` + +### `A` is equivalent to the coproduct of a decidable subtype and its complement + +```agda +module _ + {l1 l2 : Level} {A : UU l1} (P : decidable-subtype l2 A) + where + + equiv-coproduct-subtype-complement-decidable-subtype : + A ≃ + type-decidable-subtype P + + type-decidable-subtype (complement-decidable-subtype P) + equiv-coproduct-subtype-complement-decidable-subtype = + equiv-union-coproduct-disjoint-subtype + ( subtype-decidable-subtype P) + ( subtype-decidable-subtype (complement-decidable-subtype P)) + ( disjoint-complement-decidable-subtype P) ∘e + inv-equiv + ( equiv-inclusion-is-full-subtype + ( subtype-decidable-subtype + ( union-decidable-subtype P (complement-decidable-subtype P))) + ( is-full-union-subtype-complement-decidable-subtype P)) +``` diff --git a/src/ring-theory/sums-rings.lagda.md b/src/ring-theory/sums-rings.lagda.md index f2f5859aa9..78a33c9046 100644 --- a/src/ring-theory/sums-rings.lagda.md +++ b/src/ring-theory/sums-rings.lagda.md @@ -10,9 +10,15 @@ module ring-theory.sums-rings where open import elementary-number-theory.addition-natural-numbers open import elementary-number-theory.natural-numbers +open import finite-group-theory.permutations-standard-finite-types + +open import foundation.coproduct-types +open import foundation.empty-types +open import foundation.equivalences open import foundation.function-types open import foundation.homotopies open import foundation.identity-types +open import foundation.unit-type open import foundation.universe-levels open import linear-algebra.vectors @@ -22,6 +28,9 @@ open import ring-theory.rings open import ring-theory.sums-semirings open import univalent-combinatorics.coproduct-types +open import univalent-combinatorics.counting +open import univalent-combinatorics.dependent-pair-types +open import univalent-combinatorics.finite-types open import univalent-combinatorics.standard-finite-types ``` @@ -29,8 +38,12 @@ open import univalent-combinatorics.standard-finite-types ## Idea -The sum operation extends the binary addition operation on a ring `R` to any -family of elements of `R` indexed by a standard finite type. +The +{{#concept "sum operation" Disambiguation="in a ring" WD="sum" WDID=Q218005 Agda=sum-Ring}} +extends the binary addition operation on a [ring](ring-theory.rings.md) `R` to +any family of elements of `R` indexed by a +[standard finite type](univalent-combinatorics.standard-finite-types.md), or by +a [finite type](univalent-combinatorics.finite-types.md). ## Definition @@ -38,6 +51,16 @@ family of elements of `R` indexed by a standard finite type. sum-Ring : {l : Level} (R : Ring l) (n : ℕ) → functional-vec-Ring R n → type-Ring R sum-Ring R = sum-Semiring (semiring-Ring R) + +sum-count-Ring : + {l1 l2 : Level} (R : Ring l1) (A : UU l2) → count A → (A → type-Ring R) → + type-Ring R +sum-count-Ring R = sum-count-Semiring (semiring-Ring R) + +sum-finite-Ring : + {l1 l2 : Level} (R : Ring l1) (A : Finite-Type l2) → + (type-Finite-Type A → type-Ring R) → type-Ring R +sum-finite-Ring R = sum-finite-Semiring (semiring-Ring R) ``` ## Properties @@ -53,6 +76,10 @@ module _ (f : functional-vec-Ring R 1) → sum-Ring R 1 f ＝ head-functional-vec 0 f sum-one-element-Ring = sum-one-element-Semiring (semiring-Ring R) + sum-unit-finite-Ring : + (f : unit → type-Ring R) → sum-finite-Ring R unit-Finite-Type f ＝ f star + sum-unit-finite-Ring = sum-unit-finite-Semiring (semiring-Ring R) + sum-two-elements-Ring : (f : functional-vec-Ring R 2) → sum-Ring R 2 f ＝ add-Ring R (f (zero-Fin 1)) (f (one-Fin 1)) @@ -70,6 +97,12 @@ module _ (n : ℕ) {f g : functional-vec-Ring R n} → (f ~ g) → sum-Ring R n f ＝ sum-Ring R n g htpy-sum-Ring = htpy-sum-Semiring (semiring-Ring R) + + htpy-sum-finite-Ring : + {l2 : Level} (A : Finite-Type l2) → + {f g : type-Finite-Type A → type-Ring R} → (f ~ g) → + sum-finite-Ring R A f ＝ sum-finite-Ring R A g + htpy-sum-finite-Ring = htpy-sum-finite-Semiring (semiring-Ring R) ``` ### Sums are equal to the zero-th term plus the rest @@ -118,6 +151,22 @@ module _ sum-Ring R n (λ i → mul-Ring R (f i) x) right-distributive-mul-sum-Ring = right-distributive-mul-sum-Semiring (semiring-Ring R) + + left-distributive-mul-sum-finite-Ring : + {l2 : Level} (A : Finite-Type l2) (x : type-Ring R) → + (f : type-Finite-Type A → type-Ring R) → + mul-Ring R x (sum-finite-Ring R A f) ＝ + sum-finite-Ring R A (mul-Ring R x ∘ f) + left-distributive-mul-sum-finite-Ring = + left-distributive-mul-sum-finite-Semiring (semiring-Ring R) + + right-distributive-mul-sum-finite-Ring : + {l2 : Level} (A : Finite-Type l2) → + (f : type-Finite-Type A → type-Ring R) (x : type-Ring R) → + mul-Ring R (sum-finite-Ring R A f) x ＝ + sum-finite-Ring R A (mul-Ring' R x ∘ f) + right-distributive-mul-sum-finite-Ring = + right-distributive-mul-sum-finite-Semiring (semiring-Ring R) ``` ### Interchange law of sums and addition in a semiring @@ -180,6 +229,11 @@ module _ sum-zero-Ring : (n : ℕ) → sum-Ring R n (zero-functional-vec-Ring R n) ＝ zero-Ring R sum-zero-Ring = sum-zero-Semiring (semiring-Ring R) + + sum-zero-finite-Ring : + {l2 : Level} (A : Finite-Type l2) → + sum-finite-Ring R A (λ _ → zero-Ring R) ＝ zero-Ring R + sum-zero-finite-Ring = sum-zero-finite-Semiring (semiring-Ring R) ``` ### Splitting sums @@ -194,3 +248,92 @@ split-sum-Ring : ( sum-Ring R m (f ∘ inr-coproduct-Fin n m)) split-sum-Ring R = split-sum-Semiring (semiring-Ring R) ``` + +### Permutations preserve sums + +```agda +module _ + {l : Level} (R : Ring l) + where + + preserves-sum-permutation-Ring : + (n : ℕ) → (σ : Permutation n) → + (f : functional-vec-Ring R n) → + sum-Ring R n f ＝ sum-Ring R n (f ∘ map-equiv σ) + preserves-sum-permutation-Ring = + preserves-sum-permutation-Semiring (semiring-Ring R) +``` + +### Sums over finite types are preserved by equivalences + +```agda +module _ + {l1 l2 l3 : Level} (R : Ring l1) (A : Finite-Type l2) (B : Finite-Type l3) + (H : equiv-Finite-Type A B) + where + + sum-equiv-finite-Ring : + (f : type-Finite-Type A → type-Ring R) → + sum-finite-Ring R A f ＝ + sum-finite-Ring R B (f ∘ map-inv-equiv H) + sum-equiv-finite-Ring = sum-equiv-finite-Semiring (semiring-Ring R) A B H +``` + +### Sums over finite types distribute over coproducts + +```agda +module _ + {l1 l2 l3 : Level} (R : Ring l1) + (A : Finite-Type l2) (B : Finite-Type l3) + where + + sum-coproduct-finite-Ring : + (f : + type-Finite-Type A + type-Finite-Type B → type-Ring R) → + sum-finite-Ring R (coproduct-Finite-Type A B) f ＝ + add-Ring + ( R) + ( sum-finite-Ring R A (f ∘ inl)) + ( sum-finite-Ring R B (f ∘ inr)) + sum-coproduct-finite-Ring = + sum-coproduct-finite-Semiring (semiring-Ring R) A B +``` + +### Sums distribute over dependent pair types + +```agda +module _ + {l1 l2 l3 : Level} (R : Ring l1) + (A : Finite-Type l2) (B : type-Finite-Type A → Finite-Type l3) + where + + sum-Σ-finite-Ring : + (f : (a : type-Finite-Type A) → type-Finite-Type (B a) → type-Ring R) → + sum-finite-Ring R (Σ-Finite-Type A B) (ind-Σ f) ＝ + sum-finite-Ring R A (λ a → sum-finite-Ring R (B a) (f a)) + sum-Σ-finite-Ring = sum-Σ-finite-Semiring (semiring-Ring R) A B +``` + +### The sum over an empty type is zero + +```agda +module _ + {l1 l2 : Level} (R : Ring l1) (A : Finite-Type l2) + (H : is-empty (type-Finite-Type A)) + where + + sum-is-empty-finite-Ring : + (f : type-Finite-Type A → type-Ring R) → + is-zero-Ring R (sum-finite-Ring R A f) + sum-is-empty-finite-Ring = sum-is-empty-finite-Semiring (semiring-Ring R) A H +``` + +### The sum over a finite type is the sum over any count for that type + +```agda +sum-finite-count-Ring : + {l1 l2 : Level} (R : Ring l1) (A : Finite-Type l2) + (cA : count (type-Finite-Type A)) (f : type-Finite-Type A → type-Ring R) → + sum-finite-Ring R A f ＝ sum-count-Ring R (type-Finite-Type A) cA f +sum-finite-count-Ring R = sum-finite-count-Semiring (semiring-Ring R) +``` diff --git a/src/ring-theory/sums-semirings.lagda.md b/src/ring-theory/sums-semirings.lagda.md index 3f42f0a446..9c33476171 100644 --- a/src/ring-theory/sums-semirings.lagda.md +++ b/src/ring-theory/sums-semirings.lagda.md @@ -10,14 +10,21 @@ module ring-theory.sums-semirings where open import elementary-number-theory.addition-natural-numbers open import elementary-number-theory.natural-numbers +open import finite-group-theory.permutations-standard-finite-types + open import foundation.action-on-identifications-functions open import foundation.coproduct-types +open import foundation.empty-types +open import foundation.equivalences open import foundation.function-types open import foundation.homotopies open import foundation.identity-types +open import foundation.propositional-truncations +open import foundation.sets open import foundation.unit-type open import foundation.universe-levels -open import foundation.whiskering-homotopies-composition + +open import group-theory.products-of-tuples-of-elements-commutative-monoids open import linear-algebra.vectors open import linear-algebra.vectors-on-semirings @@ -25,6 +32,9 @@ open import linear-algebra.vectors-on-semirings open import ring-theory.semirings open import univalent-combinatorics.coproduct-types +open import univalent-combinatorics.counting +open import univalent-combinatorics.dependent-pair-types +open import univalent-combinatorics.finite-types open import univalent-combinatorics.standard-finite-types ``` @@ -32,8 +42,12 @@ open import univalent-combinatorics.standard-finite-types ## Idea -The sum operation extends the binary addition operation on a semiring `R` to any -family of elements of `R` indexed by a standard finite type. +The +{{#concept "sum operation" Disambiguation="in a semiring" WD="sum" WDID=Q218005 Agda=sum-Semiring}} +extends the binary addition operation on a [semiring](ring-theory.semirings.md) +`R` to any family of elements of `R` indexed by a +[standard finite type](univalent-combinatorics.standard-finite-types.md), or by +a [finite type](univalent-combinatorics.finite-types.md). ## Definition @@ -41,11 +55,20 @@ family of elements of `R` indexed by a standard finite type. sum-Semiring : {l : Level} (R : Semiring l) (n : ℕ) → (functional-vec-Semiring R n) → type-Semiring R -sum-Semiring R zero-ℕ f = zero-Semiring R -sum-Semiring R (succ-ℕ n) f = - add-Semiring R - ( sum-Semiring R n (f ∘ inl-Fin n)) - ( f (inr star)) +sum-Semiring R = + mul-fin-Commutative-Monoid (additive-commutative-monoid-Semiring R) + +sum-count-Semiring : + {l1 l2 : Level} (R : Semiring l1) (A : UU l2) (cA : count A) → + (A → type-Semiring R) → type-Semiring R +sum-count-Semiring R = + mul-count-Commutative-Monoid (additive-commutative-monoid-Semiring R) + +sum-finite-Semiring : + {l1 l2 : Level} (R : Semiring l1) (A : Finite-Type l2) → + (type-Finite-Type A → type-Semiring R) → type-Semiring R +sum-finite-Semiring R = + mul-finite-Commutative-Monoid (additive-commutative-monoid-Semiring R) ``` ## Properties @@ -60,17 +83,22 @@ module _ sum-one-element-Semiring : (f : functional-vec-Semiring R 1) → sum-Semiring R 1 f ＝ head-functional-vec 0 f - sum-one-element-Semiring f = - left-unit-law-add-Semiring R (f (inr star)) + sum-one-element-Semiring = + mul-one-element-Commutative-Monoid + ( additive-commutative-monoid-Semiring R) + + sum-unit-finite-Semiring : + (f : unit → type-Semiring R) → + sum-finite-Semiring R unit-Finite-Type f ＝ f star + sum-unit-finite-Semiring = + mul-unit-finite-Commutative-Monoid (additive-commutative-monoid-Semiring R) sum-two-elements-Semiring : (f : functional-vec-Semiring R 2) → sum-Semiring R 2 f ＝ add-Semiring R (f (zero-Fin 1)) (f (one-Fin 1)) - sum-two-elements-Semiring f = - ( associative-add-Semiring R - (zero-Semiring R) (f (zero-Fin 1)) (f (one-Fin 1))) ∙ - ( left-unit-law-add-Semiring R - ( add-Semiring R (f (zero-Fin 1)) (f (one-Fin 1)))) + sum-two-elements-Semiring = + mul-two-elements-Commutative-Monoid + ( additive-commutative-monoid-Semiring R) ``` ### Sums are homotopy invariant @@ -83,11 +111,15 @@ module _ htpy-sum-Semiring : (n : ℕ) {f g : functional-vec-Semiring R n} → (f ~ g) → sum-Semiring R n f ＝ sum-Semiring R n g - htpy-sum-Semiring zero-ℕ H = refl - htpy-sum-Semiring (succ-ℕ n) H = - ap-add-Semiring R - ( htpy-sum-Semiring n (H ·r inl-Fin n)) - ( H (inr star)) + htpy-sum-Semiring = + htpy-mul-fin-Commutative-Monoid (additive-commutative-monoid-Semiring R) + + htpy-sum-finite-Semiring : + {l2 : Level} (A : Finite-Type l2) → + {f g : type-Finite-Type A → type-Semiring R} → (f ~ g) → + sum-finite-Semiring R A f ＝ sum-finite-Semiring R A g + htpy-sum-finite-Semiring = + htpy-mul-finite-Commutative-Monoid (additive-commutative-monoid-Semiring R) ``` ### Sums are equal to the zero-th term plus the rest @@ -111,17 +143,8 @@ module _ add-Semiring R ( x) ( sum-Semiring R n (f ∘ inr-Fin n)) - snoc-sum-Semiring zero-ℕ f refl = - ( sum-one-element-Semiring R f) ∙ - ( inv (right-unit-law-add-Semiring R (f (zero-Fin 0)))) - snoc-sum-Semiring (succ-ℕ n) f refl = - ( ap - ( add-Semiring' R (head-functional-vec (succ-ℕ n) f)) - ( snoc-sum-Semiring n (f ∘ inl-Fin (succ-ℕ n)) refl)) ∙ - ( associative-add-Semiring R - ( f (zero-Fin (succ-ℕ n))) - ( sum-Semiring R n (f ∘ (inr-Fin (succ-ℕ n) ∘ inl-Fin n))) - ( head-functional-vec (succ-ℕ n) f)) + snoc-sum-Semiring = + snoc-mul-fin-Commutative-Monoid (additive-commutative-monoid-Semiring R) ``` ### Multiplication distributes over sums @@ -131,36 +154,125 @@ module _ {l : Level} (R : Semiring l) where - left-distributive-mul-sum-Semiring : - (n : ℕ) (x : type-Semiring R) - (f : functional-vec-Semiring R n) → - mul-Semiring R x (sum-Semiring R n f) ＝ - sum-Semiring R n (λ i → mul-Semiring R x (f i)) - left-distributive-mul-sum-Semiring zero-ℕ x f = - right-zero-law-mul-Semiring R x - left-distributive-mul-sum-Semiring (succ-ℕ n) x f = - ( left-distributive-mul-add-Semiring R x - ( sum-Semiring R n (f ∘ inl-Fin n)) - ( f (inr star))) ∙ - ( ap - ( add-Semiring' R (mul-Semiring R x (f (inr star)))) - ( left-distributive-mul-sum-Semiring n x (f ∘ inl-Fin n))) - - right-distributive-mul-sum-Semiring : - (n : ℕ) (f : functional-vec-Semiring R n) - (x : type-Semiring R) → - mul-Semiring R (sum-Semiring R n f) x ＝ - sum-Semiring R n (λ i → mul-Semiring R (f i) x) - right-distributive-mul-sum-Semiring zero-ℕ f x = - left-zero-law-mul-Semiring R x - right-distributive-mul-sum-Semiring (succ-ℕ n) f x = - ( right-distributive-mul-add-Semiring R - ( sum-Semiring R n (f ∘ inl-Fin n)) - ( f (inr star)) - ( x)) ∙ - ( ap - ( add-Semiring' R (mul-Semiring R (f (inr star)) x)) - ( right-distributive-mul-sum-Semiring n (f ∘ inl-Fin n) x)) + abstract + left-distributive-mul-sum-Semiring : + (n : ℕ) (x : type-Semiring R) + (f : functional-vec-Semiring R n) → + mul-Semiring R x (sum-Semiring R n f) ＝ + sum-Semiring R n (λ i → mul-Semiring R x (f i)) + left-distributive-mul-sum-Semiring zero-ℕ x f = + right-zero-law-mul-Semiring R x + left-distributive-mul-sum-Semiring (succ-ℕ n) x f = + ( left-distributive-mul-add-Semiring R x + ( sum-Semiring R n (f ∘ inl-Fin n)) + ( f (inr star))) ∙ + ( ap + ( add-Semiring' R (mul-Semiring R x (f (inr star)))) + ( left-distributive-mul-sum-Semiring n x (f ∘ inl-Fin n))) + + right-distributive-mul-sum-Semiring : + (n : ℕ) (f : functional-vec-Semiring R n) + (x : type-Semiring R) → + mul-Semiring R (sum-Semiring R n f) x ＝ + sum-Semiring R n (λ i → mul-Semiring R (f i) x) + right-distributive-mul-sum-Semiring zero-ℕ f x = + left-zero-law-mul-Semiring R x + right-distributive-mul-sum-Semiring (succ-ℕ n) f x = + ( right-distributive-mul-add-Semiring R + ( sum-Semiring R n (f ∘ inl-Fin n)) + ( f (inr star)) + ( x)) ∙ + ( ap + ( add-Semiring' R (mul-Semiring R (f (inr star)) x)) + ( right-distributive-mul-sum-Semiring n (f ∘ inl-Fin n) x)) + + left-distributive-mul-sum-finite-Semiring : + {l2 : Level} (A : Finite-Type l2) (x : type-Semiring R) → + (f : type-Finite-Type A → type-Semiring R) → + mul-Semiring R x (sum-finite-Semiring R A f) ＝ + sum-finite-Semiring R A (mul-Semiring R x ∘ f) + left-distributive-mul-sum-finite-Semiring A x f = + let + open + do-syntax-trunc-Prop + ( Id-Prop + ( set-Semiring R) + ( mul-Semiring R x (sum-finite-Semiring R A f)) + ( sum-finite-Semiring R A (mul-Semiring R x ∘ f))) + in do + cA ← is-finite-type-Finite-Type A + equational-reasoning + mul-Semiring R x (sum-finite-Semiring R A f) + ＝ + mul-Semiring + ( R) + ( x) + ( mul-count-Commutative-Monoid + ( additive-commutative-monoid-Semiring R) + ( type-Finite-Type A) + ( cA) + ( f)) + by + ap + ( mul-Semiring R x) + ( mul-finite-count-Commutative-Monoid _ A cA f) + ＝ + mul-count-Commutative-Monoid + ( additive-commutative-monoid-Semiring R) + ( type-Finite-Type A) + ( cA) + ( mul-Semiring R x ∘ f) + by + left-distributive-mul-sum-Semiring + ( number-of-elements-count cA) + ( x) + ( f ∘ map-equiv-count cA) + ＝ sum-finite-Semiring R A (mul-Semiring R x ∘ f) + by inv (mul-finite-count-Commutative-Monoid _ A cA _) + + right-distributive-mul-sum-finite-Semiring : + {l2 : Level} (A : Finite-Type l2) → + (f : type-Finite-Type A → type-Semiring R) (x : type-Semiring R) → + mul-Semiring R (sum-finite-Semiring R A f) x ＝ + sum-finite-Semiring R A (mul-Semiring' R x ∘ f) + right-distributive-mul-sum-finite-Semiring A f x = + let + open + do-syntax-trunc-Prop + ( Id-Prop + ( set-Semiring R) + ( mul-Semiring R (sum-finite-Semiring R A f) x) + ( sum-finite-Semiring R A (mul-Semiring' R x ∘ f))) + in do + cA ← is-finite-type-Finite-Type A + equational-reasoning + mul-Semiring R (sum-finite-Semiring R A f) x + ＝ + mul-Semiring + ( R) + ( mul-count-Commutative-Monoid + ( additive-commutative-monoid-Semiring R) + ( type-Finite-Type A) + ( cA) + ( f)) + ( x) + by + ap + ( mul-Semiring' R x) + ( mul-finite-count-Commutative-Monoid _ A cA f) + ＝ + mul-count-Commutative-Monoid + ( additive-commutative-monoid-Semiring R) + ( type-Finite-Type A) + ( cA) + ( mul-Semiring' R x ∘ f) + by + right-distributive-mul-sum-Semiring + ( number-of-elements-count cA) + ( f ∘ map-equiv-count cA) + ( x) + ＝ sum-finite-Semiring R A (mul-Semiring' R x ∘ f) + by inv (mul-finite-count-Commutative-Monoid _ A cA _) ``` ### Interchange law of sums and addition in a semiring @@ -206,8 +318,8 @@ module _ ( succ-ℕ n) ( cons-functional-vec-Semiring R n (zero-Semiring R) f) ＝ sum-Semiring R n f - extend-sum-Semiring n f = - right-unit-law-add-Semiring R (sum-Semiring R n f) + extend-sum-Semiring = + extend-mul-fin-Commutative-Monoid (additive-commutative-monoid-Semiring R) ``` ### Shifting a sum of elements in a semiring @@ -224,14 +336,8 @@ module _ ( snoc-functional-vec-Semiring R n f ( zero-Semiring R)) ＝ sum-Semiring R n f - shift-sum-Semiring zero-ℕ f = - left-unit-law-add-Semiring R (zero-Semiring R) - shift-sum-Semiring (succ-ℕ n) f = - ap - ( add-Semiring' R - ( head-functional-vec-Semiring R n f)) - ( shift-sum-Semiring n - ( tail-functional-vec-Semiring R n f)) + shift-sum-Semiring = + shift-mul-fin-Commutative-Monoid (additive-commutative-monoid-Semiring R) ``` ### A sum of zeroes is zero @@ -244,9 +350,14 @@ module _ sum-zero-Semiring : (n : ℕ) → sum-Semiring R n (zero-functional-vec-Semiring R n) ＝ zero-Semiring R - sum-zero-Semiring zero-ℕ = refl - sum-zero-Semiring (succ-ℕ n) = - right-unit-law-add-Semiring R _ ∙ sum-zero-Semiring n + sum-zero-Semiring = + mul-fin-unit-Commutative-Monoid (additive-commutative-monoid-Semiring R) + + sum-zero-finite-Semiring : + {l2 : Level} (A : Finite-Type l2) → + sum-finite-Semiring R A (λ _ → zero-Semiring R) ＝ zero-Semiring R + sum-zero-finite-Semiring = + mul-finite-unit-Commutative-Monoid (additive-commutative-monoid-Semiring R) ``` ### Splitting sums @@ -259,11 +370,110 @@ split-sum-Semiring : add-Semiring R ( sum-Semiring R n (f ∘ inl-coproduct-Fin n m)) ( sum-Semiring R m (f ∘ inr-coproduct-Fin n m)) -split-sum-Semiring R n zero-ℕ f = - inv (right-unit-law-add-Semiring R (sum-Semiring R n f)) -split-sum-Semiring R n (succ-ℕ m) f = - ( ap - ( add-Semiring' R (f (inr star))) - ( split-sum-Semiring R n m (f ∘ inl))) ∙ - ( associative-add-Semiring R _ _ _) +split-sum-Semiring R = + split-mul-fin-Commutative-Monoid (additive-commutative-monoid-Semiring R) +``` + +### Permutations preserve sums + +```agda +module _ + {l : Level} (R : Semiring l) + where + + preserves-sum-permutation-Semiring : + (n : ℕ) → (σ : Permutation n) → + (f : functional-vec-Semiring R n) → + sum-Semiring R n f ＝ sum-Semiring R n (f ∘ map-equiv σ) + preserves-sum-permutation-Semiring = + preserves-product-permutation-Commutative-Monoid + ( additive-commutative-monoid-Semiring R) +``` + +### Sums over finite types are preserved by equivalences + +```agda +module _ + {l1 l2 l3 : Level} (R : Semiring l1) (A : Finite-Type l2) (B : Finite-Type l3) + (H : equiv-Finite-Type A B) + where + + sum-equiv-finite-Semiring : + (f : type-Finite-Type A → type-Semiring R) → + sum-finite-Semiring R A f ＝ sum-finite-Semiring R B (f ∘ map-inv-equiv H) + sum-equiv-finite-Semiring = + mul-equiv-finite-Commutative-Monoid + ( additive-commutative-monoid-Semiring R) + ( A) + ( B) + ( H) +``` + +### Sums over finite types distribute over coproducts + +```agda +module _ + {l1 l2 l3 : Level} (R : Semiring l1) (A : Finite-Type l2) (B : Finite-Type l3) + where + + sum-coproduct-finite-Semiring : + (f : + type-Finite-Type A + type-Finite-Type B → type-Semiring R) → + sum-finite-Semiring R (coproduct-Finite-Type A B) f ＝ + add-Semiring + ( R) + ( sum-finite-Semiring R A (f ∘ inl)) + ( sum-finite-Semiring R B (f ∘ inr)) + sum-coproduct-finite-Semiring = + mul-coproduct-finite-Commutative-Monoid + ( additive-commutative-monoid-Semiring R) + ( A) + ( B) +``` + +### Sums distribute over dependent pair types + +```agda +module _ + {l1 l2 l3 : Level} (R : Semiring l1) + (A : Finite-Type l2) (B : type-Finite-Type A → Finite-Type l3) + where + + sum-Σ-finite-Semiring : + (f : (a : type-Finite-Type A) → type-Finite-Type (B a) → type-Semiring R) → + sum-finite-Semiring R (Σ-Finite-Type A B) (ind-Σ f) ＝ + sum-finite-Semiring R A (λ a → sum-finite-Semiring R (B a) (f a)) + sum-Σ-finite-Semiring = + mul-Σ-finite-Commutative-Monoid (additive-commutative-monoid-Semiring R) A B +``` + +### The sum over an empty type is zero + +```agda +module _ + {l1 l2 : Level} (R : Semiring l1) (A : Finite-Type l2) + (H : is-empty (type-Finite-Type A)) + where + + sum-is-empty-finite-Semiring : + (f : type-Finite-Type A → type-Semiring R) → + is-zero-Semiring R (sum-finite-Semiring R A f) + sum-is-empty-finite-Semiring = + mul-is-empty-finite-Commutative-Monoid + ( additive-commutative-monoid-Semiring R) + ( A) + ( H) +``` + +### The sum over a finite type is the sum over any count for that type + +```agda +sum-finite-count-Semiring : + {l1 l2 : Level} (R : Semiring l1) (A : Finite-Type l2) + (cA : count (type-Finite-Type A)) + (f : type-Finite-Type A → type-Semiring R) → + sum-finite-Semiring R A f ＝ + sum-count-Semiring R (type-Finite-Type A) cA f +sum-finite-count-Semiring R = + mul-finite-count-Commutative-Monoid (additive-commutative-monoid-Semiring R) ``` diff --git a/src/univalent-combinatorics/coproduct-types.lagda.md b/src/univalent-combinatorics/coproduct-types.lagda.md index 87603eab3b..ee2c6015ff 100644 --- a/src/univalent-combinatorics/coproduct-types.lagda.md +++ b/src/univalent-combinatorics/coproduct-types.lagda.md @@ -145,6 +145,52 @@ abstract number-of-elements-count-coproduct (pair k e) (pair l f) = refl ``` +### Mapping the `count-coproduct` equivalence on `inl-coproduct-Fin` is `inl` on the left count + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} (cA : count A) (cB : count B) + where + + map-equiv-count-coproduct-inl-coproduct-Fin : + map-equiv-count (count-coproduct cA cB) ∘ + inl-coproduct-Fin + ( number-of-elements-count cA) + ( number-of-elements-count cB) ~ + inl ∘ map-equiv-count cA + map-equiv-count-coproduct-inl-coproduct-Fin a = + ap + ( map-coproduct _ _) + ( is-retraction-map-inv-equiv + ( compute-coproduct-Fin + ( number-of-elements-count cA) + ( number-of-elements-count cB)) + ( inl a)) +``` + +### Mapping the `count-coproduct` equivalence on `inr-coproduct-Fin` is `inr` on the right count + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} (cA : count A) (cB : count B) + where + + map-equiv-count-coproduct-inr-coproduct-Fin : + map-equiv-count (count-coproduct cA cB) ∘ + inr-coproduct-Fin + ( number-of-elements-count cA) + ( number-of-elements-count cB) ~ + inr ∘ map-equiv-count cB + map-equiv-count-coproduct-inr-coproduct-Fin b = + ap + ( map-coproduct _ _) + ( is-retraction-map-inv-equiv + ( compute-coproduct-Fin + ( number-of-elements-count cA) + ( number-of-elements-count cB)) + ( inr b)) +``` + ### If both `Σ A P` and `Σ A Q` have a count, then `Σ A P + Q` have a count ```agda diff --git a/src/univalent-combinatorics/standard-finite-types.lagda.md b/src/univalent-combinatorics/standard-finite-types.lagda.md index 31d90d106c..ef02fb64b0 100644 --- a/src/univalent-combinatorics/standard-finite-types.lagda.md +++ b/src/univalent-combinatorics/standard-finite-types.lagda.md @@ -20,7 +20,9 @@ open import foundation.decidable-types open import foundation.dependent-pair-types open import foundation.embeddings open import foundation.empty-types +open import foundation.equality-cartesian-product-types open import foundation.equality-coproduct-types +open import foundation.equality-dependent-pair-types open import foundation.equivalence-injective-type-families open import foundation.equivalences open import foundation.equivalences-maybe @@ -32,8 +34,10 @@ open import foundation.negated-equality open import foundation.negation open import foundation.noncontractible-types open import foundation.preunivalent-type-families +open import foundation.propositions open import foundation.raising-universe-levels open import foundation.retractions +open import foundation.sections open import foundation.sets open import foundation.transport-along-identifications open import foundation.unit-type @@ -228,7 +232,7 @@ nat-Fin (succ-ℕ k) (inl x) = nat-Fin k x nat-Fin (succ-ℕ k) (inr x) = k nat-Fin-reverse : (k : ℕ) → Fin k → ℕ -nat-Fin-reverse (succ-ℕ k) (inl x) = succ-ℕ (nat-Fin k x) +nat-Fin-reverse (succ-ℕ k) (inl x) = succ-ℕ (nat-Fin-reverse k x) nat-Fin-reverse (succ-ℕ k) (inr x) = 0 strict-upper-bound-nat-Fin : (k : ℕ) (x : Fin k) → le-ℕ (nat-Fin k x) k @@ -491,3 +495,39 @@ is-preunivalent-Fin : is-preunivalent Fin is-preunivalent-Fin = is-preunivalent-retraction-equiv-tr-Set Fin-Set retraction-equiv-tr-Fin ``` + +### `Fin n` is equivalent to the set of natural numbers less than `n` + +```agda +nat-le-Fin-reverse : (n : ℕ) (k : Fin n) → Σ ℕ (λ m → le-ℕ m n) +nat-le-Fin-reverse (succ-ℕ n) (inr star) = zero-ℕ , star +nat-le-Fin-reverse (succ-ℕ n) (inl k) = + ind-Σ (λ m m