Zulip Chat Archive

Stream: new members

Topic: extends keyword

Calle Sönne (Jan 29 2021 at 09:09):


I want to make an instance of a class which extends 3 other classes (and contains no other fields). Specifically this one:

class reflective (R : D  C) extends is_right_adjoint R, full R, faithful R.

I have proven that my functor is an instance of each of is_right_adjoint R, full R, faithful R..
Is there a way for me to prove this using the prior instances? Or should I just incorporate their proofs into this one?
When I use the "generate skeleton for fields" feature it also expands is_right_adjoint, full and faithful into their fields.

Eric Wieser (Jan 29 2021 at 09:15):

{ .. right_adjoint_proof, .. full_proof, ..faithful_proof }

Eric Wieser (Jan 29 2021 at 09:17):

Note that instance names are fully-qualified (protected), so the proof will typically be namespace.instance_name

Kevin Buzzard (Jan 29 2021 at 09:48):

It's nice to know such classes exist already in lean. Number fields are a class which extends three classes (field, Q-algebra, finite-dimensional) and I was concerned that people would argue that if I wanted a number field i should ask for those classes instead

Eric Wieser (Jan 29 2021 at 09:55):

An argument against this type of class is that you'll often assume it even though you actually just need one of its pieces -
a lot of lemmas about docs#integral_domain are actually just about docs#no_zero_divisors

Kevin Buzzard (Jan 29 2021 at 10:11):

An argument for them is that if you tell a number theorist that they have to write three lines of gobble-de-gook every time they want a number field, this is not going to go down well. You can just as well argue that we shouldn't have a ring class, we should just have mixin after mixin.

Kevin Buzzard (Jan 29 2021 at 10:12):

Structures central to mathematics should be there, whatever the computer scientists think of them.

Julian Külshammer (Jan 29 2021 at 20:25):

Hopefully by the time number field will be used in mathlib extensively, Alex' new linter will be ready and it will tell you if you assumed number field but only needed finite-dimensional.

Last updated: Dec 20 2023 at 11:08 UTC