IntermediateField.sup_toSubfield

Stream: Is there code for X?

[Jz Pan]

We only have docs#IntermediateField.inf_toSubfield. Is IntermediateField.sup_toSubfield correct? I tried and found that rfl can't prove it. Perhaps some arguments are needed.

[Thomas Browning]

Does it follow from some combination of le_antisymm and sup_le_iff?

[Jz Pan]

Thomas Browning said:

Does it follow from some combination of le_antisymm and sup_le_iff?

I think this approach is a little bit complicated since it needs to use docs#Subfield.toIntermediateField and some others...

[Jz Pan]

This works:

import Mathlib.FieldTheory.Adjoin

namespace IntermediateField

@[simp]
theorem sup_toSubfield {F E : Type*} [Field F] [Field E] [Algebra F E] (S T : IntermediateField F E) :
    (S ⊔ T).toSubfield = S.toSubfield ⊔ T.toSubfield := by
  rw [← S.toSubfield.closure_eq, ← T.toSubfield.closure_eq, ← Subfield.closure_union]
  change Subfield.closure (Set.range (algebraMap F E) ∪ (S ∪ T)) = Subfield.closure (S ∪ T)
  congr 1
  rw [Set.union_eq_right]
  rintro _ ⟨x, rfl⟩
  exact Or.inl (algebraMap_mem S x)

[Jz Pan]

PR created as #15088.

[Eric Wieser]

Arguably we should redefine sup in the complete lattice instance above to make this true by definition

[Jz Pan]

Eric Wieser said:

Arguably we should redefine sup in the complete lattice instance above to make this true by definition

I don't know how to do that. Besides, IntermediateField.sSup_toSubfield and IntermediateField.iSup_toSubfield requires that the set in question is not empty, otherwise they are not equal. So I'm afraid that the lattice structure is different.

[Eric Wieser]

You can see how it's done for bot a few lines above. I suggest you only change sup, not sSup.

[Jz Pan]

Eric Wieser said:

You can see how it's done for bot a few lines above. I suggest you only change sup, not sSup.

Do you mean this:

instance : CompleteLattice (IntermediateField F E) where
  __ := GaloisInsertion.liftCompleteLattice IntermediateField.gi
  bot :=
    { toSubalgebra := ⊥
      inv_mem' := by rintro x ⟨r, rfl⟩; exact ⟨r⁻¹, map_inv₀ _ _⟩ }
  bot_le x := (bot_le : ⊥ ≤ x.toSubalgebra)
  sup S T := (S.toSubfield ⊔ T.toSubfield).toIntermediateField fun x ↦ by
    have : S.toSubfield ≤ S.toSubfield ⊔ T.toSubfield := le_sup_left
    exact this (algebraMap_mem S x)
  le_sup_left S T := by
    sorry
  le_sup_right S T := by
    sorry
  sup_le a b c := by
    sorry

Unfortunately, it breaks a lot of existing code relying on the old definition of sup :(

[Eric Wieser]

Ah sorry, I got confused between toSubfield and toSubalgebra. Maybe my suggestion isn't worthwhile after all, and certainly your PR is an improvement over the status quo

[Jz Pan]

Probably Subalgebra->Subring->Subsemiring version should also be added...

[Jz Pan]

ping What's the progress on reviewing #15088?

[Jz Pan]

ping I got some reviews last week, but there are 3 opening conversations I'm not intended to fix. Any other comments?