has_continuous_mul extends has_mul?

Stream: general

[Bernd Losert]

How come has_continuous_mul does not extend has_mul?

[Kevin Buzzard]

docs#has_continuous_mul

[Kevin Buzzard]

it does?

[Kevin Buzzard]

I mean, it doesn't extend it, but it asks for has_mul M which is the same thing modulo technical details about maps between classes

[Adam Topaz]

Search zulip for the word mixin for more about this design choice.

[Eric Wieser]

class has_continuous_mul extends has_mul X would mean "if you write has_continuous_mul X, you get a new multiplication on X". This means if you write [ring X] [has_continuous_mul X] you just got two different multiplication operators, which is unlikely what you wanted to express.

[Eric Wieser]

class has_continuous_mul [has_mul X] means "you can't use has_continuous_mul X unless you have a multiplication already".

[Bernd Losert]

Ah, I see.

[Bernd Losert]

I am having trouble getting the following to work:

import tactic
import order.filter.partial
import algebra.support

noncomputable theory
open set filter classical
open_locale classical filter

variables {X Y : Type*}

structure convergence_space (X : Type*) :=
(converges : filter X → X → Prop)

attribute [class] convergence_space

open convergence_space

instance [p : convergence_space X] [q : convergence_space Y] : convergence_space (X × Y) := sorry
instance [p : convergence_space X] : convergence_space (option X) := sorry

structure continuous [p : convergence_space X] [q : convergence_space Y] (f : X → Y) : Prop :=
(filter_converges : ∀ {x} {ℱ}, p.converges ℱ x → q.converges (map f ℱ) (f x))

class has_continuous_mul (X : Type*) [convergence_space X] [has_mul X] : Prop :=
(continuous_mul : continuous (λ p : X × X, p.1 * p.2))

class has_continuous_smul (S X : Type*) [has_scalar S X] [convergence_space S] [convergence_space X] : Prop :=
(continuous_smul : continuous (λ p : S × X, p.1 • p.2))

class convergence_group (G : Type*) [convergence_space G] [group G] extends has_continuous_mul G : Prop :=
(continuous_inv : continuous (has_inv.inv : G → G))

class partial_group_action (G X : Type*) [group G] :=
(α : G × option X -> option X)

open partial_group_action

class continuous_partial_group_action (G X : Type*) [convergence_group G] [partial_group_action G X] [convergence_space X] :=
(continuity : continuous α) -- COMPLAINS that it can't find instance of convergence_space G

[Adam Topaz]

That's precisely because your convergence_group is a mixin.....

[Adam Topaz]

import tactic
import order.filter.partial
import algebra.support

noncomputable theory
open set filter classical
open_locale classical filter

variables {X Y : Type*}

structure convergence_space (X : Type*) :=
(converges : filter X → X → Prop)

attribute [class] convergence_space

open convergence_space

instance [p : convergence_space X] [q : convergence_space Y] : convergence_space (X × Y) := sorry
instance [p : convergence_space X] : convergence_space (option X) := sorry

structure continuous [p : convergence_space X] [q : convergence_space Y] (f : X → Y) : Prop :=
(filter_converges : ∀ {x} {ℱ}, p.converges ℱ x → q.converges (map f ℱ) (f x))

class has_continuous_mul (X : Type*) [convergence_space X] [has_mul X] : Prop :=
(continuous_mul : continuous (λ p : X × X, p.1 * p.2))

class has_continuous_smul (S X : Type*) [has_scalar S X] [convergence_space S] [convergence_space X] : Prop :=
(continuous_smul : continuous (λ p : S × X, p.1 • p.2))

class convergence_group (G : Type*) [convergence_space G] [group G] extends has_continuous_mul G : Prop :=
(continuous_inv : continuous (has_inv.inv : G → G))

class partial_group_action (G X : Type*) [group G] :=
(α : G × option X -> option X)

open partial_group_action

class continuous_partial_group_action (G X : Type*) [convergence_space G] [group G]
  [convergence_group G] [partial_group_action G X] [convergence_space X] :=
(continuity : continuous (partial_group_action.α : G × _ → option X)) -- COMPLAINS that it can't find instance of convergence_space G

[Adam Topaz]

You should also fix your partial_group_action class, so that you can actually use \alpha instead of giving the type signature..

[Bernd Losert]

So you're saying that I should NOT make convergence_group a mixin? I was copying what topological_group does.

[Adam Topaz]

No, I'm saying that you were missing some assumptions

[Adam Topaz]

BTW, why are you defining a partial_group_action class? Can't you just use mul_action G (option X)?

[Bernd Losert]

Ah, so those assumptions are not "brought into scope" from using convergence_group G?

[Adam Topaz]

Exactly, this is the main distinction when compared with class ..... extends ...

[Adam Topaz]

Like Eric said above, if you want to have a ring with a continuous multiplication, you would need to write [ring A] [has_continuous_mul A].

[Bernd Losert]

Adam Topaz said:

BTW, why are you defining a partial_group_action class? Can't you just use mul_action G (option X)?

I still need the class for extra properties not shown in the toy code here. I guess I could extend it?

[Adam Topaz]

If [has_continuous_mul A] gave you a has_mul instance, then you would have two competing multiplciations, one from the continuous mul and one from the ring, and that's not what you want.

[Bernd Losert]

Yep.

[Adam Topaz]

Isn't a partial group action just an action of G on option X, or is that not what you are claiming?

[Bernd Losert]

Well, there's more to it. For example, forall g, alpha(g, nothing) = nothing.

[Adam Topaz]

oh right..

[Bernd Losert]

Thanks again.

[Adam Topaz]

hmm... maybe there is a way to avoid making a new definition for this...

[Adam Topaz]

Do we have a typeclass for a multiplicative action on a pointed type which respects the distinguished point @Eric Wieser ?

[Bernd Losert]

Adam Topaz said:

You should also fix your partial_group_action class, so that you can actually use \alpha instead of giving the type signature..

Why does this cause problems?

[Adam Topaz]

It doesn't cause problems per se, but why should you make a new definition with all the associated API if you can just use something off the shelf?

[Bernd Losert]

No, I meant this fix:

(continuity : continuous (partial_group_action.α : G × _ → option X))

[Adam Topaz]

Oh I see....

[Bernd Losert]

Why can't I just write continuous alpha?

[Yaël Dillies]

Adam Topaz said:

Do we have a typeclass for a multiplicative action on a pointed type which respects the distinguished point Eric Wieser ?

Sounds like (half of) a monoid_with_zero_action, if that exists?

[Adam Topaz]

Again, this is because you're using the field from a class -- we had a similar discussion about your convergence_space.converges, remember?

[Bernd Losert]

Yeah, but I made it a class, not a structure.

[Yaël Dillies]

A class is a structure!

[Bernd Losert]

True, but there's a difference between making a structure and then adding the class attribute to it and just using class.

[Yaël Dillies]

I think the only difference is the implicitness of field arguments.

[Bernd Losert]

If I use [act : partial_group_action G X] and then write act.α, it works.

[Bernd Losert]

It's as if Lean can't figure out where alpha is coming from.

[Adam Topaz]

But this is the same issue as writing p.converges for [p : convergence_space X].

[Adam Topaz]

Again, this is like writing g.to_has_mul.mul x y instead of x * y when [g : group G].

[Yaël Dillies]

To your discharge, understanding how to pass around arguments idiomatically is pretty hard. Welcome to the steep learning curve :wink:

[Bernd Losert]

Well, there seems to be some confusion on my part as to when instance arguments require something to the left of : and when not.

[Yaël Dillies]

They should almost never. But I think you're hitting the "almost" with your instances on your structures.

[Eric Wieser]

Adam Topaz said:

Do we have a typeclass for a multiplicative action on a pointed type which respects the distinguished point Eric Wieser ?

I'm afraid I can't decode this meaningully!

[Adam Topaz]

If M is a monoid and X is a pointed type with distinguished point * : X, (which might be called 0 ;)), do we have a typeclass for an action of M on X such that m \bu * = * for all m?

[Bernd Losert]

Yaël Dillies said:

They should almost never. But I think you're hitting the "almost" with your instances on your structures.

So you're saying that the confusion Lean has regarding continuous α has to do with the fact that I defined convergence_space as a structure with a class attribute afterwards?

[Yaël Dillies]

Probably, we can restrict to X := option α or with_zero α for now.

[Yaël Dillies]

No, I meant that you're doing the rare bit of the API where you need to dig the structures ugly.

[Eric Wieser]

So a typeclass with only docs#smul_zero / docs#smul_zero'?

[Adam Topaz]

yeah

[Eric Wieser]

The fact that I have two links for the same statement there indicates we do not have that generalization

[Eric Wieser]

Either you also need to assume docs#zero_smul or docs#smul_add alongside smul_zero

[Adam Topaz]

Ah, so you could take a docs#smul_with_zero of with_zero M on X

[Bernd Losert]

Consider this code:

import tactic
import order.filter.partial
import algebra.support

noncomputable theory
open set filter classical
open_locale classical filter

variables {X Y : Type*}

class partial_group_action (G X : Type*) [group G] :=
(α : G × option X -> option X)

open partial_group_action

def foo {G X : Type*} [group G] [partial_group_action G X] (g : G) (x : X) : X :=
α (g, x)

I'm not doing anything fancy here, yet it still complains.

[Bernd Losert]

Oops. Nevermind.

[Bernd Losert]

Forgot the option part. But that works without a problem regarding α.

[Adam Topaz]

import tactic
import order.filter.partial
import algebra.support

noncomputable theory
open set filter classical
open_locale classical filter

variables {X Y : Type*}

class partial_group_action (G X : Type*) [group G] :=
(α : G × option X -> option X)

open partial_group_action

def foo {G X : Type*} [group G] [partial_group_action G X] (g : G) (x : X) : option X :=
α (g, some x)

[Bernd Losert]

Yep. And I didn't have to qualify where alpha came from in this example.

[Adam Topaz]

Ok

[Adam Topaz]

That's because you gave it an input of (g, some x), so lean then knows that it's supposed to look for an $\alpha$ which takes an input of type G \x option X, and it is then able to find the typclass instance.

[Bernd Losert]

So you're saying if I just use a naked alpha (i.e. with no arguments), it can't figure out which instance to use?

[Adam Topaz]

Yeah, exactly.

[Adam Topaz]

Because there could a priori be partial_group_actions for many different types.

[Bernd Losert]

I see. I guess I was hoping it would use the "obvious to me" one.

[Adam Topaz]

It's like writing (*). This is the function has_mul.mul, but lean has no way of knowing what type this multiplciation is defined on withyout further hints.

[Bernd Losert]

That settles that matter. Thanks a bunch.

[Adam Topaz]

No worries. Typeclasses take some time to get used to.

[Bernd Losert]

I'm used to type classes in Haskell and Agda. Lean seems to have more gotchas than I expected.