IntermediateField.mem_adjoin_iff

Stream: Is there code for X?

[Jz Pan]

Do we have these?

import Mathlib.FieldTheory.SplittingField.Construction
import Mathlib.FieldTheory.IsAlgClosed.Basic
import Mathlib.FieldTheory.Separable
import Mathlib.RingTheory.IntegralDomain

theorem IntermediateField.mem_adjoin_iff (F E : Type*) [Field F] [Field E]
    [Algebra F E] {S : Set E} (x : E) :
    x ∈ IntermediateField.adjoin F S ↔ (∃ r s : MvPolynomial S F,
      x = MvPolynomial.aeval (fun y ↦ y.1) r / MvPolynomial.aeval (fun y ↦ y.1) s) := by
  sorry

theorem IntermediateField.mem_adjoin_simple_iff (F E : Type*) [Field F] [Field E]
    [Algebra F E] {α : E} (x : E) :
    x ∈ IntermediateField.adjoin F {α} ↔ (∃ r s : Polynomial F,
      x = Polynomial.aeval α r / Polynomial.aeval α s) := by
  sorry

I hope these formulations are correct: it's possible that the aeval of s is zero, but this is still correct since anything divide by zero is zero in Lean, so it is still in that field.

[Junyan Xu]

docs#IntermediateField.adjoin is defined in terms of docs#Subfield.closure, and there is docs#Subfield.mem_closure_iff.

For docs#Algebra.adjoin we have docs#Algebra.adjoin_singleton_eq_range_aeval (and docs#Algebra.adjoin_eq_range for any set and MvPolynomial), and docs#Algebra.adjoin_eq_ring_closure says Subring.closure (Set.range (algebraMap F E) ∪ S) = Algebra.adjoin F S.
We also get polynomial representations for docs#Subring.closure and docs#Subsemiring.closure via docs#Algebra.adjoin_nat and docs#Algebra.adjoin_int. However, there isn't a Algebra.adjoin_eq_semiring_closure.

P.S. I found some of these using loogle (example 1, 2).

[Jz Pan]

Thanks, currently I'm lost in the implication chain. Will check them later.

[Jz Pan]

OK this code works:

import Mathlib.FieldTheory.SplittingField.Construction
import Mathlib.FieldTheory.IsAlgClosed.Basic
import Mathlib.FieldTheory.Separable
import Mathlib.RingTheory.IntegralDomain

theorem IntermediateField.mem_adjoin_iff (F E : Type*) [Field F] [Field E]
    [Algebra F E] {S : Set E} (x : E) :
    x ∈ IntermediateField.adjoin F S ↔ (∃ r s : MvPolynomial S F,
      x = MvPolynomial.aeval Subtype.val r / MvPolynomial.aeval Subtype.val s) := by
  simp only [adjoin, mem_mk, Subring.mem_toSubsemiring, Subfield.mem_toSubring,
    Subfield.mem_closure_iff, ← Algebra.adjoin_eq_ring_closure, Subalgebra.mem_toSubring,
    Algebra.adjoin_eq_range, AlgHom.mem_range, exists_exists_eq_and]
  tauto

theorem IntermediateField.mem_adjoin_simple_iff (F E : Type*) [Field F] [Field E]
    [Algebra F E] {α : E} (x : E) :
    x ∈ IntermediateField.adjoin F {α} ↔ (∃ r s : Polynomial F,
      x = Polynomial.aeval α r / Polynomial.aeval α s) := by
  simp only [adjoin, mem_mk, Subring.mem_toSubsemiring, Subfield.mem_toSubring,
    Subfield.mem_closure_iff, ← Algebra.adjoin_eq_ring_closure, Subalgebra.mem_toSubring,
    Algebra.adjoin_singleton_eq_range_aeval, AlgHom.mem_range, exists_exists_eq_and]
  tauto

At first I want to use IntermediateField.mem_adjoin_iff to prove IntermediateField.mem_adjoin_simple_iff but somehow usingMvPolynomial.pUnitAlgEquiv is not as easy as copying the proof again.

[Jz Pan]

Are these worth to be added to mathlib? It looks like that the existing mem_xxx_iff doesn't look like these two.

[Eric Wieser]

Those look like good lemmas to me, though the second one should be called mem_adjoin_singleton_iff

[Jz Pan]

Eric Wieser said:

the second one should be called mem_adjoin_singleton_iff

In the file Mathlib.FieldTheory.Adjoin they are usually called simple, though.

[Jz Pan]

For example docs#IntermediateField.mem_adjoin_simple_self

[Thomas Browning]

Yeah, the adjoin lemmas should probably be renamed.

[Thomas Browning]

What do you need these lemmas for?

[Jz Pan]

Thomas Browning said:

What do you need these lemmas for?

https://github.com/leanprover-community/mathlib4/blob/e0830b7f850af1feb80b9ebfee2ec2d17b397b52/Mathlib/FieldTheory/PrimitiveElement.lean#L264