Membership and order for IntermediateField.extendRight

For a tower K ⊆ L ⊆ M, IntermediateField.extendRight F M is the copy of an intermediate field F of L / K inside M. Mathlib defines it and transfers algebra structure along it, but records nothing about how it sits in the order on intermediate fields of M / K. This file adds that, together with the universal property of the copy of a simple extension K⟮g⟯: it is the smallest intermediate field of M / K containing the image of g.

Main results

• IntermediateField.extendRight_eq_map: the copy, as an IntermediateField.map.
• IntermediateField.extendRight_le_iff: the copy of F lies below an intermediate field exactly when that field contains every image from F.
• IntermediateField.extendRight_adjoin_simple_le_iff: the copy of K⟮g⟯ lies inside an intermediate field exactly when that field contains the image of g.

theorem IntermediateField.extendRight_eq_map {K : Type u_1} {L : Type u_2} {M : Type u_3} [Field K] [Field L] [Field M] [Algebra K L] [Algebra K M] [Algebra L M] [IsScalarTower K L M] (F : IntermediateField K L) : F.extendRight M = map (IsScalarTower.toAlgHom K L M) F

F.extendRight M as an IntermediateField.map, spelled with IsScalarTower.toAlgHom.

theorem IntermediateField.extendRight_le_iff {K : Type u_1} {L : Type u_2} {M : Type u_3} [Field K] [Field L] [Field M] [Algebra K L] [Algebra K M] [Algebra L M] [IsScalarTower K L M] {F : IntermediateField K L} {E : IntermediateField K M} : F.extendRight M ≤ E ↔ ∀ x ∈ F, (algebraMap L M) x ∈ E

The copy of F is below an intermediate field exactly when that field contains every image from F. This decides an inclusion pointwise, with no comap.

theorem IntermediateField.extendRight_adjoin_le_iff {K : Type u_1} {L : Type u_2} {M : Type u_3} [Field K] [Field L] [Field M] [Algebra K L] [Algebra K M] [Algebra L M] [IsScalarTower K L M] {s : Set L} {E : IntermediateField K M} : (adjoin K s).extendRight M ≤ E ↔ ∀ x ∈ s, (algebraMap L M) x ∈ E

The universal property of the copy of an adjoin: the copy of K⟮s⟯ inside M lies in an intermediate field exactly when that field contains the image of every element of s.

@[simp]

theorem IntermediateField.extendRight_adjoin_simple_le_iff {K : Type u_1} {L : Type u_2} {M : Type u_3} [Field K] [Field L] [Field M] [Algebra K L] [Algebra K M] [Algebra L M] [IsScalarTower K L M] {g : L} {E : IntermediateField K M} : K⟮g⟯.extendRight M ≤ E ↔ (algebraMap L M) g ∈ E

The universal property of the copy of a simple extension: the copy of K⟮g⟯ inside M lies in an intermediate field exactly when that field contains the image of g.