Zulip Chat Archive

Stream: general

Topic: Another diamond


Riccardo Brasca (Nov 17 2021 at 10:26):

Working on FLT-regular, I found another diamond that I am not sure how to correct. Here is a #mwe

import field_theory.fixed
import field_theory.primitive_element

variables (K F E : Type*) [field K] [field F] [field E] [algebra K F] [algebra K E]
variables [finite_dimensional K F] [finite_dimensional K E] [is_separable K F]

noncomputable example : fintype (F →ₐ[K] E) := field.alg_hom.fintype K F

noncomputable example : fintype (F →ₐ[K] E) := alg_hom.fintype K F E

example : (field.alg_hom.fintype K F) = (alg_hom.fintype K F E) := rfl --fails

Note that both field.alg_hom.fintype and alg_hom.fintype are instances, so this can causes problems (and indeed it did for me, I had to manually disable one instance).

What should we do?

Anne Baanen (Nov 17 2021 at 10:30):

docs#field.alg_hom.fintype docs#alg_hom.fintype for the lazy (like me)

Eric Wieser (Nov 17 2021 at 10:36):

Does one instance imply the other?

Anne Baanen (Nov 17 2021 at 10:37):

Hmm, both seem reasonable enough, one is not a specialization of the other, and I don't really have the idea that one would be more useful than the other. So my suggestion would be to just add a note to the docstring saying "use local attribute [-instance] if you get conflicts with the other"

Anne Baanen (Nov 17 2021 at 10:37):

Eric Wieser said:

Does one instance imply the other?

No, one uses assumptions on the extension F/E and the other assumptions on K/E.

Eric Wieser (Nov 17 2021 at 10:37):

Where does the diamond actually cause you trouble @Riccardo Brasca?

Eric Wieser (Nov 17 2021 at 10:38):

One way to solve this type of thing is to change lemmas to take dumber [fintype _] arguments

Anne Baanen (Nov 17 2021 at 10:38):

Evil answer: make fintype a Prop so there can be no defeq diamonds

Riccardo Brasca (Nov 17 2021 at 10:39):

This line doesn't work without

local attribute [-instance] alg_hom.fintype

Riccardo Brasca (Nov 17 2021 at 10:41):

The problem is rw [this], so maybe stating this differently it's enough.

Anne Baanen (Nov 17 2021 at 10:45):

Let me check the code...

Eric Wieser (Nov 17 2021 at 10:51):

Another solution is to add letI : fintype (K →ₐ[ℚ] E) := ... before you create this, and replace ... with the instance you actually want

Eric Wieser (Nov 17 2021 at 10:52):

Lean will use that one before doing a full search

Anne Baanen (Nov 17 2021 at 11:06):

Wait hang on, why does Lean think finite_dimensional ℚ (algebraic_closure ℚ) is true anyway?

Anne Baanen (Nov 17 2021 at 11:07):

Pretty sure algebraic_closure ℚ is not generated by a single element, right?

Anne Baanen (Nov 17 2021 at 11:07):

#check is_cyclotomic_extension.finite_dimensional
-- is_cyclotomic_extension.finite_dimensional : ∀ (K L : Type*) [field K] [field L] [algebra K L], finite_dimensional K L

:thinking:

Eric Wieser (Nov 17 2021 at 11:13):

pp.implicit?

Anne Baanen (Nov 17 2021 at 11:15):

Indeed, pp.implicit shows the term with alg_hom.fintype uses is_cyclotomic_extension.finite_dimensional, a lemma which is in fact, not true.

Eric Wieser (Nov 17 2021 at 11:16):

Oh, I assumed that is_cyclotomic_extension.finite_dimensional was true but was stated about some weird algebra/ring instance. Clearly there's a danger to sorrying lemmas!

Anne Baanen (Nov 17 2021 at 11:17):

Fixing that instance to be actually true should fix this specific issue, but the generic one remains.

Anne Baanen (Nov 17 2021 at 11:27):

Another approach in this specific case is to replace the have line with calc:

lemma norm_zeta'_sub_one [hp : fact (p : ).prime] (hodd : p  2) :
  norm  ((zeta' p  K) - 1) = p :=
begin
  let E := algebraic_closure ,
  letI := char_zero_of_injective_algebra_map (algebra_map  E).injective,
  have hpE : ((p : ) : E)  0 := λ h, p.pos.ne (cast_eq_zero.1 h).symm,
  obtain z, hz := is_alg_closed.exists_root _ (degree_cyclotomic_pos p E p.pos).ne.symm,

  apply (algebra_map  E).injective,
  rw norm_eq_prod_embeddings,
  conv_lhs { congr, skip, funext,
    rw [ neg_sub, alg_hom.map_neg, alg_hom.map_sub, alg_hom.map_one, neg_eq_neg_one_mul] },
  replace hodd : (p : )  2 := λ hn, by exact hodd.symm (pnat.coe_inj.1 hn.symm),
  rw [prod_mul_distrib, prod_const, card_univ, alg_hom.card, finrank p,
    totient_prime hp.out, neg_one_pow_of_even (even_of_prime_neq_two_sub_one hp.out hodd), one_mul],
  calc _ = eval 1 (cyclotomic' p E) : _
  ... = _ : _,
  { rw [cyclotomic', eval_prod,  @finset.prod_attach E E,  univ_eq_attach],
    -- The following line would still fail if we write `_` instead of the `(id _)` (or with no `@` at all).
    -- `(id _)` is a trick to disable instance search.
    refine @fintype.prod_equiv _ _ _ (id _) (id _) _ _ _ _ _,
    { exact zeta'.embeddings_equiv_primitive_roots p  K E },
    intro σ, simp only [eval_sub, eval_X, eval_C, zeta'.embeddings_equiv_primitive_roots_apply] },
  rw [cyclotomic',  cyclotomic_eq_prod_X_sub_primitive_roots
    ((is_root_cyclotomic_iff hpE).2 hz), eval_one_cyclotomic_prime],
  simp,
end

Riccardo Brasca (Nov 17 2021 at 11:30):

Ops, I thought is_cyclotomic_extension.finite_dimensional automatically included [fintype S], thank's!

Riccardo Brasca (Nov 17 2021 at 11:31):

But I don't understand why Lean thinks thatℚ (algebraic_closure ℚ) is a cyclotomic extension.

Anne Baanen (Nov 17 2021 at 11:34):

Look carefully, is_cyclotomic_extension.finite_dimensional doesn't include any is_cyclotomic_extension assumptions!

Riccardo Brasca (Nov 17 2021 at 11:35):

:face_palm:

Anne Baanen (Nov 17 2021 at 11:36):

So in cyclotomic/basic.lean you probably want to replace the start of section fintype with:

variables [h₁ : fintype S] [h₂ : is_cyclotomic_extension S K L]
include h₁ h₂

Kevin Buzzard (Nov 17 2021 at 12:51):

I really like the idea of making fintype a Prop BTW, or, more precisely, making a Proppy fintype like we have set.finite (a Proppy finset).

Riccardo Brasca (Nov 17 2021 at 13:17):

I think this is a very good idea!

Eric Wieser (Nov 17 2021 at 13:19):

I suspect if we had such a finite typeclass, then src#set.finite could probably be defined in terms of it

Eric Wieser (Nov 17 2021 at 13:20):

That is, replace:

inductive set.finite (s : set α) : Prop
| intro : fintype s  set.finite

with

inductive finite (α : Type*) : Prop
| intro : fintype α  finite

def set.finite (s : set α) : Prop := finite s

Scott Morrison (Nov 17 2021 at 21:18):

One thing to note: tactic#fin_cases works if it can find a fintype instance, but would not be able to do anything with finite.

Reid Barton (Nov 17 2021 at 21:23):

How does that work? It seems like the fintype instance is at the wrong "level"


Last updated: Dec 20 2023 at 11:08 UTC