Zulip Chat Archive

Stream: new members

Topic: Forgetting type class structure on variables


Sebastian Monnet (Mar 31 2022 at 14:15):

Suppose I have defined a finite field extension L/KL/K, and now I want to use the same variable names for a result that doesn't require finiteness of the extension. Is there a way I can relax the assumption that L/KL/K is finite? Here's a very naive MWE where I fail to do this:

import field_theory.galois

variables (K L : Type*) [field K] [field L] [algebra K L] [finite_dimensional K L]

variables (L : Type*) [field L] [algebra K L]

Kevin Buzzard (Mar 31 2022 at 14:16):

Use sections?

import field_theory.galois

section fd_stuff

variables (K L : Type*) [field K] [field L] [algebra K L] [finite_dimensional K L]

end fd_stuff

section general_stuff

variables (K L : Type*) [field K] [field L] [algebra K L]

end general_stuff

Kevin Buzzard (Mar 31 2022 at 14:21):

Or even

import field_theory.galois

variables (K L : Type*) [field K] [field L] [algebra K L]

section fd_stuff

variable [finite_dimensional K L]

end fd_stuff

Sebastian Monnet (Mar 31 2022 at 14:33):

Okay, thanks!

Anne Baanen (Mar 31 2022 at 15:13):

Another approach is to name the variable and use include/omit:

import field_theory.galois

variables (K L : Type*) [field K] [field L] [algebra K L] [fd : finite_dimensional K L]

-- `fd` is not used implicitly

include fd

-- `fd` is used implicitly

omit fd

-- `fd` is not used implicitly

Note that named variables have slightly different behaviour: they are not automatically included.


Last updated: Dec 20 2023 at 11:08 UTC