Local rings
Content created by Jonathan Prieto-Cubides, Fredrik Bakke, Egbert Rijke and Gregor Perčič.
Created on 2022-05-27.
Last modified on 2023-09-21.
module ring-theory.local-rings where
Imports
open import foundation.dependent-pair-types open import foundation.disjunction open import foundation.propositions open import foundation.sets open import foundation.universe-levels open import ring-theory.invertible-elements-rings open import ring-theory.rings
Idea
A local ring is a ring such that whenever a sum of elements is invertible, then one of its summands is invertible. This implies that the non-invertible elements form an ideal. However, the law of excluded middle is needed to show that any ring of which the non-invertible elements form an ideal is a local ring.
Definition
is-local-prop-Ring : {l : Level} (R : Ring l) → Prop l is-local-prop-Ring R = Π-Prop ( type-Ring R) ( λ a → Π-Prop ( type-Ring R) ( λ b → function-Prop ( is-invertible-element-Ring R (add-Ring R a b)) ( disj-Prop ( is-invertible-element-prop-Ring R a) ( is-invertible-element-prop-Ring R b)))) is-local-Ring : {l : Level} → Ring l → UU l is-local-Ring R = type-Prop (is-local-prop-Ring R) is-prop-is-local-Ring : {l : Level} (R : Ring l) → is-prop (is-local-Ring R) is-prop-is-local-Ring R = is-prop-type-Prop (is-local-prop-Ring R) Local-Ring : (l : Level) → UU (lsuc l) Local-Ring l = Σ (Ring l) is-local-Ring module _ {l : Level} (R : Local-Ring l) where ring-Local-Ring : Ring l ring-Local-Ring = pr1 R set-Local-Ring : Set l set-Local-Ring = set-Ring ring-Local-Ring type-Local-Ring : UU l type-Local-Ring = type-Ring ring-Local-Ring is-local-ring-Local-Ring : is-local-Ring ring-Local-Ring is-local-ring-Local-Ring = pr2 R
Recent changes
- 2023-09-21. Egbert Rijke and Gregor Perčič. The classification of cyclic rings (#757).
- 2023-03-14. Fredrik Bakke. Remove all unused imports (#502).
- 2023-03-13. Jonathan Prieto-Cubides. More maintenance (#506).
- 2023-03-10. Fredrik Bakke. Additions to
fix-import
(#497). - 2023-03-09. Jonathan Prieto-Cubides. Add hooks (#495).