Stream: Mirror: Isabelle Users Mailing List

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


view this post on Zulip Email Gateway (Mar 22 2021 at 06:11):

From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>
Dear Aaron Crighton/All,

I would like to offer several comments with regard to your query. However,
please do not treat this as an official reply, as I am merely an
independent user of Isabelle, and I am not affiliated with the
developers/maintainers.

Firstly, the definition that you have chosen looks slightly odd. I believe
that a conventional form of the definition would be closer to the following
definition:

locale abstract_localization = ring_hom_cring R S h +
mult_submonoid_of_crng R D
for eT :: "'e itself" and R and S and h and D +
assumes localization_units: "h D ⊆ Units S" assumes localization_universal_property: "⋀(T::'e ring) ψ. ⟦ cring T; ψ ∈ ring_hom R T; ψ D ⊆ Units T⟧ ⟹
(
∃!φ::'c⇒'e.
φ ∈ ring_hom S T ∩ extensional (carrier S) ∧
(∀a ∈ carrier R. φ (h a) = ψ a)
)"

In this case, the type of T is still fixed, but the type variable
associated with the type of T is independent of the type variables
associated with the type of R.

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.

I believe that you may have exaggerated the problem, but I do not
have complete confidence in anything that is stated below.

When you provide an instantiation of abstract_localization, you provide a
lemma like

lemma (in eq_obj_rng_of_frac) eq_obj_rng_of_frac_abstract_localization:
fixes eT :: "'e itself"
shows "abstract_localization TYPE('e) R rec_rng_of_frac
rng_to_rng_of_frac S"
―‹Follows Theorem 4.5 in Thomas W. Hungerford's Algebra.›
sorry
(*I did sketch the proof for my own needs, and can provide it upon request,
but it is very rough*)

The lemma eq_obj_rng_of_frac_abstract_localization proves that the
constructions from the theory Localization in the AFP satisfy the universal
property, as defined above. Once the lemma is proven, it is possible to
instantiate it for any type variable 'e:

abstract_localization TYPE(?'e) R rec_rng_of_frac rng_to_rng_of_frac S

Thus, in a certain meta-sense, it does hold for rings with elements of
arbitrary types. Suppose, you have also proven abstract_localization_Q
below:

context eq_obj_rng_of_frac
begin

context
fixes Q :: "'c ring"
and t :: "'a ⇒ 'c"
begin

thm eq_obj_rng_of_frac_abstract_localization

lemma abstract_localization_Q:
fixes eT :: "'e itself" and fT :: "'f itself"
shows "abstract_localization TYPE('e) R Q t S"
sorry

end

I believe (but not entirely certain) that it should be possible to prove
that Q and rec_rng_of_frac are isomorphic by
instantiating abstract_localization_Q
and eq_obj_rng_of_frac_abstract_localization for suitable types via
instantiations like

interpret cd:
abstract_localization ‹TYPE('c)› R rec_rng_of_frac rng_to_rng_of_frac S
by (rule eq_obj_rng_of_frac_abstract_localization)
interpret Q_aa: abstract_localization ‹TYPE(('a × 'a) set)› R Q t S
by (rule abstract_localization_Q)
interpret Q_cc: abstract_localization ‹TYPE('c)› R Q t S
by (rule abstract_localization_Q)

Thence, the universal property should work as expected across types.
Nonetheless, I believe that it is not possible to state a single theorem in
the logic that captures this: one needs to instantiate
abstract_localization for every construction independently and then prove
the relevant theorems for the specific definitions (I believe that the
following post is relevant in this context:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2019-September/msg00097.html.
Still, some aspects of this problem can be automated in Isabelle/ML.
For example, see
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2020-July/msg00050.html,
where I showcase an attempt to develop a meta-category theory that could
work across types in HOL by using schematic polymorphism. However,
following this attempt, I arrived at the conclusion that "applied category
theory" can hardly be done in pure HOL conveniently (I would like to be
proven wrong though). Nonetheless, it can be done conveniently (to a point)
in ZFC in HOL, e.g. see
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2021-March/msg00022.html
(otherwise you may wish to look at other strong foundational systems
already implemented in Isabelle, e.g.
https://bitbucket.org/cezaryka/tyset/src,
https://github.com/jaycech3n/Isabelle-HoTT).

Kind Regards,
Mikhail Chekhov

On 15/03/2021 15:35:28 Aaron Crighton wrote:

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

view this post on Zulip Email Gateway (Mar 23 2021 at 19:43):

From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>
Dear All,

I noticed that I forgot to provide references for my previous post on the
mailing list and also that there is at least one case of the misuse of
terminology.

Thus, the sentence "I believe (but not entirely certain) that it should be
possible to prove that Q and rec_rng_of_frac are isomorphic by
instantiating abstract_localization_Q
and eq_obj_rng_of_frac_abstract_localization for suitable types via
instantiations like..." should read "I believe (but not entirely certain)
that it should be possible to prove that Q and rec_rng_of_frac are
isomorphic by instantiating abstract_localization_Q
and eq_obj_rng_of_frac_abstract_localization for suitable types via
interpretations like".

The missing references are
[1]. Hungerford TW. Algebra. New York: Springer; 2003.
[2]. Localization (commutative algebra) (Wikipedia) [Internet]. 2001.
Available from:
https://en.wikipedia.org/wiki/Localization_(commutative_algebra)

Kind Regards,
Mikhail Chekhov


Last updated: Sep 25 2021 at 10:20 UTC