## Stream: new members

### Topic: Invalid Constructor

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

#### Kenny Lau (Dec 31 2019 at 14:16):

use lean to enable syntax highlighting

#### Kenny Lau (Dec 31 2019 at 14:17):

lean
lorem ipsum



#### 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,


#### Kenny Lau (Dec 31 2019 at 14:19):

Lean elaborates from left to right

#### Kenny Lau (Dec 31 2019 at 14:19):

so Lean sees the anonymous constructor before it sees a

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

#### Kenny Lau (Dec 31 2019 at 14:19):

but Lean cannot figure out the type of the anonymous constructor

#### James Weaver (Dec 31 2019 at 14:23):

Thanks, that really helps!

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

#### 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 }


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

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

#### Kenny Lau (Dec 31 2019 at 14:35):

you might be familiar with priority tricks

#### Kevin Buzzard (Dec 31 2019 at 14:35):

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

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

#### Kenny Lau (Dec 31 2019 at 14:38):

but why isn't the ring_equiv.has_coe_to_fun instance triggering

#### James Weaver (Dec 31 2019 at 14:38):

You do seem to have to manually cast them using to_equiv

#### Kenny Lau (Dec 31 2019 at 14:38):

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

#### Kenny Lau (Dec 31 2019 at 14:39):

then what is ring_equiv.has_coe_to_fun for

#### James Weaver (Dec 31 2019 at 14:41):

@subtype.group is a new one to me

#### Kevin Buzzard (Dec 31 2019 at 14:42):

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

#### Kevin Buzzard (Dec 31 2019 at 14:42):

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

#### Kevin Buzzard (Dec 31 2019 at 14:42):

It doesn't typecheck.

#### 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

right, I see

#### Kevin Buzzard (Dec 31 2019 at 14:44):

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

#### 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"

#### 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?

/me nods

Right, and the $is function application with a different binding weight so as to avoid excessive parentheses? #### Kenny Lau (Dec 31 2019 at 14:48): I tried ∀ x ∈ k, (f : K ≃+* K) x = x @Kevin Buzzard #### James Weaver (Dec 31 2019 at 14:48): (Like in Haskel) #### 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? #### 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  #### 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 #### 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 #### Kevin Buzzard (Dec 31 2019 at 14:50): So arguably there's a missing instance here. #### 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) #### 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 }  #### Kenny Lau (Dec 31 2019 at 14:51): now the code is cleaner #### 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. #### 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. #### Kevin Buzzard (Dec 31 2019 at 14:58): There's no "underlying set" -- it's type theory. #### 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. #### 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). #### James Weaver (Dec 31 2019 at 15:01): That's always the way when learning a language I find. You learn by doing wrongly. #### 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. #### 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}\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 (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. #### Kevin Buzzard (Dec 31 2019 at 15:05): 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 (Dec 31 2019 at 15:06): in type theory, there are maps in both directions and you can get sick of them very quickly. #### 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. #### Kevin Buzzard (Dec 31 2019 at 15:08): something which is completely transparent to a mathematician but which is an issue when formalising. #### James Weaver (Dec 31 2019 at 15:08): ugh, yes #### James Weaver (Dec 31 2019 at 15:09): To be honest mathematicians can get very sloppy with equality and isomorphism #### 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. #### 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). #### 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" #### Kevin Buzzard (Dec 31 2019 at 15:14): but that hasn't happened yet. #### 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?

#### Kenny Lau (Jan 01 2020 at 12:43):

every ring hom between two fields is injective

#### James Weaver (Jan 01 2020 at 12:44):

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

#### 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 }


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

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


#### 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 i`to make the coercion from?

Last updated: May 18 2021 at 16:25 UTC