How to deal with cyclic import for group.units fintype?

Stream: general

[Bolton Bailey]

I would like to make the instance instance [fintype α] : fintype (units α) in in algebra.group.units. But importing data.fintype.basic in algebra.group.basic` gives the following sequence of cyclic imports:

algebra.group.units
data.fintype.basic
group_theory.perm.basic
algebra.group.pi
algebra.group.hom_instances
algebra.group_power.basic
group_theory.group_action.defs
algebra.group.hom
algebra.group.commute
algebra.group.semiconj
algebra.group.units

My current idea for fixing this is to change the data.fintype.basic import of group_theory.perm.basic to an import of data.equiv.basic - my intuition is that we shouldn't need to talk about groups to define a fintype. This import change seems to break the section equiv portion of the file, but potentially the lemmas in this section can be moved to either data.equiv.basic or to a new data.fintype.perm file and files that need these lemmas can be rerouted to the new file.

Does this seem like a sound approach, or will it fall flat somehow?

For context, I am doing this because I would like to try to prove the Lucas theorem and as a first step I want to prove p.prime ↔ fintype.card (units (zmod p)) = (p-1) so I can start to talk about the order of the multiplicative group mod p. If there's another approach someone sees I'd be interested to hear it.

[Yakov Pechersky]

Why would you import that fintype in that file? algebra.group.units is much more basic than data.fintype. Why do you think that one need not talk about groups to define a fintype?

[Yakov Pechersky]

A fintype is based on the fact that there is some finset of the type and a proof that every term of the type is in that finset. Finsets are based on multisets. The theory of multisets utilizes canonically_ordered_add_monoid, which I'm pretty sure is later in the hierarchy than groups.

[Bolton Bailey]

Yakov Pechersky said:

algebra.group.units is much more basic than data.fintype. Why do you think that one need not talk about groups to define a fintype?

Well, I guess it's the case in lean that fintypes are based on finsets, which are based on multisets. This has always felt a little counterintuitive to me because in my conception of things, fintypes should be very basic indeed: It's just a type that is finite, how much more basic can you get? Maybe you could define fintypes using bijections to fin n or something.

Yakov Pechersky said:

Why would you import that fintype in that file?

As I said, I want to prove that the units of a fintype are a fintype. Anyway I realize now that this instance already exists in data.fintype.basic, so no need to change anything.

[Notification Bot]

Bolton Bailey has marked this topic as resolved.

[Mario Carneiro]

The algebra.group.units -> data.fintype.basic import sounds unnecessary, but so does data.fintype.basic -> group_theory.perm.basic

[Mario Carneiro]

you should not need groups to define finsets, but I would also agree that finsets are more complicated than groups

[Bolton Bailey]

I don't understand why people keep saying "finsets are more complicated than groups". Which did you learn about first as an undergrad, finite sets, or groups?

[Notification Bot]

Bolton Bailey has marked this topic as unresolved.

[Yakov Pechersky]

I think to claim that something is finite isn't so basic -- the claim that there are finite seeds that do not terminate in the collatz conjecture is very hard to prove.

[Bolton Bailey]

You could just as easily say that to claim something is a group isn't basic: Consider the binary operation on {0,1} which is equal to the xor operator if the Collatz conjecture is true and the and operator if the Collatz conjecture is false. The claim that this binary operation is a group is hard to prove.

[Yakov Pechersky]

Constructing that group is hard. The same way constructing the finite set of seeds is hard. fintype is a construction of the finite terms that define the type.

[Mario Carneiro]

Just because something is taught first doesn't mean it is more basic. Real numbers are taught in grade school but they are a lot more complicated than either finiteness or groups

[Mario Carneiro]

the definition of a group is very close to the axioms

[Ruben Van de Velde]

Btw, there's one direction of your first step here: https://leanprover-community.github.io/mathlib_docs/field_theory/finite/basic.html#zmod.card_units

[Bolton Bailey]

Mario Carneiro said:

the definition of a group is very close to the axioms

This is a fair point. I guess I think about "complexity" in terms of a mixture of things, which includes questions like "What is the size of the theory behind these objects?" as well as "How much Kolmogorov complexity does it take to define them?" and "How widespread is the use of this?". Perhaps as someone with a CS focus I just use finite sets more.

About the real numbers, I would say that while I might have learned about them in grade school, I never learned to construct them from more basic concepts until after I learned about groups or finite sets. So you are definitely right that they are more complex.

[Mario Carneiro]

The main one of those that matters for mathlib is "kolmogorov complexity", or more accurately the size of the existing definition + dependents (not other definitions that might be shorter). Mathlib does not always use the shortest possible definition of every object ab initio, because there is often aggregate savings by defining things in terms of other defined things

[Mario Carneiro]

for "What is the size of the theory behind these objects?" , it's more like the theory "ahead" of the objects; this is more or less unbounded for any individual definition

[Kevin Buzzard]

@Bolton Bailey it's because finset and fintype are constructive -- these constructive CS people have a totally different idea about what finiteness is

[Kevin Buzzard]

You're totally right that you can do finite types without groups, you just use set.finite (univ : set X)

[Mario Carneiro]

you can also define set.finite directly as an inductive type, which gets you a pretty short ab initio definition of finite type

[Kevin Buzzard]

I am a strong advocate for mathematicians using nonconstructive finiteness so we can find out how to make it better

[Mario Carneiro]

But for removing spurious dependencies, the most effective method is to separate the theorems from the definition

[Mario Carneiro]

because there are lots of theorems that are "topically" related to finset or fintype that can involve almost any part of maths and you don't want that all in the .basic file

[Kevin Buzzard]

docs#set.finite

[Bolton Bailey]

But wait, docs#set.finite tells me that it is defined using fintype. So to define fintypes that way would be circular.

[Kevin Buzzard]

I have bad internet but if that def uses fintype then it might need groups

[Mario Carneiro]

fintype doesn't need groups

[Mario Carneiro]

it does need multisets / lists though

[Mario Carneiro]

and it might have a spurious dependency on groups due to the .basic issue I mentioned

[Kevin Buzzard]

So we need set.finite2 defined recursively in a separate file and then this is imported by set.finite where it's proved that this is the same as finite :-)

[Bolton Bailey]

Mario Carneiro said:

fintype doesn't need groups

Don't you? I think I see the problem now with defining finset in terms of a bijection with fin n. You still need to talk about permutations to tell if two finsets are equal in that case, so you still end up wanting to import group theory and you gain nothing.

[Kevin Buzzard]

This import thing is not the concern of mathematicians anyway. The people actually building the library know what they're doing.

[Mario Carneiro]

Here's a definition of finite that uses nothing at all other than basic logic and inductive types

inductive is_finite {α} : (α → Prop) → Prop
| empty : is_finite (λ _, false)
| cons {p} (a : α) : is_finite p → is_finite (λ x, x = a ∨ p x)

def finite (α : Sort*) : Prop := is_finite (λ _ : α, true)

[Mario Carneiro]

that's not good enough to define fintype though since we want that to be computable data

[Yakov Pechersky]

Computable fintypes (and finsets) lets you do one of the most important things about finite things -- case bash. Telling the computer to prove something by checking every term of the thing.

[Mario Carneiro]

You can define docs#set.finite much the same way as is_finite here, you just use sets instead of predicates