Submodule that is also a field

Stream: new members

[Tainnor]

I have a field extension F of R and I need to construct a submodule of it and prove that it's also a field. I don't have any issues proving this mathematically, but I don't know how to do this in Lean's type system.

I tried defining

import Mathlib

open Module FiniteDimensional

def two_dim_subfield [Field F] [Algebra ℝ F] [Module.Finite ℝ F] {z : F}
    (notinr : ∀ (r : ℝ), r•1 ≠ z) : Subfield F :=
  ((Submodule.span ℝ ({1, z} : Set F)).toSubalgebra (by sorry) (by sorry)).toSubring.toSubfield (by sorry)

(and I actually have working code that is filling those sorrys) which gives me something that is immediately a Field, but I don't know how to show that it's a submodule of F and that it's a 2D algebra over R. Basically, I can't extract the Submodule.span that is wrapped under all these toX functions.

If it's not possible to provide instances directly, I guess a bijection would also be fine. But anyway, I don't really have a clue how to approach this. Maybe this should also be done in an entirely different way.

[Kenny Lau]

I think from what I've heard this is indeed a missing corner of the library nvm!

[Eric Wieser]

Are you looking for docs#IntermediateField.adjoin ?

[Kenny Lau]

oh yeah, @Tainnor your code + description is mathematically wrong, there's nothing there saying that z is quadratic

[Kenny Lau]

when you add that back in, then you can use IntermediateField.adjoin.finrank:

/-- If `x` is an algebraic element of field `K`, then its minimal polynomial has degree
`[K(x) : K]`. -/
@[stacks 09GN]
theorem adjoin.finrank {x : L} (hx : IsIntegral K x) :
    Module.finrank K K⟮x⟯ = (minpoly K x).natDegree

[Tainnor]

Kenny Lau said:

oh yeah, Tainnor your code + description is mathematically wrong, there's nothing there saying that z is quadratic

huh, what do you mean by mathematically wrong, which part exactly?

[Tainnor]

fwiw, this is my full code (minus the proof for polynomial factorization of R) and it compiles, and it also seems obvious to me that this is 2d:

import Mathlib

variable (F : Type*)
[Field F] [Algebra ℝ F] [Module.Finite ℝ F]

open Module FiniteDimensional LinearIndependent

open Polynomial

theorem real_polynomial_factorization (p : ℝ[X]) :
    ∃ (n m : ℕ) (a : Fin n → ℝ) (b₁ b₂ : Fin m → ℝ), p.natDegree = n+2*m
      ∧ (∀ k, b₂ k ≠ 0)
      ∧ p = p.leadingCoeff • ((∏ k, (X - C (a k))) * (∏ k, (X^2 + (b₁ k) • X + C (b₂ k)))) := by
  sorry

lemma quad_eq_of_not_real_of_finite_extension (z : F) (notinr : ∀ (r : ℝ), r•1 ≠ z) :
    ∃ (a b : ℝ), a ≠ 0 ∧ z^2 = a•1 + b•z := by
  let zs : Fin ((finrank ℝ F) + 1) → F := fun k ↦ z^k.toNat
  have lindep : ¬(LinearIndependent ℝ zs) := by
    have lt : (finrank ℝ F) < (finrank ℝ F) + 1 := by omega
    contrapose! lt
    convert lt.fintype_card_le_finrank
    simp
  obtain ⟨r, sumz, einz⟩ := Fintype.not_linearIndependent_iff.mp lindep
  let p : ℝ[X] := {
    toFinsupp := {
      support := (Finset.range ((finrank ℝ F) + 1)).filter (fun n ↦ r (Fin.ofNat _ n) ≠ 0)
      toFun := fun n ↦ if h : n < (finrank ℝ F) + 1 then r (Fin.mk n h) else 0
      mem_support_toFun := by
        intro n
        constructor
        . simp only [Fin.ofNat_eq_cast, ne_eq, Finset.mem_filter, Finset.mem_range,
            dite_eq_right_iff, not_forall, and_imp]
          intro lt rnz
          use lt
          convert rnz
          exact (Fin.val_cast_of_lt lt).symm
        . simp only [ne_eq, dite_eq_right_iff, not_forall, Fin.ofNat_eq_cast, Finset.mem_filter,
            Finset.mem_range, forall_exists_index]
          intro h rnz
          refine' ⟨h, _⟩
          convert rnz
          exact Fin.val_cast_of_lt h
    }
  }
  have pnz : p ≠ 0 := by
    apply Polynomial.support_eq_empty.mpr.mt
    obtain ⟨k, rknz⟩ := einz
    apply @Finset.ne_empty_of_mem _ k.toNat
    simp [p, rknz]
  have pz_zero : p.eval₂ RingHom.smulOneHom z = 0 := by
    rw [eval₂_def, sum_def]
    conv => lhs; arg 1; dsimp [p]
    simp only [support_ofFinsupp, Finset.sum_filter, ← Fin.sum_univ_eq_sum_range]
    convert sumz using 2 with n
    by_cases rnz : r n = 0
    . simp [rnz]
    . simp [rnz, p, zs, RingHom.smulOneHom]

  obtain ⟨n, m, a, b₁, b₂, _, b₂nz, p_fact⟩ := real_polynomial_factorization p
  rw [p_fact, eval₂_smul, eval₂_mul, mul_eq_zero, mul_eq_zero] at pz_zero
  rcases pz_zero with h | ⟨h | h⟩
  . simp [pnz] at h
  . rw [eval₂_finset_prod, Fin.prod_univ_def, List.prod_eq_zero_iff, List.mem_map] at h
    obtain ⟨k, _, eqz⟩ := h
    simp [RingHom.smulOneHom, sub_eq_zero, (notinr (a k)).symm] at eqz
  rw [eval₂_finset_prod, Fin.prod_univ_def, List.prod_eq_zero_iff, List.mem_map] at h
  obtain ⟨k, _, eqz⟩ := h
  refine' ⟨-(b₂ k), -(b₁ k), neg_eq_zero.mp.mt (b₂nz k), _⟩
  rw [← sub_eq_zero]
  simp_rw [sub_add_eq_sub_sub, sub_eq_add_neg, neg_smul, neg_neg]
  rw [add_assoc, add_comm (_ • 1), ← add_assoc]
  convert eqz
  simp [RingHom.smulOneHom]

private def two_dimensional_subfield {z : F} (notinr : ∀ (r : ℝ), r•1 ≠ z) : Subfield F :=
  ((Submodule.span ℝ ({1, z} : Set F)).toSubalgebra (by
    simp [Submodule.mem_span_of_mem]
  ) (by
    intro x y xIn yIn
    obtain ⟨a, b, anz, quad_eq⟩ := quad_eq_of_not_real_of_finite_extension F z notinr
    have eq_range : ({1, z} : Set F) = Set.range ![1, z] := by ext; simp; tauto
    rw [eq_range, Submodule.mem_span_range_iff_exists_fun] at xIn yIn ⊢
    obtain ⟨c, eqx⟩ := xIn
    obtain ⟨d, eqy⟩ := yIn
    simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.sum_univ_two, Fin.isValue,
      Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.cons_val_fin_one] at eqx eqy
    use ![(c 0)*(d 0)+(c 1)*(d 1)*a, (c 0)*(d 1)+(c 1)*(d 0)+(c 1)*(d 1)*b]
    simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, Fin.sum_univ_two,
      Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.cons_val_fin_one, ← eqx, ← eqy]
    simp_rw [mul_add, add_mul]
    conv => rhs; arg 2; arg 2; equals (c 1 * d 1)•(z*z) => simp [smul_smul, mul_comm]
    rw [← pow_two, quad_eq]
    simp_rw [smul_add, add_smul, smul_one_mul, mul_smul_one, smul_smul]
    ring_nf
  )).toSubring.toSubfield (by
    intro x xIn
    by_cases notinr : ∀ (r : ℝ), r•1 ≠ x
    . obtain ⟨a, b, anz, quad_eq⟩ := quad_eq_of_not_real_of_finite_extension F x notinr
      have inveq : x⁻¹ = a⁻¹•x-(a⁻¹*b)•1 := by
        apply inv_eq_of_mul_eq_one_left
        simp_rw [sub_mul, smul_mul_assoc, ← pow_two, quad_eq, smul_add, smul_smul,
          inv_mul_cancel₀ anz, one_mul, add_sub_cancel_right, one_smul]
      rw [inveq]
      apply Subring.sub_mem
      . rw [Subalgebra.mem_toSubring] at xIn ⊢
        apply Subalgebra.smul_mem
        exact xIn
      . rw [Subalgebra.mem_toSubring] at xIn ⊢
        apply Subalgebra.smul_mem
        have eq_range : ({1, z} : Set F) = Set.range ![1, z] := by ext; simp; tauto
        simp [Submodule.mem_span_of_mem]
    . have eq_range : ({1, z} : Set F) = Set.range ![1, z] := by ext; simp; tauto
      rw [Subalgebra.mem_toSubring, Submodule.mem_toSubalgebra,
          eq_range, Submodule.mem_span_range_iff_exists_fun]
      push_neg at notinr
      obtain ⟨a, eqx⟩ := notinr
      use ![a⁻¹, 0]
      simp [← eqx, smul_inv₀]
  )

I guess the lemma quad_eq_of_not_real_of_finite_extension shows that the minimal polynomial can't be greater than 2 (and if it's not in R, it can't be 0 or 1 either).

[Kenny Lau]

yeah, ∃ (a b : ℝ), a ≠ 0 ∧ z^2 = a•1 + b•z was missing from your original code

[Kenny Lau]

which is fine, we don't like partial functions

[Tainnor]

Sure. My question wasn't about how to prove this mathematically, I'm following a textbook proof. I'm more confused about the type system here. I guess I can use IntermediateField instead, but for didactic purposes I would like to construct this object from scratch without using more advanced field theory.

[Eric Wieser]

Probably a reasonable thing to do here is show that ℝ⟮z⟯.toSubmodule = Submodule.span ℝ ({1, z} : Set F) under suitable assumptions

[Kenny Lau]

Tainnor said:

Sure. My question wasn't about how to prove this mathematically, I'm following a textbook proof. I'm more confused about the type system here. I guess I can use IntermediateField instead, but for didactic purposes I would like to construct this object from scratch without using more advanced field theory.

I don't understand this distinction. So which part of Mathlib can you use and which part of Mathlib is "more advanced field theory"?

[Tainnor]

My goal is to reproduce my textbook's proofs in Lean for didactic purposes. The proof is my textbook is low undergraduate level and doesn't assume that people know about minimal polynomials and so on. It's fairly pedestrian in that it just directly shows that the subset {1,z} satisfies the field axioms.

[Tainnor]

I probably haven't explained myself clearly.

I already have the construction of {1, z} as a subfield of F (that's what I posted initially), i.e. I know how to prove it's a field.

What I'm looking for is a way to prove the following or similar:

// this actually works
example (notinr : ∀ (r : ℝ), r•1 ≠ z) : Field (two_dimensional_subfield F notinr) := inferInstance
// but no idea how to prove this
example (notinr : ∀ (r : ℝ), r•1 ≠ z) : Module ℝ (two_dimensional_subfield F notinr) := by
    // this doesn't help a lot
    simp [two_dimensional_subfield, Submodule.toSubalgebra, Subring.toSubfield, Subalgebra.toSubring]
    sorry
// even though this works
example : Module ℝ (Submodule.span ℝ ({1, z} : Set F)) :=
  inferInstance

In my intuitive (and probably wrong) understanding, I'm just attaching proof objects to Submodule.span .... So I should still somehow be able to recover the underlying module instance, for example. But I don't know how to do that.

Maybe the answer is that this isn't possible / convenient to do that in Lean and that I'm holding it wrong, but to me this is not clear.

[Eric Wieser]

I would guess that

example (notinr : ∀ (r : ℝ), r•1 ≠ z) : Module ℝ (two_dimensional_subfield F notinr) := by
  show Module ℝ (Submodule.span ℝ ({1, z} : Set F))
  infer_instance

works

[Tainnor]

oh. Yeah, it actually does. So they're actually defeq?

[Eric Wieser]

Yes, and this shouldn't be surprising as toSubalgebra etc are keeping the same data and swapping proofs around

[Tainnor]

Yeah that makes sense.

[Notification Bot]

Tainnor has marked this topic as resolved.

[Notification Bot]

Tainnor has marked this topic as unresolved.

[Tainnor]

Sorry, I was too quick. I got confused by VS Code's interface. It actually doesn't work, instead the show step runs forever and eventually runs out of heartbeats

[Kevin Buzzard]

Can you post a #mwe of your problem? I am failing to put it together from the code which has been posted here.

[Tainnor]

Sure:

import Mathlib

variable (F : Type*)
[Field F] [Algebra ℝ F] [Module.Finite ℝ F]

open Module FiniteDimensional LinearIndependent

open Polynomial

theorem real_polynomial_factorization (p : ℝ[X]) :
    ∃ (n m : ℕ) (a : Fin n → ℝ) (b₁ b₂ : Fin m → ℝ), p.natDegree = n+2*m
      ∧ (∀ k, b₂ k ≠ 0)
      ∧ p = p.leadingCoeff • ((∏ k, (X - C (a k))) * (∏ k, (X^2 + (b₁ k) • X + C (b₂ k)))) := by
  sorry

lemma quad_eq_of_not_real_of_finite_extension (z : F) (notinr : ∀ (r : ℝ), r•1 ≠ z) :
    ∃ (a b : ℝ), a ≠ 0 ∧ z^2 = a•1 + b•z := by
  let zs : Fin ((finrank ℝ F) + 1) → F := fun k ↦ z^k.toNat
  have lindep : ¬(LinearIndependent ℝ zs) := by
    have lt : (finrank ℝ F) < (finrank ℝ F) + 1 := by omega
    contrapose! lt
    convert lt.fintype_card_le_finrank
    simp
  obtain ⟨r, sumz, einz⟩ := Fintype.not_linearIndependent_iff.mp lindep
  let p : ℝ[X] := {
    toFinsupp := {
      support := (Finset.range ((finrank ℝ F) + 1)).filter (fun n ↦ r (Fin.ofNat _ n) ≠ 0)
      toFun := fun n ↦ if h : n < (finrank ℝ F) + 1 then r (Fin.mk n h) else 0
      mem_support_toFun := by
        intro n
        constructor
        . simp only [Fin.ofNat_eq_cast, ne_eq, Finset.mem_filter, Finset.mem_range,
            dite_eq_right_iff, not_forall, and_imp]
          intro lt rnz
          use lt
          convert rnz
          exact (Fin.val_cast_of_lt lt).symm
        . simp only [ne_eq, dite_eq_right_iff, not_forall, Fin.ofNat_eq_cast, Finset.mem_filter,
            Finset.mem_range, forall_exists_index]
          intro h rnz
          refine' ⟨h, _⟩
          convert rnz
          exact Fin.val_cast_of_lt h
    }
  }
  have pnz : p ≠ 0 := by
    apply Polynomial.support_eq_empty.mpr.mt
    obtain ⟨k, rknz⟩ := einz
    apply @Finset.ne_empty_of_mem _ k.toNat
    simp [p, rknz]
  have pz_zero : p.eval₂ RingHom.smulOneHom z = 0 := by
    rw [eval₂_def, sum_def]
    conv => lhs; arg 1; dsimp [p]
    simp only [support_ofFinsupp, Finset.sum_filter, ← Fin.sum_univ_eq_sum_range]
    convert sumz using 2 with n
    by_cases rnz : r n = 0
    . simp [rnz]
    . simp [rnz, p, zs, RingHom.smulOneHom]

  obtain ⟨n, m, a, b₁, b₂, _, b₂nz, p_fact⟩ := real_polynomial_factorization p
  rw [p_fact, eval₂_smul, eval₂_mul, mul_eq_zero, mul_eq_zero] at pz_zero
  rcases pz_zero with h | ⟨h | h⟩
  . simp [pnz] at h
  . rw [eval₂_finset_prod, Fin.prod_univ_def, List.prod_eq_zero_iff, List.mem_map] at h
    obtain ⟨k, _, eqz⟩ := h
    simp [RingHom.smulOneHom, sub_eq_zero, (notinr (a k)).symm] at eqz
  rw [eval₂_finset_prod, Fin.prod_univ_def, List.prod_eq_zero_iff, List.mem_map] at h
  obtain ⟨k, _, eqz⟩ := h
  refine' ⟨-(b₂ k), -(b₁ k), neg_eq_zero.mp.mt (b₂nz k), _⟩
  rw [← sub_eq_zero]
  simp_rw [sub_add_eq_sub_sub, sub_eq_add_neg, neg_smul, neg_neg]
  rw [add_assoc, add_comm (_ • 1), ← add_assoc]
  convert eqz
  simp [RingHom.smulOneHom]

private def two_dimensional_subfield {z : F} (notinr : ∀ (r : ℝ), r•1 ≠ z) : Subfield F :=
  ((Submodule.span ℝ ({1, z} : Set F)).toSubalgebra (by
    simp [Submodule.mem_span_of_mem]
  ) (by
    intro x y xIn yIn
    obtain ⟨a, b, anz, quad_eq⟩ := quad_eq_of_not_real_of_finite_extension F z notinr
    have eq_range : ({1, z} : Set F) = Set.range ![1, z] := by ext; simp; tauto
    rw [eq_range, Submodule.mem_span_range_iff_exists_fun] at xIn yIn ⊢
    obtain ⟨c, eqx⟩ := xIn
    obtain ⟨d, eqy⟩ := yIn
    simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.sum_univ_two, Fin.isValue,
      Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.cons_val_fin_one] at eqx eqy
    use ![(c 0)*(d 0)+(c 1)*(d 1)*a, (c 0)*(d 1)+(c 1)*(d 0)+(c 1)*(d 1)*b]
    simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, Fin.sum_univ_two,
      Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.cons_val_fin_one, ← eqx, ← eqy]
    simp_rw [mul_add, add_mul]
    conv => rhs; arg 2; arg 2; equals (c 1 * d 1)•(z*z) => simp [smul_smul, mul_comm]
    rw [← pow_two, quad_eq]
    simp_rw [smul_add, add_smul, smul_one_mul, mul_smul_one, smul_smul]
    ring_nf
  )).toSubring.toSubfield (by
    intro x xIn
    by_cases notinr : ∀ (r : ℝ), r•1 ≠ x
    . obtain ⟨a, b, anz, quad_eq⟩ := quad_eq_of_not_real_of_finite_extension F x notinr
      have inveq : x⁻¹ = a⁻¹•x-(a⁻¹*b)•1 := by
        apply inv_eq_of_mul_eq_one_left
        simp_rw [sub_mul, smul_mul_assoc, ← pow_two, quad_eq, smul_add, smul_smul,
          inv_mul_cancel₀ anz, one_mul, add_sub_cancel_right, one_smul]
      rw [inveq]
      apply Subring.sub_mem
      . rw [Subalgebra.mem_toSubring] at xIn ⊢
        apply Subalgebra.smul_mem
        exact xIn
      . rw [Subalgebra.mem_toSubring] at xIn ⊢
        apply Subalgebra.smul_mem
        have eq_range : ({1, z} : Set F) = Set.range ![1, z] := by ext; simp; tauto
        simp [Submodule.mem_span_of_mem]
    . have eq_range : ({1, z} : Set F) = Set.range ![1, z] := by ext; simp; tauto
      rw [Subalgebra.mem_toSubring, Submodule.mem_toSubalgebra,
          eq_range, Submodule.mem_span_range_iff_exists_fun]
      push_neg at notinr
      obtain ⟨a, eqx⟩ := notinr
      use ![a⁻¹, 0]
      simp [← eqx, smul_inv₀]
  )

-- this times out
lemma two_dim_subfield_module {z : F} (notinr : ∀ (r : ℝ), r•1 ≠ z) :
    Module ℝ (two_dimensional_subfield F znotinr) := by
  show Module ℝ (Submodule.span ℝ ({1, z} : Set F))
  infer_instance

[Kenny Lau]

@Tainnor basically subring and subfield are evil because they forget the R, which is why we've been telling you to use IntermediateField instead

[Tainnor]

good to know! so these structures should be avoided?

[Kenny Lau]

Tainnor said:

I already have the construction of {1, z} as a subfield of F

You might be a bit overconfident here. Translating Maths statements (and constructions) into Lean is an art and there is often more than one way to do it. I think my point here is that your construction is not the only one (and might not be the best one)

[Kenny Lau]

Tainnor said:

good to know! so these structures should be avoided?

Correct, you should always use Subalgebra and IntermediateField

[Kenny Lau]

mostly because there are a lot of other Subrings and Subfields that you don't really want

[Kenny Lau]

for example, Q[e] is a subring of F

[Kevin Buzzard]

@Tainnor you say "this times out" in your code but if you set_option autoImplicit false then you get an error about an unknown variable. Are you sure your code is typo-free?

[Kevin Buzzard]

Autoimplicits turn typos into timeouts. Things are much better now though with the new warning system:

Screenshot from 2025-07-02 00-07-33.png

The grey {znotinr} means "I have no idea what this is so I just made something up which had the right type"

[Tainnor]

Kevin Buzzard said:

Tainnor you say "this times out" in your code but if you set_option autoImplicit false then you get an error about an unknown variable. Are you sure your code is typo-free?

Oh yeah, good point I had a typo

[Tainnor]

If I fix it, I get "type of theorem ... is not a proposition"

[Tainnor]

I feel like I'm really fundamentally misunderstanding something about the type system

[Kevin Buzzard]

I have set_option autoImplicit false on in FLT because for me the benefits of being informed about typos far outweigh the advantages of being able to concoct an arbitrary term of a given type

[Kevin Buzzard]

Module ℝ (two_dimensional_subfield F znotinr) is not a theorem. It is the structure of a real vector space on the type (two_dimensional_subfield F znotinr) so in particular it can be completely unrelated to any addition or scalar multiplication which already exist on this type.

[Kevin Buzzard]

Why are you making two_dimensional_subfield a Subfield and not an IntermediateField? This would presumably do the thing which you actually wanted to do with your module "theorem".

[Kevin Buzzard]

The extra theorem which Lean will make you prove with IntermediateField is precisely the thing which you are trying to "prove" with this incorrect Module definition.

[Tainnor]

Kevin Buzzard said:

Why are you making two_dimensional_subfield a Subfield and not an IntermediateField? this would presumably do the thing which you actually wanted to do with your module "theorem".

Because I didn't know about that. And I often have a hard time figure out what the right structures / classes to use are. I'm fine with switching to IntermediateField, if that's better (although I don't yet understand why this is the case), but I would like to be able to supply my own proof that the thing in question is actually a field, since I'm doing this for didactic purposes and following a textbook proof (i.e. using a lemma about quadratic polynomials would defeat the purpose for me).

[Tainnor]

Kevin Buzzard said:

Module ℝ (two_dimensional_subfield F znotinr) is not a theorem. It is the structure of a real vector space on the type (two_dimensional_subfield F znotinr) so in particular it can be completely unrelated to any addition or scalar multiplication which already exist on this type.

This makes sense. What I'm trying to do is to manually provide an instance. If I change it from a lemma to an example it works btw. I always thought examples are just unnamed theorems, but I guess I was wrong :sweat_smile:

[Tainnor]

I mean maybe that's bad and one shouldn't manually provide an instance.

[Kevin Buzzard]

Lean's typeclass set-up (Group, Ring etc) is done in such a way that all these things are data, so you can't "prove" them. For example I can easily make a term of type Field Nat by just supplying different addition and multiplication to the standard ones, e.g. by bijecting Nat with an alg closure of Z/2Z. A consequence of this set-up is that it's actually quite hard to start with a monoid G, do some stuff, prove that an inverse of every element exists and then prove the "theorem" that G is a group, because Group G means "you can now totally override multiplication". When I learnt about Lean I thought that this was kind of a disaster, because I imagined that all of the time we would be doing things like "here is a group G, here is a random subset S, now I do loads of maths, and deduce that S is a subgroup". But I was wrong, and in the few cases when we do want to do things like this, there is typically a workaround.

[Kevin Buzzard]

The typeclass system is incredibly fragile, it's very easy to create so-called "diamonds" if you don't use it correctly and these turn into very obscure errors.

[Kenny Lau]

Tainnor said:

I would like to be able to supply my own proof that the thing in question is actually a field

That's what I was referring to when I said that there are multiple ways to translate something.

When mathematicians say "is a field", they mean something that doesn't really have a direct translation to Lean, because in Lean every time you write down an expression, the type has to already have been specified.

So, there would be two different approaches here (and the second one is better):

1. You would form the object Submodule.span \R {1, z} : Submodule \R F, and transport it all the way to an object of type Intermediate \R F (read this very carefully, and make sure that you understand which one is the "term" and which one is the "type". If you don't know what term and type mean, ask.)
2. You would directly form the object IntermediateField.adjoin \R z : IntermediateField \R F, and prove that the underlying set / R-submodule is actually the thing you want

Make sure you understand what these two approaches are. Make sure very carefully that you understand the mathematical content behind both approaches.

[Tainnor]

Kevin Buzzard said:

Lean's typeclass set-up (Group, Ring etc) is done in such a way that all these things are data, so you can't "prove" them. For example I can easily make a term of type Field Nat by just supplying different addition and multiplication to the standard ones, e.g. by bijecting Nat with an alg closure of Z/2Z. A consequence of this set-up is that it's actually quite hard to start with a monoid G, do some stuff, prove that an inverse of every element exists and then prove the "theorem" that G is a group, because Group G means "you can now totally override multiplication". When I learnt about Lean I thought that this was kind of a disaster, because I imagined that all of the time we would be doing things like "here is a group G, here is a random subset S, now I do loads of maths, and deduce that S is a subgroup". But I was wrong, and in the few cases when we do want to do things like this, there is typically a workaround.

thanks for the patient explanation. Yes, this is indeed how I would intuitively approach this. What are these workarounds that you mention if you don't mind me asking?

[Kevin Buzzard]

def two_dimensional_subfield {z : F} (notinr : ∀ (r : ℝ), r•1 ≠ z) :
    IntermediateField ℝ F where
  carrier := (Submodule.span ℝ ({1, z} : Set F))
  mul_mem' := sorry
  add_mem' hx hy := add_mem hx hy
  algebraMap_mem' r := sorry
  inv_mem' := sorry

variable (z : F) (notinr : ∀ (r : ℝ), r•1 ≠ z) in
#synth Module ℝ (two_dimensional_subfield F notinr) -- now the system knows it's an ℝ-module automatically

[Kenny Lau]

Kevin Buzzard said:

by bijecting Nat with an alg closure of Z/2Z

I like how you chose that over Q :rofl:

[Tainnor]

Kevin Buzzard said:

def two_dimensional_subfield {z : F} (notinr : ∀ (r : ℝ), r•1 ≠ z) :
    IntermediateField ℝ F where
  carrier := (Submodule.span ℝ ({1, z} : Set F))
  mul_mem' := sorry
  add_mem' hx hy := add_mem hx hy
  algebraMap_mem' r := sorry
  inv_mem' := sorry

Yes, or actually this which is almost identical to my original, except it's not using the "evil" subring and subfield:

private def two_dimensional_subfield {z : F} (notinr : ∀ (r : ℝ), r•1 ≠ z) : IntermediateField ℝ F :=
  ((Submodule.span ℝ ({1, z} : Set F)).toSubalgebra (by
    simp [Submodule.mem_span_of_mem]
  ) (by
    intro x y xIn yIn
    obtain ⟨a, b, anz, quad_eq⟩ := quad_eq_of_not_real_of_finite_extension F z notinr
    have eq_range : ({1, z} : Set F) = Set.range ![1, z] := by ext; simp; tauto
    rw [eq_range, Submodule.mem_span_range_iff_exists_fun] at xIn yIn ⊢
    obtain ⟨c, eqx⟩ := xIn
    obtain ⟨d, eqy⟩ := yIn
    simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.sum_univ_two, Fin.isValue,
      Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.cons_val_fin_one] at eqx eqy
    use ![(c 0)*(d 0)+(c 1)*(d 1)*a, (c 0)*(d 1)+(c 1)*(d 0)+(c 1)*(d 1)*b]
    simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, Fin.sum_univ_two,
      Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.cons_val_fin_one, ← eqx, ← eqy]
    simp_rw [mul_add, add_mul]
    conv => rhs; arg 2; arg 2; equals (c 1 * d 1)•(z*z) => simp [smul_smul, mul_comm]
    rw [← pow_two, quad_eq]
    simp_rw [smul_add, add_smul, smul_one_mul, mul_smul_one, smul_smul]
    ring_nf
  )).toIntermediateField (by
    intro x xIn
    by_cases notinr : ∀ (r : ℝ), r•1 ≠ x
    . obtain ⟨a, b, anz, quad_eq⟩ := quad_eq_of_not_real_of_finite_extension F x notinr
      have inveq : x⁻¹ = a⁻¹•x-(a⁻¹*b)•1 := by
        apply inv_eq_of_mul_eq_one_left
        simp_rw [sub_mul, smul_mul_assoc, ← pow_two, quad_eq, smul_add, smul_smul,
          inv_mul_cancel₀ anz, one_mul, add_sub_cancel_right, one_smul]
      rw [inveq]
      apply Subalgebra.sub_mem
      . apply Subalgebra.smul_mem
        exact xIn
      . apply Subalgebra.smul_mem
        have eq_range : ({1, z} : Set F) = Set.range ![1, z] := by ext; simp; tauto
        simp [Submodule.mem_span_of_mem]
    . have eq_range : ({1, z} : Set F) = Set.range ![1, z] := by ext; simp; tauto
      rw [Submodule.mem_toSubalgebra, eq_range, Submodule.mem_span_range_iff_exists_fun]
      push_neg at notinr
      obtain ⟨a, eqx⟩ := notinr
      use ![a⁻¹, 0]
      simp [← eqx, smul_inv₀]
  )

[Kenny Lau]

@Tainnor And try to understand very carefully that the code Kevin Buzzard just provided is using the first approach I mentioned.

[Kevin Buzzard]

sure this is close to what you were doing, but my way is a bit more readable and has the advantage that typeclass inference now finds the module instance automatically (I just edited my code to demonstrate this)

[Kenny Lau]

(For the sake of clarity, which I agree might be a bit too much for now and doesn't really matter, just my force of habit, that the two by blocks should really have been factored out as separate lemmas, for readability.)

[Kevin Buzzard]

yeah Lean prefers lots of small proofs of different lemmas to one big proof

[Tainnor]

Kevin Buzzard said:

yeah Lean prefers lots of small proofs of different lemmas to one big proof

I've already noticed this. I have files that take very long to compile because of this. The problem is that it's often deep within the proof of something that I realise I need auxiliary lemmas and then it's a lot of manual work to transport all the necessary preconditions (I wish there was some "extract lemma" like in many other programming languages, or maybe there is and I missed it).

[Tainnor]

Kevin Buzzard said:

sure this is close to what you were doing, but my way is a bit more readable and has the advantage that typeclass inference now finds the module instance automatically (I just edited my code to demonstrate this)

That's a good point. I don't really have any good insight in how the type inference mechanism works and why certain things are more easily auto-discoverable

[Kenny Lau]

Kenny Lau said:

yeah, ∃ (a b : ℝ), a ≠ 0 ∧ z^2 = a•1 + b•z was missing from your original code

Aha I finally understand what went wrong here, I forgot that \R means the reals and the only non-trivial algebraic extension is \C :rofl:

[Tainnor]

Yes, that's the exact proof I'm working towards

[Tainnor]

Only took me translating about 2/3s of a semester of an undergraduate complex analysis course to get there :sweat_smile:

[Kevin Buzzard]

Tainnor said:

(I wish there was some "extract lemma" like in many other programming languages, or maybe there is and I missed it).

This is probably extract_goal.

[Kenny Lau]

import Mathlib

variable (F : Type*) [Field F] [Algebra ℝ F] [Module.Finite ℝ F]

def rankTwo {z : F} (notinr : ∀ (r : ℝ), r•1 ≠ z) : IntermediateField ℝ F where
  mul_mem' := sorry
  algebraMap_mem' r := sorry
  inv_mem' := sorry
  __ := Submodule.span ℝ {1, z}

I take back my statement above saying that approach 2 is better, because approach 1 also has its merits here; in any case here is another way to do approach 1 from which you can derive add_mem automatically

[Tainnor]

Kevin Buzzard said:

Tainnor said:

(I wish there was some "extract lemma" like in many other programming languages, or maybe there is and I missed it).

This is probably extract_goal.

good to know

[Tainnor]

Kenny Lau said:

import Mathlib

variable (F : Type*) [Field F] [Algebra ℝ F] [Module.Finite ℝ F]

def rankTwo {z : F} (notinr : ∀ (r : ℝ), r•1 ≠ z) : IntermediateField ℝ F where
  mul_mem' := sorry
  algebraMap_mem' r := sorry
  inv_mem' := sorry
  __ := Submodule.span ℝ {1, z}

I take back my statement above saying that approach 2 is better, because approach 1 also has its merits here; in any case here is another way to do approach 1 from which you can derive add_mem automatically

oh! what is this __ doing?

[Kenny Lau]

It means "copy as many fields of this structure as possible"

[Tainnor]

that's good to know

[Kenny Lau]

for example, if you have a type S and you already have an instance of AddCommGroup S (i.e. "S is an abelian group under addition"), and you want to make an instance of Ring S (i.e. "S is a ring"), then you can use this trick to reduce the number of goals

[Tainnor]

very helpful