Another diamond

Stream: general

[Riccardo Brasca]

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]

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

[Eric Wieser]

Does one instance imply the other?

[Anne Baanen]

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]

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]

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

[Eric Wieser]

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

[Anne Baanen]

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

[Riccardo Brasca]

This line doesn't work without

local attribute [-instance] alg_hom.fintype

[Riccardo Brasca]

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

[Anne Baanen]

Let me check the code...

[Eric Wieser]

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

[Eric Wieser]

Lean will use that one before doing a full search

[Anne Baanen]

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

[Anne Baanen]

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

[Anne Baanen]

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

pp.implicit?

[Anne Baanen]

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]

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]

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

[Anne Baanen]

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]

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

[Riccardo Brasca]

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

[Anne Baanen]

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

[Riccardo Brasca]

:face_palm:

[Anne Baanen]

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]

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]

I think this is a very good idea!

[Eric Wieser]

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

[Eric Wieser]

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]

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]

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