Zulip Chat Archive

Stream: Is there code for X?

Topic: rational functions


view this post on Zulip Hunter Monroe (Apr 12 2021 at 18:27):

Is there code for rational functions? It appears on the page for missing undergrad math and is not in the PR list or issues. I would like to add code for rational functions--any reactions? For the definition, what would be a good name , e.g., ratfunc? What should this code cover? I suggest: identifying domain and range of rational functions, definition of horizontal, vertical, and slant asymptotes using limits, formula for asymptotes.

view this post on Zulip Yury G. Kudryashov (Apr 12 2021 at 18:35):

Probably you should start with purely algebraic definition (e.g., as the field of fractions of polynomial R).

view this post on Zulip Yury G. Kudryashov (Apr 12 2021 at 18:36):

Once this is merged, you can prove something about limits etc.

view this post on Zulip Damiano Testa (Apr 12 2021 at 18:57):

There is something about localizations in the file ring_theory/localization. In particular, I think that it defines a localization of an integral domain at the multiplicative submonoid of all the non-zero elements as fraction_map R K. I hope that this could be a beginning!

view this post on Zulip Hunter Monroe (Apr 13 2021 at 04:48):

OK, for full generality, given a field F, and polynomials over elements of F which form a ring R, we define polynomial_fraction_ring , as "fraction_ring R" with Type u_4. And then a rational function would be any element of that. This would be a new definition in ring_theory.localization. Is that roughly what you are suggesting?

view this post on Zulip Johan Commelin (Apr 13 2021 at 05:14):

I would call it rational_functions F.

view this post on Zulip Johan Commelin (Apr 13 2021 at 05:14):

And it doesn't have to be defined that way. You can also define it in a hands-on manner. But it will be important that you provide localization (polynomial F) (rational_function F).

view this post on Zulip Johan Commelin (Apr 13 2021 at 05:15):

Because once you have done that, you can start treating it as a localization, which unlocks a nice library for you.

view this post on Zulip Hunter Monroe (Apr 13 2021 at 05:23):

Johan Commelin said:

Because once you have done that, you can start treating it as a localization, which unlocks a nice library for you.

OK makes sense Johan, thanks

view this post on Zulip Hunter Monroe (Apr 17 2021 at 14:43):

(deleted)

view this post on Zulip Hunter Monroe (Apr 17 2021 at 14:44):

@Johan Commelin am I heading in the right direction and what is needed for the last line?

import data.polynomial.basic
import ring_theory.localization
universes u
variables {R : Type u}
namespace polynomial
variable [comm_ring R]
variables {p : polynomial R}
def rational_functions : fraction_ring p
end polynomial

view this post on Zulip Adam Topaz (Apr 17 2021 at 14:51):

@Hunter Monroe #backticks

view this post on Zulip Eric Wieser (Apr 17 2021 at 14:54):

The syntax is def name : type := value, your def is missing the :=

view this post on Zulip Eric Wieser (Apr 17 2021 at 14:55):

Does docs#fraction_ring exist?

view this post on Zulip Adam Topaz (Apr 17 2021 at 14:55):

Yes, but note that it takes a ring as an input, not a polynomial.

view this post on Zulip Adam Topaz (Apr 17 2021 at 14:56):

You probably want something of the following form:

import data.polynomial.basic
import ring_theory.localization

variables (k : Type*) [field k]

def rational_function_field_in_one_variable :=
  fraction_ring (polynomial k)

(and probably a better name than I came up with :smile: )

view this post on Zulip Eric Wieser (Apr 17 2021 at 20:28):

(deleted)


Last updated: May 16 2021 at 05:21 UTC