Zulip Chat Archive

Stream: new members

Topic: Invalid Constructor


view this post on Zulip James Weaver (Dec 31 2019 at 14:16):

I'm having a bit of trouble with inductive type constructors. My code is as follows:

import algebra.ring
import data.equiv.algebra
import field_theory.subfield

set_option class.instance_max_depth 40

-- define fixes K k f for any f ∈ ring_aut K
def fixes {K : Type*} [discrete_field K] (k : set K) [is_subfield k] : (ring_aut K)  Prop
:= (λ f : ring_aut K, ( x : k, f.to_fun x = x))

-- define gal K k
def gal (K : Type*) [discrete_field K] (k : set K) [is_subfield k] := { α : (K +* K) // (fixes k α) }
instance {K : Type*} [discrete_field K] {k : set K} [is_subfield k] :has_coe (gal K k) (ring_aut K) := ⟨λ s, s.val

section gal

-- Let K/k be an extension of fields
variable {K : Type*}
variable [discrete_field K]
variable {k : set K}
variable [is_subfield k]

-- Show that id is in gal
def aut_one : ring_aut K :=  group.one (ring_aut K)
theorem aut_one_fixes_k : fixes k aut_one := begin rw [fixes], intro, refl end
def gal_one : gal K k :=  aut_one, aut_one_fixes_k 

-- define multiplication in the galois group
def aut_mul : ring_aut K  ring_aut K  ring_aut K := group.mul
theorem gal_closed_under_aut_mul (g h : gal K k) : fixes k (aut_mul g h) :=
begin
    intro x,
    change g.val.to_fun (h.val.to_fun x) = x,
    rw [h.property, g.property]
end
def gal_mul : gal K k  gal K k  gal K k :=
    λ g h : (gal K k),  aut_mul g h, gal_closed_under_aut_mul g h

-- show that the galois group is closed under inversion
def aut_inv : ring_aut K  ring_aut K := group.inv
theorem gal_closed_under_inversion (g : gal K k) : fixes k (aut_inv g.val) :=
begin
    intro x,
    apply g.val.to_equiv.injective,
    change g.val.to_fun (g.val.inv_fun x) = g.val.to_fun x,
    rw [g.val.right_inv, g.property],
end
def gal_inv : gal K k  gal K k := λ g : gal K k, aut_inv g.val, gal_closed_under_inversion g

-- show is assoc
theorem gal_mul_assoc :  (a b c : gal K k), gal_mul (gal_mul a b) c = gal_mul a (gal_mul b c) :=
begin
    intros a b c,
    split,
end

-- show gal_one is the left and right identity
theorem gal_one_mul :  (a : gal K k), gal_mul gal_one a = a :=
begin
    intro a,
    change  aut_mul aut_one a.val, gal_closed_under_aut_mul gal_one a  = a,
end

The last line produces an error, specifically it tells me:

invalid constructor ⟨...⟩, expected type is not an inductive type
  ?m_1

which isn't making much sense to me. As far as I can see the type gal K k really ought to be deducible, so it should be using the constructor for that type, which as a subtype is of the form ⟨a : ring_aut K, p : fixes k a⟩.

view this post on Zulip Kenny Lau (Dec 31 2019 at 14:16):

use ```lean to enable syntax highlighting

view this post on Zulip Kenny Lau (Dec 31 2019 at 14:17):

```lean
lorem ipsum
```

view this post on Zulip Kenny Lau (Dec 31 2019 at 14:18):

change that line to:

change ( aut_mul aut_one a.val, gal_closed_under_aut_mul gal_one a  : gal K k) = a,

view this post on Zulip Kenny Lau (Dec 31 2019 at 14:19):

Lean elaborates from left to right

view this post on Zulip Kenny Lau (Dec 31 2019 at 14:19):

so Lean sees the anonymous constructor before it sees a

view this post on Zulip Kenny Lau (Dec 31 2019 at 14:19):

and it tries to match the type of a to the type of the anonymous constructor (i.e. coerce RHS to LHS)

view this post on Zulip Kenny Lau (Dec 31 2019 at 14:19):

but Lean cannot figure out the type of the anonymous constructor

view this post on Zulip James Weaver (Dec 31 2019 at 14:23):

Thanks, that really helps!

view this post on Zulip Kevin Buzzard (Dec 31 2019 at 14:33):

One issue with doing Galois theory like this (with subfields) is that in practice you might end up with two fields E and F and an injective field map from E to F, and you'll have to dance around between E and the image of the map. This is not really an issue when doing mathematics, but when formalising it in type theory you might find that it becomes a pain and you'd be better off setting things up with E a field and F an E-algebra.

view this post on Zulip Kenny Lau (Dec 31 2019 at 14:34):

import algebra.ring
import data.equiv.algebra
import field_theory.subfield

universes u

-- Define fixes k f for any f : ring_aut K.
def fixes {K : Type u} [discrete_field K] (k : set K) [is_subfield k] (f : ring_aut K) : Prop :=
 x  k, @coe_fn _ ring_equiv.has_coe_to_fun f x = x

-- Define gal K k.
def gal (K : Type*) [discrete_field K] (k : set K) [is_subfield k] :=
{ α : K +* K // fixes k α }

instance {K : Type*} [discrete_field K] {k : set K} [is_subfield k] :
  has_coe (gal K k) (ring_aut K) :=
⟨λ s, s.val

instance {K : Type*} [discrete_field K] {k : set K} [is_subfield k] :
  group (gal K k) :=
@subtype.group (ring_aut K) _ { f | fixes k f }
{ mul_mem := λ f g hf hg x hx, show f.1 (g.1 x) = x, by rw [show g.1 x = x, from hg x hx]; exact hf x hx,
  one_mem := λ x hx, rfl,
  inv_mem := λ f hf x hx, (equiv.symm_apply_eq _).2 $ eq.symm $ hf x hx }

view this post on Zulip Kevin Buzzard (Dec 31 2019 at 14:34):

theorem aut_one_fixes_k : fixes k aut_one := begin intro, refl end You don't need the rewrite, because it's true by definition ;-)

view this post on Zulip Kenny Lau (Dec 31 2019 at 14:35):

@Kevin Buzzard try as I might, I cannot fix the line with @coe_fn _ ring_equiv.has_coe_to_fun f x = x (L9)

view this post on Zulip Kenny Lau (Dec 31 2019 at 14:35):

you might be familiar with priority tricks

view this post on Zulip Kevin Buzzard (Dec 31 2019 at 14:35):

theorem aut_one_fixes_k : fixes k aut_one := λ _, rfl is the term mode version

view this post on Zulip Kevin Buzzard (Dec 31 2019 at 14:38):

Kevin Buzzard try as I might, I cannot fix the line with @coe_fn _ ring_equiv.has_coe_to_fun f x = x (L9)

 x  k, f.to_equiv x = x

? I remember talking about this with Mario. I think there's no coercion from all these higher equivs to regular equiv, and perhaps this is for a reason.

view this post on Zulip Kenny Lau (Dec 31 2019 at 14:38):

but why isn't the ring_equiv.has_coe_to_fun instance triggering

view this post on Zulip James Weaver (Dec 31 2019 at 14:38):

You do seem to have to manually cast them using to_equiv

view this post on Zulip Kenny Lau (Dec 31 2019 at 14:38):

@James Weaver btw this is how I would construct the group structure

view this post on Zulip Kenny Lau (Dec 31 2019 at 14:39):

then what is ring_equiv.has_coe_to_fun for

view this post on Zulip James Weaver (Dec 31 2019 at 14:41):

@subtype.group is a new one to me

view this post on Zulip Kevin Buzzard (Dec 31 2019 at 14:42):

In type theory a set is a term, not a type.

view this post on Zulip Kevin Buzzard (Dec 31 2019 at 14:42):

So group X doesn't make sense if X is a subset of Y.

view this post on Zulip Kevin Buzzard (Dec 31 2019 at 14:42):

It doesn't typecheck.

view this post on Zulip Kevin Buzzard (Dec 31 2019 at 14:43):

If X is a subgroup of G, then subtype.group is the function you need to create the group ↥X term

view this post on Zulip James Weaver (Dec 31 2019 at 14:44):

right, I see

view this post on Zulip Kevin Buzzard (Dec 31 2019 at 14:44):

where that weird little up-arrow means "change the subset X into a subtype"

view this post on Zulip Kevin Buzzard (Dec 31 2019 at 14:45):

You can figure out what Kenny is doing by just writing #check @subtype.group. The @ sign means "let me fill in all of the inputs to the function myself, even the ones you usually guess for me in the {} and [] brackets"

view this post on Zulip Kevin Buzzard (Dec 31 2019 at 14:47):

but why isn't the ring_equiv.has_coe_to_fun instance triggering

Is it because ring_aut isn't syntactically equivalent to ring_equiv?

view this post on Zulip James Weaver (Dec 31 2019 at 14:47):

/me nods

view this post on Zulip James Weaver (Dec 31 2019 at 14:48):

Right, and the $ is function application with a different binding weight so as to avoid excessive parentheses?

view this post on Zulip Kenny Lau (Dec 31 2019 at 14:48):

I tried ∀ x ∈ k, (f : K ≃+* K) x = x @Kevin Buzzard

view this post on Zulip James Weaver (Dec 31 2019 at 14:48):

(Like in Haskel)

view this post on Zulip Kevin Buzzard (Dec 31 2019 at 14:49):

I tried ∀ x ∈ k, (f : K ≃+* K) x = x Kevin Buzzard

Maybe that's one of those "check that f can be considered as having type ring_equiv but don't actually change what Lean thinks the type of f is?" issues?

view this post on Zulip Kevin Buzzard (Dec 31 2019 at 14:50):

instance (α : Type*) [ring α] : has_coe_to_fun (ring_aut α) := ⟨_, ring_equiv.to_fun

def fixes {K : Type u} [discrete_field K] (k : set K) [is_subfield k] (f : ring_aut K) : Prop :=
 x  k, f x = x

view this post on Zulip Kenny Lau (Dec 31 2019 at 14:50):

ok ∀ x ∈ k, (show K ≃+* K, from f) x = x worked but that is only zeta equivalent

view this post on Zulip Kenny Lau (Dec 31 2019 at 14:50):

instance (α : Type*) [ring α] : has_coe_to_fun (ring_aut α) := ⟨_, ring_equiv.to_fun

def fixes {K : Type u} [discrete_field K] (k : set K) [is_subfield k] (f : ring_aut K) : Prop :=
 x  k, f x = x

nice

view this post on Zulip Kevin Buzzard (Dec 31 2019 at 14:50):

So arguably there's a missing instance here.

view this post on Zulip Kevin Buzzard (Dec 31 2019 at 14:51):

(and I don't care if I made a loop in the instance graph because eveything is defeq)

view this post on Zulip Kenny Lau (Dec 31 2019 at 14:51):

import algebra.ring
import data.equiv.algebra
import field_theory.subfield

universes u

-- credit Kevin Buzzard
instance (α : Type*) [ring α] : has_coe_to_fun (ring_aut α) := ⟨_, ring_equiv.to_fun

-- Define fixes k f for any f : ring_aut K.
def fixes {K : Type u} [discrete_field K] (k : set K) [is_subfield k] (f : ring_aut K) : Prop :=
 x  k, f x = x

-- Define gal K k.
def gal (K : Type*) [discrete_field K] (k : set K) [is_subfield k] :=
{ α : K +* K // fixes k α }

instance {K : Type*} [discrete_field K] {k : set K} [is_subfield k] :
  has_coe (gal K k) (ring_aut K) :=
⟨λ s, s.val

instance {K : Type*} [discrete_field K] {k : set K} [is_subfield k] :
  group (gal K k) :=
@subtype.group (ring_aut K) _ { f | fixes k f }
{ mul_mem := λ f g hf hg x hx, show f (g x) = x, by rw hg x hx; exact hf x hx,
  one_mem := λ x hx, rfl,
  inv_mem := λ f hf x hx, (equiv.symm_apply_eq _).2 $ eq.symm $ hf x hx }

view this post on Zulip Kenny Lau (Dec 31 2019 at 14:51):

now the code is cleaner

view this post on Zulip Kevin Buzzard (Dec 31 2019 at 14:56):

theorem gal_one_mul :  (a : gal K k), gal_mul gal_one a = a :=
begin
  intro a,
  unfold gal_mul gal_one,
  unfold_coes,
  dsimp,
...

is another way of getting around the change issue. But actually the correct thing to do is to play around like I'm doing above, and then see what you want to change the goal to, and then use change the way Kenny said.

view this post on Zulip James Weaver (Dec 31 2019 at 14:58):

I did find the operation of the function set a little surprising
I would have expected set K to be an assertion that K is a set or a way of accessing the underlying set of K, but it seems that set K is the type of subsets of the underlying set of K.

view this post on Zulip Kevin Buzzard (Dec 31 2019 at 14:58):

There's no "underlying set" -- it's type theory.

view this post on Zulip Kevin Buzzard (Dec 31 2019 at 14:59):

I spent a long time mentally changing set K to subset_of K before I got the hang of it.

view this post on Zulip Kevin Buzzard (Dec 31 2019 at 15:00):

This kerfuffle is one reason why I would consider setting it up with k and K both types and an injective field map k -> K. This is a delicate type theory foundational issue which has burned me in the past (I wrote a bunch of MSc level algebraic and arithmetic geometry up in Lean and it taught me loads about what to avoid -- the hard way).

view this post on Zulip James Weaver (Dec 31 2019 at 15:01):

That's always the way when learning a language I find. You learn by doing wrongly.

view this post on Zulip Kevin Buzzard (Dec 31 2019 at 15:02):

The way to think about it is to imagine what might come your way in the future which you might want to apply your theory to, and if your theory only applies after a lot of pain then you might have set up your theory incorrectly. The p-adic valuation of 0 is +infinity and as you can imagine, this is a pain. But here's a summary of how it caused me far more pain than it should have done.

view this post on Zulip Kevin Buzzard (Dec 31 2019 at 15:03):

We were setting up a theory of adic spaces so we needed a theory of norms on general rings. A general norm takes values (in the mathematical literature) in the set 0Γ{0}\cup\Gamma where Γ\Gamma is a totally ordered group under multiplication (for example the positive reals). We dutifully defined a new function which ate Gamma and spat out {0} union Gamma.

view this post on Zulip Kevin Buzzard (Dec 31 2019 at 15:05):

and then let our norms take values in this. And then we tried to unify our work with the p-adic norm, but the p-adic norm was taking values in the non-negative real numbers :-/ and although this might be canonically isomorphic to {0} union (positive reals), it wasn't _equal_ to it, so there was a lot of faffing around which culminated in our changing our definition of a general norm.

view this post on Zulip Kevin Buzzard (Dec 31 2019 at 15:05):

This issue doesn't exist mathematically, because of course R0=R>0{0}\mathbb{R}_{\geq0}=\mathbb{R}_{>0}\cup\{0\}, but this is a set-theoretic equals not a type-theoretic one.

view this post on Zulip Kevin Buzzard (Dec 31 2019 at 15:06):

in type theory, there are maps in both directions and you can get sick of them very quickly.

view this post on Zulip Kevin Buzzard (Dec 31 2019 at 15:08):

so if you want to do Gal(C/R) with your Galois theory, but for some reason you want to use Lean's real numbers, which are of course not defined as a subfield of the complex numbers, then you'll be forever passing between Lean's real numbers and the subfield of C.

view this post on Zulip Kevin Buzzard (Dec 31 2019 at 15:08):

something which is completely transparent to a mathematician but which is an issue when formalising.

view this post on Zulip James Weaver (Dec 31 2019 at 15:08):

ugh, yes

view this post on Zulip James Weaver (Dec 31 2019 at 15:09):

To be honest mathematicians can get very sloppy with equality and isomorphism

view this post on Zulip Kevin Buzzard (Dec 31 2019 at 15:11):

Mathematicians know that nothing changes if you move from the reals as Cauchy sequences to the reals as Dedekind cuts to the reals as a subfield of C, but really these are all ("canonical") isomorphisms, and they are sufficiently canonical that any sensible mathematical statement about "the reals" will be true for one iff it's true for all of them. However there are stupid statements which are only true for some and not for others (e.g. in set theory one could ask "is the real number 37 a countable or an uncountable set?") and in type theory there are analogous pathological (i.e. non-mathematical) questions which one could ask about "the reals" which might be true for one model and false for others.

view this post on Zulip Kevin Buzzard (Dec 31 2019 at 15:12):

This means that working with isomorphisms is harder than it should be (e.g. you can't rw h if h is a proof that the rings A and B are isomorphic, and you have a proof that A is Noetherian, and your goal is to prove that B is Noetherian).

view this post on Zulip Kevin Buzzard (Dec 31 2019 at 15:13):

one day a computer scientist will come and write some kind of rw on steroids which will let us rewrite here, because Noetherian will be tagged with a special tag saying "this predicate on rings is constant on isomorphism classes"

view this post on Zulip Kevin Buzzard (Dec 31 2019 at 15:14):

but that hasn't happened yet.

view this post on Zulip James Weaver (Jan 01 2020 at 12:42):

Right, after some changes based on what you both said yesterday this is what I have now:

import algebra.ring
import data.equiv.algebra
import field_theory.subfield

universes u

-- Causes ring automorphisms K ≃+* K to be coercible to functions K → K
-- credit Kevin Buzzard
instance (α : Type*) [ring α] : has_coe_to_fun (ring_aut α) := ⟨_, ring_equiv.to_fun

-- Define a field extension as a chosen monomorphism k → K
structure field_extension
    (K k : Type*) [discrete_field k] [discrete_field K]
        := mk :: (inc: ring_hom k K) (inj: function.injective inc.to_fun)

-- Define a coercion from a field extension to a ring_homomorphism, this in turn provides coercions to
-- other types including k → K
instance
    (K k : Type*) [discrete_field k] [discrete_field K] :
        has_coe (field_extension K k) (ring_hom k K) := ⟨λ ext, ext.inc


-- Define fixes k f for any f : ring_aut K.
def fixes
    {K k : Type u} [discrete_field k] [discrete_field K]
    (ext: field_extension K k) (f : ring_aut K)
        : Prop :=  x : k, f (ext x) = ext x

-- Define gal for an extension
def gal
    {K k : Type u} [discrete_field k] [discrete_field K]
    (K_k: field_extension K k)
        := { α : ring_aut K // fixes K_k α }

-- Define a coercion from gal K_k to ring_aut K
-- This in turn will allow coercions further including to K → K
instance
    {K k : Type u} [discrete_field k] [discrete_field K]
    (K_k: field_extension K k) :
        has_coe (gal K_k) (ring_aut K) :=
            ⟨λ s, s.val

-- Prove that gal K_k is a group under composition
instance
    {K k : Type u} [discrete_field k] [discrete_field K]
    (K_k: field_extension K k) :
        group (gal K_k) :=
@subtype.group (ring_aut K) _ { f | fixes K_k f }
{ mul_mem := λ f g hf hg x, show f (g $ K_k x) = K_k x, by rw hg x; exact hf x,
  one_mem := λ x, by refl,
  inv_mem := λ f hf x, (equiv.symm_apply_eq _).2 $ eq.symm $ hf x }

which seems fine in of itself, but when I try adding this below:

instance (K k : Type*) [discrete_field k] [discrete_field K] (K_k : field_extension K k) : has_coe k K := K_k


variable K : Type u
variable k : Type u
variable f : K  K
variable [discrete_field k]
variable [discrete_field K]

#check f (discrete_field.one k)

I get a peculiar (to me) error where it complains that it can't automatically synthesise a name for the has_coe instance, which is odd since no other has_coe instance I've seen has needed an explicit name. Adding an explicit name fixes that error, but the check in the last line doesn't seem to find the coercion from k to K and complains that discrete_field one k isn't a K.

Any thoughts? Have I made another obvious mistake somewhere?

view this post on Zulip Kenny Lau (Jan 01 2020 at 12:43):

every ring hom between two fields is injective

view this post on Zulip James Weaver (Jan 01 2020 at 12:44):

Of course it is. Shows how long it's been since I was doing maths regularly.

view this post on Zulip James Weaver (Jan 01 2020 at 12:53):

Ok, right, so that being the case, this seems sufficient:

import algebra.ring
import data.equiv.algebra
import field_theory.subfield

universes u

-- Causes ring automorphisms K ≃+* K to be coercible to functions K → K
-- credit Kevin Buzzard
instance (α : Type*) [ring α] : has_coe_to_fun (ring_aut α) := ⟨_, ring_equiv.to_fun


-- Define fixes k f for any f : ring_aut K.
def fixes
    {K k : Type u} [discrete_field k] [discrete_field K]
    (ext: k →+* K) (f : ring_aut K)
        : Prop :=  x : k, f (ext x) = ext x

-- Define gal for an extension
def gal
    {K k : Type u} [discrete_field k] [discrete_field K]
    (K_k: k →+* K)
        := { α : ring_aut K // fixes K_k α }

-- Define a coercion from gal K_k to ring_aut K
-- This in turn will allow coercions further including to K → K
instance
    {K k : Type u} [discrete_field k] [discrete_field K]
    (K_k: k →+* K) :
        has_coe (gal K_k) (ring_aut K) :=
            ⟨λ s, s.val

-- Prove that gal K_k is a group under composition
instance
    {K k : Type u} [discrete_field k] [discrete_field K]
    (K_k: k →+* K) :
        group (gal K_k) :=
@subtype.group (ring_aut K) _ { f | fixes K_k f }
{ mul_mem := λ f g hf hg x, show f (g $ K_k x) = K_k x, by rw hg x; exact hf x,
  one_mem := λ x, by refl,
  inv_mem := λ f hf x, (equiv.symm_apply_eq _).2 $ eq.symm $ hf x }

view this post on Zulip James Weaver (Jan 01 2020 at 13:01):

Still running into a problem with

-- introduce an example
variable K : Type u
variable k : Type u
variable [discrete_field k]
variable [discrete_field K]
variable i : k →+* K

instance n:has_coe k K := i

variable f : K  K

#check f (1 : k)

though. The has_coe instance demands an explicit name and isn't found by the #check command.

view this post on Zulip Alex J. Best (Jan 01 2020 at 13:10):

I think your problem is that i is a variable, the following works

universe u


variable K : Type*
variable k : Type*
variable [discrete_field k]
variable [discrete_field K]
def i : k →+* K := sorry

instance n : has_coe k K := i K k
variable f : K  K

#check f (1 : k)

view this post on Zulip Alex J. Best (Jan 01 2020 at 13:14):

I don't know exactly what your use case is so maybe this isnt that useful? But before you had n depending on i so the coercion couldn't just pick one ito make the coercion from?


Last updated: May 18 2021 at 16:25 UTC