Invalid Constructor

Stream: new members

[James Weaver]

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⟩.

[Kenny Lau]

use ```lean to enable syntax highlighting

[Kenny Lau]

```lean
lorem ipsum
```

[Kenny Lau]

change that line to:

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

[Kenny Lau]

Lean elaborates from left to right

[Kenny Lau]

so Lean sees the anonymous constructor before it sees a

[Kenny Lau]

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

[Kenny Lau]

but Lean cannot figure out the type of the anonymous constructor

[James Weaver]

Thanks, that really helps!

[Kevin Buzzard]

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.

[Kenny Lau]

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 }

[Kevin Buzzard]

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 ;-)

[Kenny Lau]

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

[Kenny Lau]

you might be familiar with priority tricks

[Kevin Buzzard]

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

[Kevin Buzzard]

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.

[Kenny Lau]

but why isn't the ring_equiv.has_coe_to_fun instance triggering

[James Weaver]

You do seem to have to manually cast them using to_equiv

[Kenny Lau]

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

[Kenny Lau]

then what is ring_equiv.has_coe_to_fun for

[James Weaver]

@subtype.group is a new one to me

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

It doesn't typecheck.

[Kevin Buzzard]

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

[James Weaver]

right, I see

[Kevin Buzzard]

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

[Kevin Buzzard]

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"

[Kevin Buzzard]

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?

[James Weaver]

/me nods

[James Weaver]

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

[Kenny Lau]

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

[James Weaver]

(Like in Haskel)

[Kevin Buzzard]

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?

[Kevin Buzzard]

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

[Kenny Lau]

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

[Kenny Lau]

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

[Kevin Buzzard]

So arguably there's a missing instance here.

[Kevin Buzzard]

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

[Kenny Lau]

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 }

[Kenny Lau]

now the code is cleaner

[Kevin Buzzard]

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.

[James Weaver]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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).

[James Weaver]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

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}\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.

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[James Weaver]

ugh, yes

[James Weaver]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

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).

[Kevin Buzzard]

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"

[Kevin Buzzard]

but that hasn't happened yet.

[James Weaver]

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?

[Kenny Lau]

every ring hom between two fields is injective

[James Weaver]

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

[James Weaver]

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 }

[James Weaver]

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.

[Alex J. Best]

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)

[Alex J. Best]

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?