Email Gateway (Mar 15 2021 at 19:36): Email Gateway (Mar 15 2021 at 19:36):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
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: Jul 15 2022 at 23:21 UTC