Semisimple commutative finite rings
Content created by Egbert Rijke, Fredrik Bakke and Victor Blanchi.
Created on 2023-05-25.
Last modified on 2023-06-10.
module finite-algebra.semisimple-commutative-finite-rings where
Imports
open import elementary-number-theory.natural-numbers open import finite-algebra.commutative-finite-rings open import finite-algebra.dependent-products-commutative-finite-rings open import finite-algebra.finite-fields open import finite-algebra.homomorphisms-commutative-finite-rings open import foundation.dependent-pair-types open import foundation.existential-quantification open import foundation.function-types open import foundation.propositional-truncations open import foundation.universe-levels open import univalent-combinatorics.finite-types open import univalent-combinatorics.standard-finite-types
Idea
A semisimple commutative finite rings is a commutative finie rings wich is merely equivalent to an iterated cartesian product of finite fields.
Definitions
Semisimple commutative finite rings
is-semisimple-Commutative-Ring-𝔽 : {l1 : Level} (l2 : Level) → Commutative-Ring-𝔽 l1 → UU (l1 ⊔ lsuc l2) is-semisimple-Commutative-Ring-𝔽 l2 R = exists ( ℕ) ( λ n → exists-Prop ( Fin n → Field-𝔽 l2) ( λ A → trunc-Prop ( type-hom-Commutative-Ring-𝔽 ( R) ( Π-Commutative-Ring-𝔽 ( Fin n , is-finite-Fin n) ( commutative-finite-ring-Field-𝔽 ∘ A))))) Semisimple-Commutative-Ring-𝔽 : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2) Semisimple-Commutative-Ring-𝔽 l1 l2 = Σ (Commutative-Ring-𝔽 l1) (is-semisimple-Commutative-Ring-𝔽 l2) module _ {l1 l2 : Level} (A : Semisimple-Commutative-Ring-𝔽 l1 l2) where commutative-finite-ring-Semisimple-Commutative-Ring-𝔽 : Commutative-Ring-𝔽 l1 commutative-finite-ring-Semisimple-Commutative-Ring-𝔽 = pr1 A
Properties
The number of ways to equip a finite type with a structure of semisimple commutative finite ring is finite
module _ {l1 : Level} (l2 : Level) (X : 𝔽 l1) where structure-semisimple-commutative-ring-𝔽 : UU (l1 ⊔ lsuc l2) structure-semisimple-commutative-ring-𝔽 = Σ ( structure-commutative-ring-𝔽 X) ( λ r → is-semisimple-Commutative-Ring-𝔽 ( l2) ( compute-structure-commutative-ring-𝔽 X r)) compute-structure-semisimple-commutative-ring-𝔽 : structure-semisimple-commutative-ring-𝔽 → Semisimple-Commutative-Ring-𝔽 l1 l2 pr1 (compute-structure-semisimple-commutative-ring-𝔽 (p , s)) = compute-structure-commutative-ring-𝔽 X p pr2 (compute-structure-semisimple-commutative-ring-𝔽 (p , s)) = s -- is-finite-structure-semisimple-commutative-ring-𝔽 : -- is-finite structure-semisimple-commutative-ring-𝔽 -- is-finite-structure-semisimple-commutative-ring-𝔽 = -- is-finite-Σ -- ( is-finite-structure-commutative-ring-𝔽 X) -- ( λ c → {!!})
Recent changes
- 2023-06-10. Egbert Rijke. cleaning up transport and dependent identifications files (#650).
- 2023-06-09. Fredrik Bakke. Remove unused imports (#648).
- 2023-05-25. Victor Blanchi and Egbert Rijke. Towards Hasse-Weil species (#631).