From: AARON CRIGHTON <crightoa@mcmaster.ca>

Hello Everyone,

I have been working on a project in HOL-Algebra and have encountered an

issue with a certain kind of construction I'd like to perform. I would like

to prove some lemmas and perform constructions involving ring

localizations. I understand that there is an AFP submission which

constructs the localization of a ring at a multiplicative subset, but I was

hoping I could formulate an abstract locale for a ring R and a localization

of that ring in terms of the universal property of localizations. This

would be desirable because in many cases the localization of a ring can

arise in ways other than the canonical construction (such as when one is

already working with a local ring). In my case, I would like to be able to

view localizations of the integers as subrings of the field of rational

numbers. My first attempt at this definition was:

locale abstract_localization = ring_hom_cring R S h +

mult_submonoid_of_crng R D for

R and S and h and D

- assumes localization_universal_property:

"⋀T ψ. ⟦ cring T; ψ ∈ ring_hom R T; ψ ` D ⊆ Units T⟧ ⟹

(∃! φ. φ ∈ ring_hom R S ∩ extensional (carrier R) ∧

(∀ a ∈ carrier R. φ (h a) = ψ a)) "

This definition does not work, however, because the locale fixes a type for

the elements of the ring T in the axiom, and so the axiom only applies to

rings of this type. Of course this means that there will be many instances

of this locale satisfied by rings S which are not the localization of R.

One workaround for this that I have considered would be to replace my axiom

with the assertion that my ring is isomorphic to the concrete construction

of the localization from the AFP, and then prove a lemma which states that

the universal property above is necessary and sufficient for verifying an

instance of this locale.

I was wondering if anyone might have any thoughts on a general way to do

this kind of construction, or if there are reasons why this construction is

suboptimal in HOL-Algebra.

Thanks for your consideration,

Aaron

Last updated: Jan 25 2022 at 02:35 UTC