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

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: Jul 15 2022 at 23:21 UTC