Extending intermediate fields to a larger extension

Given a tower of field extensions K ⊆ L ⊆ M and an intermediate field F of L/K, this file defines IntermediateField.extendRight F M, the image of F under the inclusion L ⊆ M, as an intermediate field of M/K. It is canonically isomorphic to F as a K-algebra.

The main motivation is to embed a subextension F/K of L/K into a larger extension M/K. This is useful for instance when one needs M/K to be Galois.

Main definitions

• IntermediateField.extendRight F M: the intermediate field of M/K defined as the image of F under the map L →ₐ[K] M.
• IntermediateField.extendRightEquiv F M: the K-algebra isomorphism F ≃ₐ[K] extendRight F M.

Main instances

• IntermediateField.extendRight.algebra: for S with Algebra S F, S acts on extendRight F M.
• IntermediateField.extendRight.isFractionRing: transfers the IsFractionRing S F instance.
• IntermediateField.extendRight.isIntegralClosure: transfers the IsIntegralClosure S R F instance.

def IntermediateField.extendRight {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (F : IntermediateField K L) (M : Type u_3) [Field M] [Algebra K M] [Algebra L M] [IsScalarTower K L M] : IntermediateField K M

The image of the intermediate field F of L/K under the inclusion L ⊆ M, viewed as an intermediate field of M/K.

Equations

• F.extendRight M = IntermediateField.map (Algebra.algHom K L M) F

noncomputable def IntermediateField.extendRightEquiv {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (F : IntermediateField K L) (M : Type u_3) [Field M] [Algebra K M] [Algebra L M] [IsScalarTower K L M] : ↥F ≃ₐ[K] ↥(F.extendRight M)

The isomorphism between F and its image F.extendRight M in M.

Equations

• F.extendRightEquiv M = F.equivMap (Algebra.algHom K L M)

@[simp]

theorem IntermediateField.algebraMap_extendRightEquiv {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (F : IntermediateField K L) (M : Type u_3) [Field M] [Algebra K M] [Algebra L M] [IsScalarTower K L M] (a : ↥F) : (algebraMap (↥(F.extendRight M)) M) ((F.extendRightEquiv M) a) = (algebraMap (↥F) M) a

@[simp]

theorem IntermediateField.coe_extendRightEquiv {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (F : IntermediateField K L) (M : Type u_3) [Field M] [Algebra K M] [Algebra L M] [IsScalarTower K L M] (a : ↥F) : ↑((F.extendRightEquiv M) a) = (algebraMap (↥F) M) a

@[simp]

theorem IntermediateField.algebraMap_extendRightEquiv_symm {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (F : IntermediateField K L) (M : Type u_3) [Field M] [Algebra K M] [Algebra L M] [IsScalarTower K L M] (a : ↥(F.extendRight M)) : (algebraMap (↥F) M) ((F.extendRightEquiv M).symm a) = ↑a

theorem IntermediateField.extendRight.algebraMap_mem {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (F : IntermediateField K L) (M : Type u_3) [Field M] [Algebra K M] [Algebra L M] [IsScalarTower K L M] {S : Type u_5} [CommRing S] [Algebra S ↥F] [Algebra S M] [IsScalarTower S (↥F) M] (s : S) : (algebraMap S M) s ∈ F.extendRight M

@[implicit_reducible]

instance IntermediateField.extendRight.instSMulSubtypeMem {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (F : IntermediateField K L) (M : Type u_3) [Field M] [Algebra K M] [Algebra L M] [IsScalarTower K L M] {S : Type u_5} [CommRing S] [Algebra S ↥F] [Algebra S M] [IsScalarTower S (↥F) M] : SMul S ↥(F.extendRight M)

Equations

• IntermediateField.extendRight.instSMulSubtypeMem F M = { smul := fun (s : S) (x : ↥(F.extendRight M)) => ⟨s • ↑x, ⋯⟩ }

@[simp]

theorem IntermediateField.extendRight.coe_smul {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (F : IntermediateField K L) (M : Type u_3) [Field M] [Algebra K M] [Algebra L M] [IsScalarTower K L M] {S : Type u_5} [CommRing S] [Algebra S ↥F] [Algebra S M] [IsScalarTower S (↥F) M] (s : S) (x : ↥(F.extendRight M)) : ↑(s • x) = s • ↑x

@[implicit_reducible]

noncomputable instance IntermediateField.extendRight.algebra {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (F : IntermediateField K L) (M : Type u_3) [Field M] [Algebra K M] [Algebra L M] [IsScalarTower K L M] {S : Type u_5} [CommRing S] [Algebra S ↥F] [Algebra S M] [IsScalarTower S (↥F) M] : Algebra S ↥(F.extendRight M)

Equations

• One or more equations did not get rendered due to their size.

instance IntermediateField.extendRight.instIsScalarTowerSubtypeMem {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (F : IntermediateField K L) (M : Type u_3) [Field M] [Algebra K M] [Algebra L M] [IsScalarTower K L M] {S : Type u_5} [CommRing S] [Algebra S ↥F] [Algebra S M] [IsScalarTower S (↥F) M] : IsScalarTower S (↥(F.extendRight M)) M

instance IntermediateField.extendRight.instIsScalarTowerSubtypeMem_1 {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (F : IntermediateField K L) (M : Type u_3) [Field M] [Algebra K M] [Algebra L M] [IsScalarTower K L M] {S : Type u_5} [CommRing S] [Algebra S ↥F] [Algebra S M] [IsScalarTower S (↥F) M] : IsScalarTower S ↥F ↥(F.extendRight M)

instance IntermediateField.extendRight.instIsScalarTowerSubtypeMem_2 {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (F : IntermediateField K L) (M : Type u_3) [Field M] [Algebra K M] [Algebra L M] [IsScalarTower K L M] {R : Type u_4} {S : Type u_5} [CommRing R] [CommRing S] [Algebra S ↥F] [Algebra S M] [IsScalarTower S (↥F) M] [Algebra R S] [Algebra R ↥F] [Algebra R M] [IsScalarTower R (↥F) M] [IsScalarTower R S M] : IsScalarTower R S ↥(F.extendRight M)

noncomputable def IntermediateField.extendRightEquiv' {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (F : IntermediateField K L) (M : Type u_3) [Field M] [Algebra K M] [Algebra L M] [IsScalarTower K L M] (S : Type u_5) [CommRing S] [Algebra S ↥F] [Algebra S M] [IsScalarTower S (↥F) M] : ↥F ≃ₐ[S] ↥(F.extendRight M)

Variant of extendRightEquiv giving an S-algebra isomorphism F ≃ₐ[S] F.extendRight M, for a commutative ring S with Algebra S F.

Equations

• F.extendRightEquiv' M S = AlgEquiv.ofBijective (Algebra.algHom S ↥F ↥(F.extendRight M)) ⋯

@[simp]

theorem IntermediateField.extendRight.coe_extendRightEquiv' {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (F : IntermediateField K L) (M : Type u_3) [Field M] [Algebra K M] [Algebra L M] [IsScalarTower K L M] (S : Type u_5) [CommRing S] [Algebra S ↥F] [Algebra S M] [IsScalarTower S (↥F) M] (a : ↥F) : ↑((F.extendRightEquiv' M S) a) = (algebraMap (↥F) M) a

@[simp]

theorem IntermediateField.extendRight.algebraMap_extendRightEquiv' {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (F : IntermediateField K L) (M : Type u_3) [Field M] [Algebra K M] [Algebra L M] [IsScalarTower K L M] (S : Type u_5) [CommRing S] [Algebra S ↥F] [Algebra S M] [IsScalarTower S (↥F) M] (a : ↥F) : (algebraMap (↥(F.extendRight M)) M) ((F.extendRightEquiv' M S) a) = (algebraMap (↥F) M) a

@[simp]

theorem IntermediateField.extendRight.algebraMap_extendRightEquiv'_symm {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (F : IntermediateField K L) (M : Type u_3) [Field M] [Algebra K M] [Algebra L M] [IsScalarTower K L M] (S : Type u_5) [CommRing S] [Algebra S ↥F] [Algebra S M] [IsScalarTower S (↥F) M] (a : ↥(F.extendRight M)) : (algebraMap (↥F) M) ((F.extendRightEquiv' M S).symm a) = ↑a

instance IntermediateField.extendRight.isFractionRing {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (F : IntermediateField K L) (M : Type u_3) [Field M] [Algebra K M] [Algebra L M] [IsScalarTower K L M] {S : Type u_5} [CommRing S] [Algebra S ↥F] [Algebra S M] [IsScalarTower S (↥F) M] [IsFractionRing S ↥F] : IsFractionRing S ↥(F.extendRight M)

instance IntermediateField.extendRight.isIntegralClosure {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (F : IntermediateField K L) (M : Type u_3) [Field M] [Algebra K M] [Algebra L M] [IsScalarTower K L M] {R : Type u_4} {S : Type u_5} [CommRing R] [CommRing S] [Algebra S ↥F] [Algebra S M] [IsScalarTower S (↥F) M] [Algebra R ↥F] [Algebra R M] [IsScalarTower R (↥F) M] [IsIntegralClosure S R ↥F] : IsIntegralClosure S R ↥(F.extendRight M)