Homomorphisms of ring extensions of the rational numbers

Content created by Garrett Figueroa and malarbol.

Created on 2025-08-11.
Last modified on 2025-08-11.

{-# OPTIONS --lossy-unification #-}

module ring-theory.homomorphisms-ring-extensions-rational-numbers where
Imports 
open import foundation.universe-levels

open import ring-theory.homomorphisms-rings
open import ring-theory.ring-extensions-rational-numbers

Idea

Homomorphisms of rational extensions of ℚ are homomorphisms between their underlying rings.

Definitions

Homorphisms of ring extensions of ℚ

module _
  {l1 l2 : Level}
  (A : Rational-Extension-Ring l1)
  (B : Rational-Extension-Ring l2)
  where

  hom-Rational-Extension-Ring : UU (l1 ⊔ l2)
  hom-Rational-Extension-Ring =
    hom-Ring
      ( ring-Rational-Extension-Ring A)
      ( ring-Rational-Extension-Ring B)

  map-hom-Rational-Extension-Ring :
    hom-Rational-Extension-Ring →
    type-Rational-Extension-Ring A →
    type-Rational-Extension-Ring B
  map-hom-Rational-Extension-Ring =
    map-hom-Ring
      ( ring-Rational-Extension-Ring A)
      ( ring-Rational-Extension-Ring B)

Recent changes