A common overfield of two field extensions

Two extensions K / k and L / k embed into a common overfield: take a residue field of a maximal ideal of K ⊗[k] L. This file records that construction together with the comparison between successive and direct scalar extension, and the injective map induced by either field embedding.

Main declarations

• TauCeti.Algebra.TensorProduct.commonOverfield: constructs a common overfield of two field extensions.
• TauCeti.Algebra.TensorProduct.CommonOverfield.comparison: compares scalar extension through the first field with direct scalar extension to the common overfield.
• TauCeti.Algebra.TensorProduct.CommonOverfield.map: extends scalars along the embedding of the second field.

This is base-change descent infrastructure for geometric connectedness and reducedness in the ReductiveGroups roadmap.

structure TauCeti.Algebra.TensorProduct.CommonOverfield (k : Type u) (K : Type v) (L : Type w) [Field k] [Field K] [Field L] [Algebra k K] [Algebra k L] : Type (max (max u (v + 1)) (w + 1))

A common overfield of two extensions K / k and L / k.

The K-algebra structure on Ω is compatible with its k-algebra structure, while right embeds L into Ω as a k-algebra.

• Ω : Type (max v w)

  The common overfield.

• fieldΩ : Field self.Ω

  The field structure on the common overfield.

• algebraOmega : Algebra k self.Ω

  The common overfield as a k-algebra.

• algebraKΩ : Algebra K self.Ω

  The common overfield as a K-algebra.

• isScalarTower : IsScalarTower k K self.Ω

  Compatibility of the k- and K-algebra structures on the common overfield.

• right : L →ₐ[k] self.Ω

  The embedding of the second field extension into the common overfield.

noncomputable def TauCeti.Algebra.TensorProduct.commonOverfield (k : Type u) (K : Type v) (L : Type w) [Field k] [Field K] [Field L] [Algebra k K] [Algebra k L] : CommonOverfield k K L

Construct a common overfield of two extensions of a field.

Equations

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

noncomputable def TauCeti.Algebra.TensorProduct.CommonOverfield.comparison {k : Type u} {K : Type v} {L : Type w} [Field k] [Field K] [Field L] [Algebra k K] [Algebra k L] (d : CommonOverfield k K L) (A : Type x) [CommSemiring A] [Algebra k A] : TensorProduct K (TensorProduct k K A) d.Ω ≃+* TensorProduct k A d.Ω

Successive scalar extension through K agrees with direct scalar extension to a common overfield.

Equations

• d.comparison A = TauCeti.Algebra.TensorProduct.baseChangeTowerRingEquiv k K A d.Ω

@[simp]

theorem TauCeti.Algebra.TensorProduct.CommonOverfield.comparison_tmul_tmul {k : Type u} {K : Type v} {L : Type w} [Field k] [Field K] [Field L] [Algebra k K] [Algebra k L] (d : CommonOverfield k K L) (A : Type x) [CommSemiring A] [Algebra k A] (x : K) (a : A) (ω : d.Ω) : (d.comparison A) (x ⊗ₜ[k] a ⊗ₜ[K] ω) = a ⊗ₜ[k] (x • ω)

The common-overfield comparison sends nested pure tensors to pure tensors.

@[simp]

theorem TauCeti.Algebra.TensorProduct.CommonOverfield.comparison_symm_tmul {k : Type u} {K : Type v} {L : Type w} [Field k] [Field K] [Field L] [Algebra k K] [Algebra k L] (d : CommonOverfield k K L) (A : Type x) [CommSemiring A] [Algebra k A] (a : A) (ω : d.Ω) : (d.comparison A).symm (a ⊗ₜ[k] ω) = 1 ⊗ₜ[k] a ⊗ₜ[K] ω

The inverse common-overfield comparison sends pure tensors to nested pure tensors.

noncomputable def TauCeti.Algebra.TensorProduct.CommonOverfield.map {k : Type u} {K : Type v} {L : Type w} [Field k] [Field K] [Field L] [Algebra k K] [Algebra k L] (d : CommonOverfield k K L) (A : Type x) [CommSemiring A] [Algebra k A] : TensorProduct k A L →ₐ[k] TensorProduct k A d.Ω

Scalar extension along the embedding of L into a common overfield.

Equations

• d.map A = Algebra.TensorProduct.map (AlgHom.id k A) d.right

@[simp]

theorem TauCeti.Algebra.TensorProduct.CommonOverfield.map_tmul {k : Type u} {K : Type v} {L : Type w} [Field k] [Field K] [Field L] [Algebra k K] [Algebra k L] (d : CommonOverfield k K L) (A : Type x) [CommSemiring A] [Algebra k A] (a : A) (l : L) : (d.map A) (a ⊗ₜ[k] l) = a ⊗ₜ[k] d.right l

Scalar extension to a common overfield maps each pure tensor componentwise.

theorem TauCeti.Algebra.TensorProduct.CommonOverfield.map_injective {k : Type u} {K : Type v} {L : Type w} [Field k] [Field K] [Field L] [Algebra k K] [Algebra k L] (d : CommonOverfield k K L) (A : Type x) [CommRing A] [Algebra k A] : Function.Injective ⇑(d.map A)

Scalar extension from L to a common overfield is injective.