Definition of Absorbs

Stream: maths

[Yury G. Kudryashov]

What do you think about redefining docs#Absorbs as below? It is equivalent to the existing definition for an action of a (semi)normed ring on a module but doesn't need norm, metric etc.

def Absorbs (M : Type*) {α : Type*} [Bornology M] [SMul M α] (A B : Set α) : Prop :=
  ∀ᶠ a in cobounded M, B ⊆ a • A

[Yury G. Kudryashov]

@Jean Lo, you wrote the current definition in !3#4827, what do you think about :up:?

[Yury G. Kudryashov]

@Bhavik Mehta and @Yaël Dillies you're also mentioned as the authors of file#Mathlib/Analysis/LocallyConvex/Basic
what do you think about :up:?

[Jireh Loreaux]

Makes sense to me, but I know you didn't ask me :wink:

[Yury G. Kudryashov]

I tagged the authors of that file...

[Yaël Dillies]

I think that's much slicker than the current definition. And you get to move it out of that file (I would personally move it to Topology.Bornology.Pointwise). I'm sold.

[Yury G. Kudryashov]

I'm moving it to Topology.Bornology.Absorbs

[Yury G. Kudryashov]

And I'm going to add typeclasses for properties like -(cobounded X) = cobounded X and (cobounded G)⁻¹ = 𝓝[≠] 0

[Yury G. Kudryashov]

/me is away for a few hours

[Yaël Dillies]

If you're going to do that, then I'd suggest putting it all in a single file Topology.Bornology.Pointwise.

[Patrick Massot]

We should also asks @Anatole Dedecker.

[Yury G. Kudryashov]

Yaël Dillies said:

If you're going to do that, then I'd suggest putting it all in a single file Topology.Bornology.Pointwise.

Some of these definitions need topology, some don't. I was going to put them into different files.

[Yaël Dillies]

Hmm... good point. I'll wait to see the PRs to complain. :stuck_out_tongue:

[Yury G. Kudryashov]

#8856 is a dependency