Quantifying over classes

Stream: new members

[Raphael Appenzeller]

Let's say I have a property of two groups (in the example, that they are not equal). I then have a Lemma which should state that for a given group G there exists another group H such that the property is satisfied.

def my_property (G H : Type*)[group G][group H] := G ≠ H

lemma example_lemma (G : Type)[group G]
  : ∃ (H : Type) (prop : group H) , my_property G H   := by sorry

This gives me the following error that is a bit strange, as the expected type seems to be exactly the same as the provided one:

expected type:
G: Type
_inst_1: group G
H: Type
prop: group H
⊢ Prop

failed to synthesize type class instance for
G : Type,
_inst_1 : group G,
H : Type,
prop : group H
⊢ group H

The question is how to quantify over classes. Or maybe we are not supposed to do that with classes, but only with structures? But then how would I do that?

I notice that if I write G = H directly in the Lemma-statement, i don't get a mistake, but then probably only the types have to be equal, not the group structures.

[Eric Rodriguez]

usually the way to do this is by exactI, that is:

def my_property (G H : Type*)[group G][group H] := G ≠ H

lemma example_lemma (G : Type)[group G]
  : ∃ (H : Type) [group H] , by exactI my_property G H   := by sorry

it's not great :/ in lean4 this will be gone

[Eric Rodriguez]

(note that I changed to instance brackets in the lemma)

[Raphael Appenzeller]

Ok, thanks! How do I learn about things like these?

[Yaël Dillies]

By asking here :smile:

[Junyan Xu]

I don't think (group H) vs [group H] makes any difference?

[Eric Rodriguez]

I guess not, but it's probably better to state it in this way for binport/etc. What really is the difference overall apart from being able to skip names? Because this works, for example:

import algebra.group

def test (F) [monoid F] := (1 : F)

example {F} (h : monoid F) : test F = 1 := rfl

[Yaël Dillies]

It might have to do with triggering a typeclass search.

[Junyan Xu]

I think brackets inside existential quantifier never makes any difference; they only make difference in a function type whose terms can be applied to things, including forall propositions.

[Junyan Xu]

By the way G ≠ H doesn't mean the group stuctures are different/not isomorphic; it means the underlying types are not equal (which is an ill-behaved notion). If you have two [group G] instances then their equality is indeed equivalent to the group structures being equal, but we lack such extensionality lemmas for algebraic structures.

[Yaël Dillies]

Actually, we don't: docs#group.ext

[Junyan Xu]

Oh thanks! I think we are only missing them for more advanced structures, like field, algebra.

[Yaël Dillies]

This is from the time Bryan Gin-ge Chen was trying to prove the equivalence between boolean rings and boolean algebras. As it turns out, those extensionality lemmas are not really what we want. Instead, I did it using an equivalence of categories: docs#BoolRing_equiv_BoolAlg

[Yaël Dillies]

So yeah we don't have it for field simply because boolean rings are not fields!

[Junyan Xu]

If you have the leisure you may try to prove this is a partial order, though I don't really need it as preorder is enough to apply Zorn's lemma.

[Yaël Dillies]

Would that not be better expressed using subfield?

[Junyan Xu]

big k doesn't have a field structure. It's a type of cardinality large enough to properly contain all algebraic extensions of k.

[Reid Barton]

Yeah it's a bit weird: the carriers of the extensions under consideration are all subsets of a fixed set/type, but the field operations are not fixed (and the containment relation requires the operations to be preserved). When I came across this proof presented (a bit sketchily) in a textbook, I actually didn't believe it was correct for a while.

[Yaël Dillies]

Oh, that's pretty cursed indeed.

[Eric Rodriguez]

if big is in Type u, why can't you use Type u instead of some huge set?

[Eric Rodriguez]

is it about stating the compatibility conditions?

[Junyan Xu]

I explained why just above the definition of alg_extension in the link

[Junyan Xu]

In short: there is a large enough family of canonical maps between subsets of a type with all triangles commuting, but not between all types in a universe.

[Eric Rodriguez]

oh, that makes sense... I wonder if there is a purely type-theoretic way to resolve this, but I doubt it

[Junyan Xu]

I actually took that approach until I realized I can't take the direct limit ..