WIP

agda · Sep 30, 2024 · 1cb7ca5 · 1cb7ca5
1 parent ed48931
commit 1cb7ca5
Showing 1 changed file with 25 additions and 0 deletions.
diff --git a/Cubical/Algebra/CommRing/Instances/Polynomials/Typevariate/CommQuotient.agda b/Cubical/Algebra/CommRing/Instances/Polynomials/Typevariate/CommQuotient.agda
@@ -0,0 +1,25 @@
+{-# OPTIONS --safe #-}
+{-
+ The goal of this module is to show that for a ring R, type I and ideal J there is an
+ isomorphism of algebras
+
+    (R/J)[I] ≃ R[I]/J
+
+-}
+module Cubical.Algebra.CommRing.Instances.Polynomials.Typevariate.CommQuotient where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Function using (_∘_; _$_)
+open import Cubical.Foundations.Structure using (⟨_⟩)
+
+open import Cubical.Data.Sum as ⊎
+open import Cubical.Data.Sigma
+
+open import Cubical.Algebra.CommRing
+open import Cubical.Algebra.CommRing.Quotient
+open import Cubical.Algebra.CommRing.Instances.Polynomials.Typevariate.Base
+open import Cubical.Algebra.CommRing.Instances.Polynomials.Typevariate.UniversalProperty
+
+private
+  variable
+    ℓ ℓ' : Level