## Stream: Mirror: Isabelle Users Mailing List

### Topic: [isabelle] Specifying a Universal Property in a locale de...

#### 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

• 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