IntermediateField mem_adjoin_of_mem

Stream: mathlib4

[Dion Leijnse]

Currently, mathlib contains the statement Algebra.mem_adjoin_of_mem, which says that x ∈ adjoin R s if x ∈ s for a subset s of an R-algebra A. There does not seem to be an analogous statement for the similar setting of Intermediate Fields. The proof there is not hard, but would it make sense to add this as an API lemma (and possibly tag it with aesop as done for Algebra.mem_adjoin_of_mem)? At least it would make some of my proofs a bit cleaner.

import Mathlib

example (k K : Type) [CommRing k] [Ring K] [Algebra k K] {S : Set K} {x : K} (h : x ∈ S) :
    x ∈ Algebra.adjoin k S :=
  Algebra.mem_adjoin_of_mem h

lemma IntermediateField.mem_adjoin_of_mem (k K : Type) [Field k] [Field K] [Algebra k K] {S : Set K} {x : K} (h : x ∈ S) :
    x ∈ IntermediateField.adjoin k S :=
  IntermediateField.algebra_adjoin_le_adjoin k S <| Algebra.mem_adjoin_of_mem h

[Andrew Yang]

This is docs#IntermediateField.subset_adjoin

[Andrew Yang]

Although arguably we could add an applied version for discoverability.

[Dion Leijnse]

Thanks, that also works. But I do agree that maybe adding the result for discoverability could help (at least then I could have found it with exact?).

[Artie Khovanov]

I added all these mem_adjoin_of_mem lemmas for the purpose of making aesop more efficient. Please feel free to add missing ones, and please aesop tag them the same way.

More generally I am working on a refactor to unify all substructure closure operators. Once that is merged, all of these operations will have the same API.

[Artie Khovanov]

#25963 - uniform API for substructures

[Dion Leijnse]

I'm making a PR for this now, but I see that Algebra.subset_adjoin has the tag @[simp, aesop safe 20 (rule_sets := [SetLike])] which IntermediateField.subset_adjoin does not have. Do you think it's worth adding this also to IntermediateField.subset_adjoin?

[Artie Khovanov]

Dion Leijnse said:

I'm making a PR for this now, but I see that Algebra.subset_adjoin has the tag @[simp, aesop safe 20 (rule_sets := [SetLike])] which IntermediateField.subset_adjoin does not have. Do you think it's worth adding this also to IntermediateField.subset_adjoin?

Yeah, please make the APIs consistent if able. If you look at eg Subgroup.closure or Subring.closure you'll see they have the same theorems and attributes.

[Dion Leijnse]

I've made a PR for this: #33122