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