Module

Compositum.lean

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.Compositum

61 declarations indexed from sourceView source ↗

Module documentation

Field-theoretic composita for finite valued extensions

The actual common-top part of Abhyankar's lemma needs valuation data on the compositum L ⊔ K' inside a common ambient field. This file records the purely field-theoretic source facts before any valuation extension is added: finite-dimensionality over either branch, degree bounds and equalities, the intersection degree square, and separability of the common top.

Imports8

Mathlib.Algebra.Algebra.Subalgebra.Lattice
Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Mathlib.FieldTheory.Relrank
Mathlib.FieldTheory.LinearDisjoint
Mathlib.FieldTheory.SeparableClosure
Mathlib.RingTheory.Ideal.Quotient.Operations
Mathlib.RingTheory.Unramified.Field
Mathlib.RingTheory.TensorProduct.Finite

Imported by9

theorem

fg_comap_val_of_fg_of_le

L40 ↗

DiscreteValuationField.FieldCompositum.fg_comap_val_of_fg_of_le

Documentation

A finitely generated intermediate field of the ambient field Ω which is contained in L remains finitely generated after pulling it back to the field type L.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
namespace DiscreteValuationField
namespace FieldCompositum
open scoped TensorProduct
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]

Lean source · statement

theorem fg_comap_val_of_fg_of_le
    (L₀ L : IntermediateField K Ω) (hL₀_le : L₀ ≤ L) (hfg : L₀.FG) :
    (L₀.comap L.val).FG

theorem

map_val_le_self

L79 ↗

DiscreteValuationField.FieldCompositum.map_val_le_self

Documentation

The image of an intermediate field of L under the ambient inclusion L -> Ω is contained in the original ambient intermediate field L.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
namespace DiscreteValuationField
namespace FieldCompositum
open scoped TensorProduct
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]

Lean source · statement

theorem map_val_le_self
    (L : IntermediateField K Ω) (U : IntermediateField K L) :
    U.map L.val ≤ L

theorem

sup_map_val_sup_le_sup_of_right_le

L89 ↗

DiscreteValuationField.FieldCompositum.sup_map_val_sup_le_sup_of_right_le

Documentation

If the right finite-support field lies in K', then the finite common top built from a left subfield of L maps into the ambient common top L ⊔ K'.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
namespace DiscreteValuationField
namespace FieldCompositum
open scoped TensorProduct
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]

Lean source · statement

theorem sup_map_val_sup_le_sup_of_right_le
    (L K' : IntermediateField K Ω) (U : IntermediateField K L)
    {K₀ : IntermediateField K Ω} (hK₀ : K₀ ≤ K') :
    (U.map L.val ⊔ K₀ : IntermediateField K Ω) ≤
      (L ⊔ K' : IntermediateField K Ω)

theorem

finiteDimensional_map_val_of_finiteDimensional

L104 ↗

DiscreteValuationField.FieldCompositum.finiteDimensional_map_val_of_finiteDimensional

Documentation

Finite-dimensionality transfers from a left subextension U ≤ L to its image in the ambient field Ω.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
namespace DiscreteValuationField
namespace FieldCompositum
open scoped TensorProduct
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]

Lean source · statement

theorem finiteDimensional_map_val_of_finiteDimensional
    (L : IntermediateField K Ω) (U : IntermediateField K L)
    [FiniteDimensional K U] :
    FiniteDimensional K (U.map L.val)

instance

supRightAlgebra

L110 ↗

DiscreteValuationField.FieldCompositum.supRightAlgebra

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
namespace DiscreteValuationField
namespace FieldCompositum
open scoped TensorProduct
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]

Lean source · statement

instance supRightAlgebra (L K' : IntermediateField K Ω) :
    Algebra K' (L ⊔ K' : IntermediateField K Ω)

instance

supLeftAlgebra

L114 ↗

DiscreteValuationField.FieldCompositum.supLeftAlgebra

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
namespace DiscreteValuationField
namespace FieldCompositum
open scoped TensorProduct
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]

Lean source · statement

instance supLeftAlgebra (L K' : IntermediateField K Ω) :
    Algebra L (L ⊔ K' : IntermediateField K Ω)

instance

supRightIsScalarTower

L118 ↗

DiscreteValuationField.FieldCompositum.supRightIsScalarTower

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
namespace DiscreteValuationField
namespace FieldCompositum
open scoped TensorProduct
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]

Lean source · statement

instance supRightIsScalarTower (L K' : IntermediateField K Ω) :
    IsScalarTower K K' (L ⊔ K' : IntermediateField K Ω)

instance

supLeftIsScalarTower

L125 ↗

DiscreteValuationField.FieldCompositum.supLeftIsScalarTower

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
namespace DiscreteValuationField
namespace FieldCompositum
open scoped TensorProduct
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]

Lean source · statement

instance supLeftIsScalarTower (L K' : IntermediateField K Ω) :
    IsScalarTower K L (L ⊔ K' : IntermediateField K Ω)

theorem

tensorProduct_exists_list_sum_tmul

L135 ↗

DiscreteValuationField.FieldCompositum.tensorProduct_exists_list_sum_tmul

Documentation

Every tensor is a finite sum of pure tensors. This local source form is used to move from abstract field-level tensor representatives to denominator clearing data in the compositum arguments.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
namespace DiscreteValuationField
namespace FieldCompositum
open scoped TensorProduct
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]

Lean source · full declaration

theorem tensorProduct_exists_list_sum_tmul
    {R : Type u} {A B : Type v} [CommSemiring R]
    [AddCommMonoid A] [Module R A] [AddCommMonoid B] [Module R B]
    (z : A ⊗[R] B) :
    ∃ l : List (A × B), z = (l.map (fun p => p.1 ⊗ₜ[R] p.2)).sum := by
  refine TensorProduct.inductionOn z ?tmul ?add
  · intro a b
    exact ⟨[(a, b)], by simp⟩
  · intro x y hx hy
    rcases hx with ⟨lx, hx⟩
    rcases hy with ⟨ly, hy⟩
    refine ⟨lx ++ ly, ?_⟩
    rw [List.map_append, List.sum_append, ← hx, ← hy]

theorem

sup_productMap_range

L152 ↗

DiscreteValuationField.FieldCompositum.sup_productMap_range

Documentation

The field-level product map L ⊗_K K' -> Ω has image exactly the compositum subalgebra L ⊔ K'. This is the pure algebraic generation source behind the later valuation-ring common-top comparison.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
namespace DiscreteValuationField
namespace FieldCompositum
open scoped TensorProduct
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]

Lean source · statement

theorem sup_productMap_range
    (L K' : IntermediateField K Ω) [FiniteDimensional K L] :
    (Algebra.TensorProduct.productMap L.val K'.val).range =
      (L ⊔ K').toSubalgebra

theorem

exists_tensor_productMap_eq_of_mem_sup

L161 ↗

DiscreteValuationField.FieldCompositum.exists_tensor_productMap_eq_of_mem_sup

Documentation

Every element of the compositum is represented by a tensor under the field-level product map L ⊗_K K' -> Ω.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
namespace DiscreteValuationField
namespace FieldCompositum
open scoped TensorProduct
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]

Lean source · statement

theorem exists_tensor_productMap_eq_of_mem_sup
    (L K' : IntermediateField K Ω) [FiniteDimensional K L]
    {x : Ω} (hx : x ∈ (L ⊔ K' : IntermediateField K Ω)) :
    ∃ z : L ⊗[K] K', Algebra.TensorProduct.productMap L.val K'.val z = x

theorem

sup_productMap_val_comp

L174 ↗

DiscreteValuationField.FieldCompositum.sup_productMap_val_comp

Documentation

The product map into the actual compositum subtype agrees with the ambient product map after coercing the target back to Ω.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
namespace DiscreteValuationField
namespace FieldCompositum
open scoped TensorProduct
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]

Lean source · full declaration

theorem sup_productMap_val_comp
    (L K' : IntermediateField K Ω) :
    (L ⊔ K').val.comp
        (Algebra.TensorProduct.productMap
          (IntermediateField.inclusion (show L ≤ L ⊔ K' from le_sup_left))
          (IntermediateField.inclusion (show K' ≤ L ⊔ K' from le_sup_right))) =
        Algebra.TensorProduct.productMap L.val K'.val := by
    apply Algebra.TensorProduct.ext
    · ext a
      rfl
    · ext b
      rfl

theorem

exists_sup_tensor_productMap_eq

L189 ↗

DiscreteValuationField.FieldCompositum.exists_sup_tensor_productMap_eq

Documentation

Every element of the compositum subtype is represented by a tensor under the intrinsic product map L ⊗_K K' -> L ⊔ K'.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
namespace DiscreteValuationField
namespace FieldCompositum
open scoped TensorProduct
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]

Lean source · full declaration

theorem exists_sup_tensor_productMap_eq
    (L K' : IntermediateField K Ω) [FiniteDimensional K L]
    (x : (L ⊔ K' : IntermediateField K Ω)) :
    ∃ z : L ⊗[K] K',
      Algebra.TensorProduct.productMap
          (IntermediateField.inclusion (show L ≤ L ⊔ K' from le_sup_left))
          (IntermediateField.inclusion (show K' ≤ L ⊔ K' from le_sup_right)) z =
        x := by
  rcases exists_tensor_productMap_eq_of_mem_sup
      (K := K) (Ω := Ω) L K' x.2 with ⟨z, hz⟩
  refine ⟨z, ?_⟩
  apply Subtype.ext
  rw [← hz]
  exact congrArg (fun f => f z)
    (sup_productMap_val_comp (K := K) (Ω := Ω) L K')

theorem

sup_productMap_surjective

L208 ↗

DiscreteValuationField.FieldCompositum.sup_productMap_surjective

Documentation

The intrinsic field-level product map L ⊗_K K' -> L ⊔ K' is surjective. This is the exact field-generation source used before any valuation-ring generation statement is attempted.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
namespace DiscreteValuationField
namespace FieldCompositum
open scoped TensorProduct
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]

Lean source · full declaration

theorem sup_productMap_surjective
    (L K' : IntermediateField K Ω) [FiniteDimensional K L] :
    Function.Surjective
      (Algebra.TensorProduct.productMap
        (IntermediateField.inclusion (show L ≤ L ⊔ K' from le_sup_left))
        (IntermediateField.inclusion (show K' ≤ L ⊔ K' from le_sup_right))) := by
  intro x
  exact exists_sup_tensor_productMap_eq (K := K) (Ω := Ω) L K' x

theorem

exists_list_sum_sup_tensor_productMap_eq

L219 ↗

DiscreteValuationField.FieldCompositum.exists_list_sum_sup_tensor_productMap_eq

Documentation

Finite-sum form of the intrinsic field-level product-map generation L ⊗_K K' -> L ⊔ K'.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
namespace DiscreteValuationField
namespace FieldCompositum
open scoped TensorProduct
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]

Lean source · full declaration

theorem exists_list_sum_sup_tensor_productMap_eq
    (L K' : IntermediateField K Ω) [FiniteDimensional K L]
    (x : (L ⊔ K' : IntermediateField K Ω)) :
    ∃ l : List (L × K'),
      Algebra.TensorProduct.productMap
          (IntermediateField.inclusion (show L ≤ L ⊔ K' from le_sup_left))
          (IntermediateField.inclusion (show K' ≤ L ⊔ K' from le_sup_right))
          ((l.map (fun p => p.1 ⊗ₜ[K] p.2)).sum) =
        x := by
  rcases exists_sup_tensor_productMap_eq (K := K) (Ω := Ω) L K' x with
    ⟨z, hz⟩
  rcases tensorProduct_exists_list_sum_tmul
      (R := K) (A := L) (B := K') z with ⟨l, hl⟩
  refine ⟨l, ?_⟩
  rw [← hl]
  exact hz

theorem

sup_left_adjoin_right_range_eq_top

L237 ↗

DiscreteValuationField.FieldCompositum.sup_left_adjoin_right_range_eq_top

Documentation

The compositum is generated over the left factor by the right factor.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
namespace DiscreteValuationField
namespace FieldCompositum
open scoped TensorProduct
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]

Lean source · full declaration

theorem sup_left_adjoin_right_range_eq_top
    (L K' : IntermediateField K Ω) [FiniteDimensional K L] :
    Algebra.adjoin L
        (Set.range
          (IntermediateField.inclusion
            (show K' ≤ L ⊔ K' from le_sup_right))) =
      (⊤ : Subalgebra L (L ⊔ K' : IntermediateField K Ω)) := by
  let iL :
      L →ₐ[K] (L ⊔ K' : IntermediateField K Ω) :=
    IntermediateField.inclusion (show L ≤ L ⊔ K' from le_sup_left)
  let iK' :
      K' →ₐ[K] (L ⊔ K' : IntermediateField K Ω) :=
    IntermediateField.inclusion (show K' ≤ L ⊔ K' from le_sup_right)
  let S : Subalgebra L (L ⊔ K' : IntermediateField K Ω) :=
    Algebra.adjoin L (Set.range iK')
  change S = ⊤
  apply Algebra.eq_top_iff.2
  intro x
  rcases exists_sup_tensor_productMap_eq (K := K) (Ω := Ω) L K' x with
    ⟨z, hz⟩
  rw [← hz]
  refine TensorProduct.inductionOn z ?tmul ?add
  · intro a b
    have ha : iL a ∈ S := by
      change algebraMap L (L ⊔ K' : IntermediateField K Ω) a ∈ S
      exact S.algebraMap_mem a
    have hb : iK' b ∈ S :=
      Algebra.subset_adjoin (R := L) (s := Set.range iK') ⟨b, rfl⟩
    simpa [S, iL, iK', Algebra.TensorProduct.productMap_apply_tmul] using
      S.mul_mem ha hb
  · intro x y hx hy
    simpa [map_add] using S.add_mem hx hy

theorem

sup_flip_productMap_range

L273 ↗

DiscreteValuationField.FieldCompositum.sup_flip_productMap_range

Documentation

The field-level product map K' ⊗_K L -> Ω has image exactly the compositum subalgebra L ⊔ K'. This is the order matching the later valuation-ring tensor product O_K' ⊗_{O_K} O_L.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
namespace DiscreteValuationField
namespace FieldCompositum
open scoped TensorProduct
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]

Lean source · statement

theorem sup_flip_productMap_range
    (L K' : IntermediateField K Ω) [FiniteDimensional K L] :
    (Algebra.TensorProduct.productMap K'.val L.val).range =
      (L ⊔ K').toSubalgebra

theorem

exists_flip_tensor_productMap_eq_of_mem_sup

L284 ↗

DiscreteValuationField.FieldCompositum.exists_flip_tensor_productMap_eq_of_mem_sup

Documentation

Every element of the compositum is represented by a tensor under the field-level product map K' ⊗_K L -> Ω, in the order matching the valuation ring tensor product.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
namespace DiscreteValuationField
namespace FieldCompositum
open scoped TensorProduct
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]

Lean source · statement

theorem exists_flip_tensor_productMap_eq_of_mem_sup
    (L K' : IntermediateField K Ω) [FiniteDimensional K L]
    {x : Ω} (hx : x ∈ (L ⊔ K' : IntermediateField K Ω)) :
    ∃ z : K' ⊗[K] L, Algebra.TensorProduct.productMap K'.val L.val z = x

theorem

sup_flip_productMap_val_comp

L297 ↗

DiscreteValuationField.FieldCompositum.sup_flip_productMap_val_comp

Documentation

The product map K' ⊗_K L -> L ⊔ K' agrees with the ambient product map after coercing the target back to Ω.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
namespace DiscreteValuationField
namespace FieldCompositum
open scoped TensorProduct
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]

Lean source · full declaration

theorem sup_flip_productMap_val_comp
    (L K' : IntermediateField K Ω) :
    (L ⊔ K').val.comp
        (Algebra.TensorProduct.productMap
          (IntermediateField.inclusion (show K' ≤ L ⊔ K' from le_sup_right))
          (IntermediateField.inclusion (show L ≤ L ⊔ K' from le_sup_left))) =
        Algebra.TensorProduct.productMap K'.val L.val := by
    apply Algebra.TensorProduct.ext
    · ext a
      rfl
    · ext b
      rfl

theorem

exists_sup_flip_tensor_productMap_eq

L312 ↗

DiscreteValuationField.FieldCompositum.exists_sup_flip_tensor_productMap_eq

Documentation

Every element of the compositum subtype is represented by a tensor under the intrinsic product map K' ⊗_K L -> L ⊔ K'.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
namespace DiscreteValuationField
namespace FieldCompositum
open scoped TensorProduct
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]

Lean source · full declaration

theorem exists_sup_flip_tensor_productMap_eq
    (L K' : IntermediateField K Ω) [FiniteDimensional K L]
    (x : (L ⊔ K' : IntermediateField K Ω)) :
    ∃ z : K' ⊗[K] L,
      Algebra.TensorProduct.productMap
          (IntermediateField.inclusion (show K' ≤ L ⊔ K' from le_sup_right))
          (IntermediateField.inclusion (show L ≤ L ⊔ K' from le_sup_left)) z =
        x := by
  rcases exists_flip_tensor_productMap_eq_of_mem_sup
      (K := K) (Ω := Ω) L K' x.2 with ⟨z, hz⟩
  refine ⟨z, ?_⟩
  apply Subtype.ext
  rw [← hz]
  exact congrArg (fun f => f z)
    (sup_flip_productMap_val_comp (K := K) (Ω := Ω) L K')

theorem

sup_flip_productMap_surjective

L331 ↗

DiscreteValuationField.FieldCompositum.sup_flip_productMap_surjective

Documentation

The intrinsic field-level product map K' ⊗_K L -> L ⊔ K' is surjective. This is the source form aligned with the valuation-ring tensor map used in the unramified base-change construction.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
namespace DiscreteValuationField
namespace FieldCompositum
open scoped TensorProduct
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]

Lean source · full declaration

theorem sup_flip_productMap_surjective
    (L K' : IntermediateField K Ω) [FiniteDimensional K L] :
    Function.Surjective
      (Algebra.TensorProduct.productMap
        (IntermediateField.inclusion (show K' ≤ L ⊔ K' from le_sup_right))
        (IntermediateField.inclusion (show L ≤ L ⊔ K' from le_sup_left))) := by
  intro x
  exact exists_sup_flip_tensor_productMap_eq (K := K) (Ω := Ω) L K' x

def

supFlipProductMapRightAlgHom

L343 ↗

DiscreteValuationField.FieldCompositum.supFlipProductMapRightAlgHom

Documentation

The intrinsic product map K' ⊗_K L -> L ⊔ K', regarded as a K'-algebra hom. This is the field-level base-change map used in the the unramified base-change theorem; no separability of K'/K is involved.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
namespace DiscreteValuationField
namespace FieldCompositum
open scoped TensorProduct
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]

Lean source · statement

def supFlipProductMapRightAlgHom
    (L K' : IntermediateField K Ω) :
    K' ⊗[K] L →ₐ[K'] (L ⊔ K' : IntermediateField K Ω)

theorem

supFlipProductMapRightAlgHom_surjective

L355 ↗

DiscreteValuationField.FieldCompositum.supFlipProductMapRightAlgHom_surjective

Documentation

The K'-algebra product map K' ⊗_K L -> L ⊔ K' is surjective.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
namespace DiscreteValuationField
namespace FieldCompositum
open scoped TensorProduct
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]

Lean source · statement

theorem supFlipProductMapRightAlgHom_surjective
    (L K' : IntermediateField K Ω) [FiniteDimensional K L] :
    Function.Surjective
      (supFlipProductMapRightAlgHom (K := K) (Ω := Ω) L K')

theorem

finiteDimensional_sup_over_right_of_left

L369 ↗

DiscreteValuationField.FieldCompositum.finiteDimensional_sup_over_right_of_left

Documentation

The actual compositum L ⊔ K' is finite over the right factor whenever the left factor is finite over the base.

This is the finite-dimensional source needed for unramified base change: base change by an arbitrary algebraic extension is reduced elementwise to a finite right subextension, but the finiteness of the right branch itself comes from the finite left factor.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
namespace DiscreteValuationField
namespace FieldCompositum
open scoped TensorProduct
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]

Lean source · statement

theorem finiteDimensional_sup_over_right_of_left
    (L K' : IntermediateField K Ω) [FiniteDimensional K L] :
    FiniteDimensional K' (L ⊔ K' : IntermediateField K Ω)

instance

tensorProductIdealHasQuotient

L379 ↗

DiscreteValuationField.FieldCompositum.tensorProductIdealHasQuotient

Documentation

The algebraic first-isomorphism theorem with the source ring structure fixed by its commutative-ring parent.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
namespace DiscreteValuationField
namespace FieldCompositum
open scoped TensorProduct
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]

Lean source · statement

instance tensorProductIdealHasQuotient
    (L K' : IntermediateField K Ω) :
    HasQuotient (K' ⊗[K] L) (Ideal (K' ⊗[K] L))

def

quotientKerAlgEquivOfSurjectiveCommRing

L385 ↗

DiscreteValuationField.FieldCompositum.quotientKerAlgEquivOfSurjectiveCommRing

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
namespace DiscreteValuationField
namespace FieldCompositum
open scoped TensorProduct
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
/-- The algebraic first-isomorphism theorem with the source ring structure
fixed by its commutative-ring parent. -/
local instance tensorProductIdealHasQuotient
    (L K' : IntermediateField K Ω) :
    HasQuotient (K' ⊗[K] L) (Ideal (K' ⊗[K] L)) :=
  @Ideal.instHasQuotient (K' ⊗[K] L)
    (inferInstance : CommRing (K' ⊗[K] L)).toRing

Lean source · statement

def quotientKerAlgEquivOfSurjectiveCommRing
    {R A B : Type*}
    [ringR : CommSemiring R] [ringA : CommRing A]
    [algebraRA : Algebra R A]
    [ringB : Semiring B] [algebraRB : Algebra R B]
    {f : A →ₐ[R] B} (hf : Function.Surjective f) :
    (@HasQuotient.Quotient A (Ideal A)
      (@Ideal.instHasQuotient A ringA.toRing)
      (RingHom.ker f.toRingHom)) ≃ₐ[R] B

def

supFlipProductMapRightAlgHomQuotientKerAlgEquiv

L399 ↗

DiscreteValuationField.FieldCompositum.supFlipProductMapRightAlgHomQuotientKerAlgEquiv

Documentation

The field factor selected by the product map K' ⊗_K L -> L ⊔ K' is the actual compositum field: quotienting by the kernel of the surjective K'-algebra map gives L ⊔ K'.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
namespace DiscreteValuationField
namespace FieldCompositum
open scoped TensorProduct
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
/-- The algebraic first-isomorphism theorem with the source ring structure
fixed by its commutative-ring parent. -/
local instance tensorProductIdealHasQuotient
    (L K' : IntermediateField K Ω) :
    HasQuotient (K' ⊗[K] L) (Ideal (K' ⊗[K] L)) :=
  @Ideal.instHasQuotient (K' ⊗[K] L)
    (inferInstance : CommRing (K' ⊗[K] L)).toRing

Lean source · statement

def supFlipProductMapRightAlgHomQuotientKerAlgEquiv
    (L K' : IntermediateField K Ω) [FiniteDimensional K L] :
    ((K' ⊗[K] L) ⧸
        (RingHom.ker
          (supFlipProductMapRightAlgHom (K := K) (Ω := Ω) L K').toRingHom))
      ≃ₐ[K'] (L ⊔ K' : IntermediateField K Ω)

theorem

exists_list_sum_sup_flip_tensor_productMap_eq

L422 ↗

DiscreteValuationField.FieldCompositum.exists_list_sum_sup_flip_tensor_productMap_eq

Documentation

Finite-sum form of the intrinsic field-level product-map generation K' ⊗_K L -> L ⊔ K', in the order matching the valuation-ring tensor product.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
namespace DiscreteValuationField
namespace FieldCompositum
open scoped TensorProduct
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
/-- The algebraic first-isomorphism theorem with the source ring structure
fixed by its commutative-ring parent. -/
local instance tensorProductIdealHasQuotient
    (L K' : IntermediateField K Ω) :
    HasQuotient (K' ⊗[K] L) (Ideal (K' ⊗[K] L)) :=
  @Ideal.instHasQuotient (K' ⊗[K] L)
    (inferInstance : CommRing (K' ⊗[K] L)).toRing

Lean source · full declaration

theorem exists_list_sum_sup_flip_tensor_productMap_eq
    (L K' : IntermediateField K Ω) [FiniteDimensional K L]
    (x : (L ⊔ K' : IntermediateField K Ω)) :
    ∃ l : List (K' × L),
      Algebra.TensorProduct.productMap
          (IntermediateField.inclusion (show K' ≤ L ⊔ K' from le_sup_right))
          (IntermediateField.inclusion (show L ≤ L ⊔ K' from le_sup_left))
          ((l.map (fun p => p.1 ⊗ₜ[K] p.2)).sum) =
        x := by
  rcases exists_sup_flip_tensor_productMap_eq (K := K) (Ω := Ω) L K' x with
    ⟨z, hz⟩
  rcases tensorProduct_exists_list_sum_tmul
      (R := K) (A := K') (B := L) z with ⟨l, hl⟩
  refine ⟨l, ?_⟩
  rw [← hl]
  exact hz

theorem

sup_right_adjoin_left_range_eq_top

L440 ↗

DiscreteValuationField.FieldCompositum.sup_right_adjoin_left_range_eq_top

Documentation

The compositum is generated over the right factor by the left factor.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
namespace DiscreteValuationField
namespace FieldCompositum
open scoped TensorProduct
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
/-- The algebraic first-isomorphism theorem with the source ring structure
fixed by its commutative-ring parent. -/
local instance tensorProductIdealHasQuotient
    (L K' : IntermediateField K Ω) :
    HasQuotient (K' ⊗[K] L) (Ideal (K' ⊗[K] L)) :=
  @Ideal.instHasQuotient (K' ⊗[K] L)
    (inferInstance : CommRing (K' ⊗[K] L)).toRing

Lean source · full declaration

theorem sup_right_adjoin_left_range_eq_top
    (L K' : IntermediateField K Ω) [FiniteDimensional K L] :
    Algebra.adjoin K'
        (Set.range
          (IntermediateField.inclusion
            (show L ≤ L ⊔ K' from le_sup_left))) =
      (⊤ : Subalgebra K' (L ⊔ K' : IntermediateField K Ω)) := by
  let iK' :
      K' →ₐ[K] (L ⊔ K' : IntermediateField K Ω) :=
    IntermediateField.inclusion (show K' ≤ L ⊔ K' from le_sup_right)
  let iL :
      L →ₐ[K] (L ⊔ K' : IntermediateField K Ω) :=
    IntermediateField.inclusion (show L ≤ L ⊔ K' from le_sup_left)
  let S : Subalgebra K' (L ⊔ K' : IntermediateField K Ω) :=
    Algebra.adjoin K' (Set.range iL)
  change S = ⊤
  apply Algebra.eq_top_iff.2
  intro x
  rcases exists_sup_flip_tensor_productMap_eq (K := K) (Ω := Ω) L K' x with
    ⟨z, hz⟩
  rw [← hz]
  refine TensorProduct.inductionOn z ?tmul ?add
  · intro a b
    have ha : iK' a ∈ S := by
      change algebraMap K' (L ⊔ K' : IntermediateField K Ω) a ∈ S
      exact S.algebraMap_mem a
    have hb : iL b ∈ S :=
      Algebra.subset_adjoin (R := K') (s := Set.range iL) ⟨b, rfl⟩
    simpa [S, iK', iL, Algebra.TensorProduct.productMap_apply_tmul] using
      S.mul_mem ha hb
  · intro x y hx hy
    simpa [map_add] using S.add_mem hx hy

theorem

sup_right_adjoin_left_singleton_eq_top_of_adjoin_eq_top

L477 ↗

DiscreteValuationField.FieldCompositum.sup_right_adjoin_left_singleton_eq_top_of_adjoin_eq_top

Documentation

If the left factor is generated over K by one element, then the compositum is generated over the right factor by the image of that same element. This is the field-level primitive-generator source behind the residue-generation step in unramified base change.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
namespace DiscreteValuationField
namespace FieldCompositum
open scoped TensorProduct
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
/-- The algebraic first-isomorphism theorem with the source ring structure
fixed by its commutative-ring parent. -/
local instance tensorProductIdealHasQuotient
    (L K' : IntermediateField K Ω) :
    HasQuotient (K' ⊗[K] L) (Ideal (K' ⊗[K] L)) :=
  @Ideal.instHasQuotient (K' ⊗[K] L)
    (inferInstance : CommRing (K' ⊗[K] L)).toRing

Lean source · full declaration

theorem sup_right_adjoin_left_singleton_eq_top_of_adjoin_eq_top
    (L K' : IntermediateField K Ω) [FiniteDimensional K L]
    (x : L)
    (hx : Algebra.adjoin K ({x} : Set L) =
      (⊤ : Subalgebra K L)) :
    Algebra.adjoin K'
        ({(IntermediateField.inclusion
            (show L ≤ L ⊔ K' from le_sup_left)) x} :
          Set (L ⊔ K' : IntermediateField K Ω)) =
      (⊤ : Subalgebra K' (L ⊔ K' : IntermediateField K Ω)) := by
  let iL :
      L →ₐ[K] (L ⊔ K' : IntermediateField K Ω) :=
    IntermediateField.inclusion (show L ≤ L ⊔ K' from le_sup_left)
  let S : Subalgebra K' (L ⊔ K' : IntermediateField K Ω) :=
    Algebra.adjoin K' ({iL x} : Set (L ⊔ K' : IntermediateField K Ω))
  have hrange_le :
      Algebra.adjoin K' (Set.range iL) ≤ S := by
    rw [Algebra.adjoin_le_iff]
    intro y hy
    rcases hy with ⟨z, rfl⟩
    have hz : z ∈ Algebra.adjoin K ({x} : Set L) := by
      simp [hx]
    change iL z ∈ S
    refine
      Algebra.adjoin_induction
        (p := fun z _ => iL z ∈ S)
        ?mem ?algebraMap ?add ?mul hz
    · intro z hz
      have hz_eq : z = x := by
        simpa using hz
      rw [hz_eq]
      exact Algebra.self_mem_adjoin_singleton K' (iL x)
    · intro a
      have hscalar :
          iL (algebraMap K L a) =
            algebraMap K' (L ⊔ K' : IntermediateField K Ω)
              (algebraMap K K' a) := by
        ext
        rfl
      rw [hscalar]
      exact S.algebraMap_mem (algebraMap K K' a)
    · intro z₁ z₂ _hz₁ _hz₂ hz₁_mem hz₂_mem
      simpa [map_add] using S.add_mem hz₁_mem hz₂_mem
    · intro z₁ z₂ _hz₁ _hz₂ hz₁_mem hz₂_mem
      simpa [map_mul] using S.mul_mem hz₁_mem hz₂_mem
  have htop_le : (⊤ : Subalgebra K' (L ⊔ K' : IntermediateField K Ω)) ≤ S := by
    rw [← sup_right_adjoin_left_range_eq_top (K := K) (Ω := Ω) L K']
    exact hrange_le
  exact le_antisymm le_top htop_le

theorem

right_finrank_mul_compositum_finrank

L528 ↗

DiscreteValuationField.FieldCompositum.right_finrank_mul_compositum_finrank

Documentation

Tower formula for the degree of the compositum over the right factor.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
namespace DiscreteValuationField
namespace FieldCompositum
open scoped TensorProduct
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
/-- The algebraic first-isomorphism theorem with the source ring structure
fixed by its commutative-ring parent. -/
local instance tensorProductIdealHasQuotient
    (L K' : IntermediateField K Ω) :
    HasQuotient (K' ⊗[K] L) (Ideal (K' ⊗[K] L)) :=
  @Ideal.instHasQuotient (K' ⊗[K] L)
    (inferInstance : CommRing (K' ⊗[K] L)).toRing

Lean source · full declaration

theorem right_finrank_mul_compositum_finrank
    (L K' : IntermediateField K Ω) :
    Module.finrank K K' *
        Module.finrank K'
          (IntermediateField.extendScalars (show K' ≤ L ⊔ K' from le_sup_right)) =
      Module.finrank K (L ⊔ K' : IntermediateField K Ω) := by
  have h := IntermediateField.finrank_bot_mul_relfinrank
    (show K' ≤ L ⊔ K' from le_sup_right)
  simpa [IntermediateField.relfinrank_eq_finrank_of_le
    (show K' ≤ L ⊔ K' from le_sup_right)] using h

theorem

left_finrank_mul_compositum_finrank

L540 ↗

DiscreteValuationField.FieldCompositum.left_finrank_mul_compositum_finrank

Documentation

Tower formula for the degree of the compositum over the left factor.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
namespace DiscreteValuationField
namespace FieldCompositum
open scoped TensorProduct
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
/-- The algebraic first-isomorphism theorem with the source ring structure
fixed by its commutative-ring parent. -/
local instance tensorProductIdealHasQuotient
    (L K' : IntermediateField K Ω) :
    HasQuotient (K' ⊗[K] L) (Ideal (K' ⊗[K] L)) :=
  @Ideal.instHasQuotient (K' ⊗[K] L)
    (inferInstance : CommRing (K' ⊗[K] L)).toRing

Lean source · full declaration

theorem left_finrank_mul_compositum_finrank
    (L K' : IntermediateField K Ω) :
    Module.finrank K L *
        Module.finrank L
          (IntermediateField.extendScalars (show L ≤ L ⊔ K' from le_sup_left)) =
      Module.finrank K (L ⊔ K' : IntermediateField K Ω) := by
  have h := IntermediateField.finrank_bot_mul_relfinrank
    (show L ≤ L ⊔ K' from le_sup_left)
  simpa [IntermediateField.relfinrank_eq_finrank_of_le
    (show L ≤ L ⊔ K' from le_sup_left)] using h

theorem

finiteDimensional_compositum_over_right_of_left

L553 ↗

DiscreteValuationField.FieldCompositum.finiteDimensional_compositum_over_right_of_left

Documentation

The compositum is finite over the right factor when the left factor is finite over the base.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
namespace DiscreteValuationField
namespace FieldCompositum
open scoped TensorProduct
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
/-- The algebraic first-isomorphism theorem with the source ring structure
fixed by its commutative-ring parent. -/
local instance tensorProductIdealHasQuotient
    (L K' : IntermediateField K Ω) :
    HasQuotient (K' ⊗[K] L) (Ideal (K' ⊗[K] L)) :=
  @Ideal.instHasQuotient (K' ⊗[K] L)
    (inferInstance : CommRing (K' ⊗[K] L)).toRing

Lean source · full declaration

theorem finiteDimensional_compositum_over_right_of_left
    (L K' : IntermediateField K Ω)
    [FiniteDimensional K L] :
    FiniteDimensional K'
      (IntermediateField.extendScalars (show K' ≤ L ⊔ K' from le_sup_right)) := by
  change FiniteDimensional K' (L ⊔ K' : IntermediateField K Ω)
  exact finiteDimensional_sup_over_right_of_left L K'

theorem

finiteDimensional_compositum_over_right

L563 ↗

DiscreteValuationField.FieldCompositum.finiteDimensional_compositum_over_right

Documentation

The compositum is finite over the right factor when both factors are finite over the base.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
namespace DiscreteValuationField
namespace FieldCompositum
open scoped TensorProduct
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
/-- The algebraic first-isomorphism theorem with the source ring structure
fixed by its commutative-ring parent. -/
local instance tensorProductIdealHasQuotient
    (L K' : IntermediateField K Ω) :
    HasQuotient (K' ⊗[K] L) (Ideal (K' ⊗[K] L)) :=
  @Ideal.instHasQuotient (K' ⊗[K] L)
    (inferInstance : CommRing (K' ⊗[K] L)).toRing

Lean source · full declaration

theorem finiteDimensional_compositum_over_right
    (L K' : IntermediateField K Ω)
    [FiniteDimensional K L] [FiniteDimensional K K'] :
    FiniteDimensional K'
      (IntermediateField.extendScalars (show K' ≤ L ⊔ K' from le_sup_right)) := by
  exact finiteDimensional_compositum_over_right_of_left L K'

theorem

finiteDimensional_compositum_over_left

L572 ↗

DiscreteValuationField.FieldCompositum.finiteDimensional_compositum_over_left

Documentation

The compositum is finite over the left factor when both factors are finite over the base.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
namespace DiscreteValuationField
namespace FieldCompositum
open scoped TensorProduct
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
/-- The algebraic first-isomorphism theorem with the source ring structure
fixed by its commutative-ring parent. -/
local instance tensorProductIdealHasQuotient
    (L K' : IntermediateField K Ω) :
    HasQuotient (K' ⊗[K] L) (Ideal (K' ⊗[K] L)) :=
  @Ideal.instHasQuotient (K' ⊗[K] L)
    (inferInstance : CommRing (K' ⊗[K] L)).toRing

Lean source · full declaration

theorem finiteDimensional_compositum_over_left
    (L K' : IntermediateField K Ω)
    [FiniteDimensional K L] [FiniteDimensional K K'] :
    FiniteDimensional L
      (IntermediateField.extendScalars (show L ≤ L ⊔ K' from le_sup_left)) := by
  apply FiniteDimensional.of_finrank_pos
  have hformula := left_finrank_mul_compositum_finrank (K := K) (Ω := Ω) L K'
  have hsup_pos : 0 < Module.finrank K (L ⊔ K' : IntermediateField K Ω) := by
    exact Module.finrank_pos
  rw [← hformula] at hsup_pos
  exact Nat.pos_of_mul_pos_left hsup_pos

theorem

finiteDimensional_sup_over_right

L585 ↗

DiscreteValuationField.FieldCompositum.finiteDimensional_sup_over_right

Documentation

The common top field L ⊔ K' is finite over the right factor.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
namespace DiscreteValuationField
namespace FieldCompositum
open scoped TensorProduct
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
/-- The algebraic first-isomorphism theorem with the source ring structure
fixed by its commutative-ring parent. -/
local instance tensorProductIdealHasQuotient
    (L K' : IntermediateField K Ω) :
    HasQuotient (K' ⊗[K] L) (Ideal (K' ⊗[K] L)) :=
  @Ideal.instHasQuotient (K' ⊗[K] L)
    (inferInstance : CommRing (K' ⊗[K] L)).toRing

Lean source · statement

theorem finiteDimensional_sup_over_right
    (L K' : IntermediateField K Ω)
    [FiniteDimensional K L] [FiniteDimensional K K'] :
    FiniteDimensional K' (L ⊔ K' : IntermediateField K Ω)

theorem

finiteDimensional_sup_over_left

L592 ↗

DiscreteValuationField.FieldCompositum.finiteDimensional_sup_over_left

Documentation

The common top field L ⊔ K' is finite over the left factor.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
namespace DiscreteValuationField
namespace FieldCompositum
open scoped TensorProduct
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
/-- The algebraic first-isomorphism theorem with the source ring structure
fixed by its commutative-ring parent. -/
local instance tensorProductIdealHasQuotient
    (L K' : IntermediateField K Ω) :
    HasQuotient (K' ⊗[K] L) (Ideal (K' ⊗[K] L)) :=
  @Ideal.instHasQuotient (K' ⊗[K] L)
    (inferInstance : CommRing (K' ⊗[K] L)).toRing

Lean source · statement

theorem finiteDimensional_sup_over_left
    (L K' : IntermediateField K Ω)
    [FiniteDimensional K L] [FiniteDimensional K K'] :
    FiniteDimensional L (L ⊔ K' : IntermediateField K Ω)

theorem

compositum_finrank_over_right_le_left

L600 ↗

DiscreteValuationField.FieldCompositum.compositum_finrank_over_right_le_left

Documentation

The degree of the base-changed field extension L K' / K' is bounded by the degree of L / K.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
namespace DiscreteValuationField
namespace FieldCompositum
open scoped TensorProduct
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
/-- The algebraic first-isomorphism theorem with the source ring structure
fixed by its commutative-ring parent. -/
local instance tensorProductIdealHasQuotient
    (L K' : IntermediateField K Ω) :
    HasQuotient (K' ⊗[K] L) (Ideal (K' ⊗[K] L)) :=
  @Ideal.instHasQuotient (K' ⊗[K] L)
    (inferInstance : CommRing (K' ⊗[K] L)).toRing

Lean source · full declaration

theorem compositum_finrank_over_right_le_left
    (L K' : IntermediateField K Ω)
    [FiniteDimensional K L] [FiniteDimensional K K'] :
    Module.finrank K'
        (IntermediateField.extendScalars (show K' ≤ L ⊔ K' from le_sup_right)) ≤
      Module.finrank K L := by
  have hformula := right_finrank_mul_compositum_finrank (K := K) (Ω := Ω) L K'
  have hsup_le := IntermediateField.finrank_sup_le L K'
  have hmul :
      Module.finrank K K' *
          Module.finrank K'
            (IntermediateField.extendScalars (show K' ≤ L ⊔ K' from le_sup_right)) ≤
        Module.finrank K K' * Module.finrank K L := by
    calc
      Module.finrank K K' *
          Module.finrank K'
            (IntermediateField.extendScalars (show K' ≤ L ⊔ K' from le_sup_right)) =
          Module.finrank K (L ⊔ K' : IntermediateField K Ω) := hformula
      _ ≤ Module.finrank K L * Module.finrank K K' := hsup_le
      _ = Module.finrank K K' * Module.finrank K L := by rw [mul_comm]
  exact Nat.le_of_mul_le_mul_left hmul
    (Module.finrank_pos (R := K) (M := K'))

theorem

compositum_finrank_over_left_le_right

L624 ↗

DiscreteValuationField.FieldCompositum.compositum_finrank_over_left_le_right

Documentation

Symmetric bound for the degree of the compositum over the left factor.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
namespace DiscreteValuationField
namespace FieldCompositum
open scoped TensorProduct
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
/-- The algebraic first-isomorphism theorem with the source ring structure
fixed by its commutative-ring parent. -/
local instance tensorProductIdealHasQuotient
    (L K' : IntermediateField K Ω) :
    HasQuotient (K' ⊗[K] L) (Ideal (K' ⊗[K] L)) :=
  @Ideal.instHasQuotient (K' ⊗[K] L)
    (inferInstance : CommRing (K' ⊗[K] L)).toRing

Lean source · full declaration

theorem compositum_finrank_over_left_le_right
    (L K' : IntermediateField K Ω)
    [FiniteDimensional K L] [FiniteDimensional K K'] :
    Module.finrank L
        (IntermediateField.extendScalars (show L ≤ L ⊔ K' from le_sup_left)) ≤
      Module.finrank K K' := by
  have hformula := left_finrank_mul_compositum_finrank (K := K) (Ω := Ω) L K'
  have hsup_le := IntermediateField.finrank_sup_le L K'
  have hmul :
      Module.finrank K L *
          Module.finrank L
            (IntermediateField.extendScalars (show L ≤ L ⊔ K' from le_sup_left)) ≤
        Module.finrank K L * Module.finrank K K' := by
    calc
      Module.finrank K L *
          Module.finrank L
            (IntermediateField.extendScalars (show L ≤ L ⊔ K' from le_sup_left)) =
          Module.finrank K (L ⊔ K' : IntermediateField K Ω) := hformula
      _ ≤ Module.finrank K L * Module.finrank K K' := hsup_le
  exact Nat.le_of_mul_le_mul_left hmul
    (Module.finrank_pos (R := K) (M := L))

theorem

sup_finrank_over_right_le_left

L647 ↗

DiscreteValuationField.FieldCompositum.sup_finrank_over_right_le_left

Documentation

Common-top form of the degree bound for L ⊔ K' / K'.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
namespace DiscreteValuationField
namespace FieldCompositum
open scoped TensorProduct
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
/-- The algebraic first-isomorphism theorem with the source ring structure
fixed by its commutative-ring parent. -/
local instance tensorProductIdealHasQuotient
    (L K' : IntermediateField K Ω) :
    HasQuotient (K' ⊗[K] L) (Ideal (K' ⊗[K] L)) :=
  @Ideal.instHasQuotient (K' ⊗[K] L)
    (inferInstance : CommRing (K' ⊗[K] L)).toRing

Lean source · statement

theorem sup_finrank_over_right_le_left
    (L K' : IntermediateField K Ω)
    [FiniteDimensional K L] [FiniteDimensional K K'] :
    Module.finrank K' (L ⊔ K' : IntermediateField K Ω) ≤
      Module.finrank K L

theorem

sup_finrank_over_left_le_right

L672 ↗

DiscreteValuationField.FieldCompositum.sup_finrank_over_left_le_right

Documentation

Common-top form of the degree bound for L ⊔ K' / L.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
namespace DiscreteValuationField
namespace FieldCompositum
open scoped TensorProduct
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
/-- The algebraic first-isomorphism theorem with the source ring structure
fixed by its commutative-ring parent. -/
local instance tensorProductIdealHasQuotient
    (L K' : IntermediateField K Ω) :
    HasQuotient (K' ⊗[K] L) (Ideal (K' ⊗[K] L)) :=
  @Ideal.instHasQuotient (K' ⊗[K] L)
    (inferInstance : CommRing (K' ⊗[K] L)).toRing

Lean source · statement

theorem sup_finrank_over_left_le_right
    (L K' : IntermediateField K Ω)
    [FiniteDimensional K L] [FiniteDimensional K K'] :
    Module.finrank L (L ⊔ K' : IntermediateField K Ω) ≤
      Module.finrank K K'

theorem

relfinrank_intersection_square

L697 ↗

DiscreteValuationField.FieldCompositum.relfinrank_intersection_square

Documentation

Relative-degree square for a compositum, measured from the intersection L ⊓ K'.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
namespace DiscreteValuationField
namespace FieldCompositum
open scoped TensorProduct
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
/-- The algebraic first-isomorphism theorem with the source ring structure
fixed by its commutative-ring parent. -/
local instance tensorProductIdealHasQuotient
    (L K' : IntermediateField K Ω) :
    HasQuotient (K' ⊗[K] L) (Ideal (K' ⊗[K] L)) :=
  @Ideal.instHasQuotient (K' ⊗[K] L)
    (inferInstance : CommRing (K' ⊗[K] L)).toRing

Lean source · statement

theorem relfinrank_intersection_square
    (L K' : IntermediateField K Ω) :
    (L ⊓ K').relfinrank K' * K'.relfinrank (L ⊔ K') =
      (L ⊓ K').relfinrank L * L.relfinrank (L ⊔ K')

theorem

relfinrank_intersection_extendScalars_square

L717 ↗

DiscreteValuationField.FieldCompositum.relfinrank_intersection_extendScalars_square

Documentation

The same relative-degree square written with base-changed intermediate fields over the right and left compositum branches.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
namespace DiscreteValuationField
namespace FieldCompositum
open scoped TensorProduct
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
/-- The algebraic first-isomorphism theorem with the source ring structure
fixed by its commutative-ring parent. -/
local instance tensorProductIdealHasQuotient
    (L K' : IntermediateField K Ω) :
    HasQuotient (K' ⊗[K] L) (Ideal (K' ⊗[K] L)) :=
  @Ideal.instHasQuotient (K' ⊗[K] L)
    (inferInstance : CommRing (K' ⊗[K] L)).toRing

Lean source · full declaration

theorem relfinrank_intersection_extendScalars_square
    (L K' : IntermediateField K Ω) :
    (L ⊓ K').relfinrank K' *
        Module.finrank K'
          (IntermediateField.extendScalars (show K' ≤ L ⊔ K' from le_sup_right)) =
      (L ⊓ K').relfinrank L *
        Module.finrank L
          (IntermediateField.extendScalars (show L ≤ L ⊔ K' from le_sup_left)) := by
  rw [← IntermediateField.relfinrank_eq_finrank_of_le
      (show K' ≤ L ⊔ K' from le_sup_right),
    ← IntermediateField.relfinrank_eq_finrank_of_le
      (show L ≤ L ⊔ K' from le_sup_left)]
  exact relfinrank_intersection_square L K'

theorem

compositum_finrank_over_right_dvd_intersection_product

L732 ↗

DiscreteValuationField.FieldCompositum.compositum_finrank_over_right_dvd_intersection_product

Documentation

The right compositum degree divides the left intersection-product.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
namespace DiscreteValuationField
namespace FieldCompositum
open scoped TensorProduct
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
/-- The algebraic first-isomorphism theorem with the source ring structure
fixed by its commutative-ring parent. -/
local instance tensorProductIdealHasQuotient
    (L K' : IntermediateField K Ω) :
    HasQuotient (K' ⊗[K] L) (Ideal (K' ⊗[K] L)) :=
  @Ideal.instHasQuotient (K' ⊗[K] L)
    (inferInstance : CommRing (K' ⊗[K] L)).toRing

Lean source · full declaration

theorem compositum_finrank_over_right_dvd_intersection_product
    (L K' : IntermediateField K Ω) :
    Module.finrank K'
        (IntermediateField.extendScalars (show K' ≤ L ⊔ K' from le_sup_right)) ∣
      (L ⊓ K').relfinrank L *
        Module.finrank L
          (IntermediateField.extendScalars (show L ≤ L ⊔ K' from le_sup_left)) := by
  exact dvd_of_mul_left_eq _
    (relfinrank_intersection_extendScalars_square L K')

theorem

compositum_finrank_over_left_dvd_intersection_product

L743 ↗

DiscreteValuationField.FieldCompositum.compositum_finrank_over_left_dvd_intersection_product

Documentation

The left compositum degree divides the symmetric intersection-product.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
namespace DiscreteValuationField
namespace FieldCompositum
open scoped TensorProduct
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
/-- The algebraic first-isomorphism theorem with the source ring structure
fixed by its commutative-ring parent. -/
local instance tensorProductIdealHasQuotient
    (L K' : IntermediateField K Ω) :
    HasQuotient (K' ⊗[K] L) (Ideal (K' ⊗[K] L)) :=
  @Ideal.instHasQuotient (K' ⊗[K] L)
    (inferInstance : CommRing (K' ⊗[K] L)).toRing

Lean source · full declaration

theorem compositum_finrank_over_left_dvd_intersection_product
    (L K' : IntermediateField K Ω) :
    Module.finrank L
        (IntermediateField.extendScalars (show L ≤ L ⊔ K' from le_sup_left)) ∣
      (L ⊓ K').relfinrank K' *
        Module.finrank K'
          (IntermediateField.extendScalars (show K' ≤ L ⊔ K' from le_sup_right)) := by
  exact dvd_of_mul_left_eq _
    (relfinrank_intersection_extendScalars_square L K').symm

theorem

sup_finrank_over_right_dvd_intersection_product

L754 ↗

DiscreteValuationField.FieldCompositum.sup_finrank_over_right_dvd_intersection_product

Documentation

Common-top form of the right branch degree divisibility.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
namespace DiscreteValuationField
namespace FieldCompositum
open scoped TensorProduct
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
/-- The algebraic first-isomorphism theorem with the source ring structure
fixed by its commutative-ring parent. -/
local instance tensorProductIdealHasQuotient
    (L K' : IntermediateField K Ω) :
    HasQuotient (K' ⊗[K] L) (Ideal (K' ⊗[K] L)) :=
  @Ideal.instHasQuotient (K' ⊗[K] L)
    (inferInstance : CommRing (K' ⊗[K] L)).toRing

Lean source · statement

theorem sup_finrank_over_right_dvd_intersection_product
    (L K' : IntermediateField K Ω) :
    Module.finrank K' (L ⊔ K' : IntermediateField K Ω) ∣
      (L ⊓ K').relfinrank L *
        Module.finrank L (L ⊔ K' : IntermediateField K Ω)

theorem

sup_finrank_over_left_dvd_intersection_product

L768 ↗

DiscreteValuationField.FieldCompositum.sup_finrank_over_left_dvd_intersection_product

Documentation

Common-top form of the left branch degree divisibility.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
namespace DiscreteValuationField
namespace FieldCompositum
open scoped TensorProduct
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
/-- The algebraic first-isomorphism theorem with the source ring structure
fixed by its commutative-ring parent. -/
local instance tensorProductIdealHasQuotient
    (L K' : IntermediateField K Ω) :
    HasQuotient (K' ⊗[K] L) (Ideal (K' ⊗[K] L)) :=
  @Ideal.instHasQuotient (K' ⊗[K] L)
    (inferInstance : CommRing (K' ⊗[K] L)).toRing

Lean source · statement

theorem sup_finrank_over_left_dvd_intersection_product
    (L K' : IntermediateField K Ω) :
    Module.finrank L (L ⊔ K' : IntermediateField K Ω) ∣
      (L ⊓ K').relfinrank K' *
        Module.finrank K' (L ⊔ K' : IntermediateField K Ω)

theorem

linearDisjoint_of_finrank_coprime

L783 ↗

DiscreteValuationField.FieldCompositum.linearDisjoint_of_finrank_coprime

Documentation

If two finite-degree intermediate fields have coprime degrees over the base, then they are linearly disjoint over the base.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
namespace DiscreteValuationField
namespace FieldCompositum
open scoped TensorProduct
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
/-- The algebraic first-isomorphism theorem with the source ring structure
fixed by its commutative-ring parent. -/
local instance tensorProductIdealHasQuotient
    (L K' : IntermediateField K Ω) :
    HasQuotient (K' ⊗[K] L) (Ideal (K' ⊗[K] L)) :=
  @Ideal.instHasQuotient (K' ⊗[K] L)
    (inferInstance : CommRing (K' ⊗[K] L)).toRing

Lean source · statement

theorem linearDisjoint_of_finrank_coprime
    (L K' : IntermediateField K Ω)
    (hcop : Nat.Coprime (Module.finrank K L) (Module.finrank K K')) :
    L.LinearDisjoint K'

theorem

compositum_finrank_over_right_eq_left_of_linearDisjoint

L791 ↗

DiscreteValuationField.FieldCompositum.compositum_finrank_over_right_eq_left_of_linearDisjoint

Documentation

Under linear disjointness, the degree of L K' / K' equals the degree of L / K.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
namespace DiscreteValuationField
namespace FieldCompositum
open scoped TensorProduct
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
/-- The algebraic first-isomorphism theorem with the source ring structure
fixed by its commutative-ring parent. -/
local instance tensorProductIdealHasQuotient
    (L K' : IntermediateField K Ω) :
    HasQuotient (K' ⊗[K] L) (Ideal (K' ⊗[K] L)) :=
  @Ideal.instHasQuotient (K' ⊗[K] L)
    (inferInstance : CommRing (K' ⊗[K] L)).toRing

Lean source · full declaration

theorem compositum_finrank_over_right_eq_left_of_linearDisjoint
    (L K' : IntermediateField K Ω)
    [FiniteDimensional K K']
    (hlin : L.LinearDisjoint K') :
    Module.finrank K'
        (IntermediateField.extendScalars (show K' ≤ L ⊔ K' from le_sup_right)) =
      Module.finrank K L := by
  have hformula := right_finrank_mul_compositum_finrank (K := K) (Ω := Ω) L K'
  have hsup := hlin.finrank_sup
  have hmul :
      Module.finrank K K' *
          Module.finrank K'
            (IntermediateField.extendScalars (show K' ≤ L ⊔ K' from le_sup_right)) =
        Module.finrank K K' * Module.finrank K L := by
    calc
      Module.finrank K K' *
          Module.finrank K'
            (IntermediateField.extendScalars (show K' ≤ L ⊔ K' from le_sup_right)) =
          Module.finrank K (L ⊔ K' : IntermediateField K Ω) := hformula
      _ = Module.finrank K L * Module.finrank K K' := hsup
      _ = Module.finrank K K' * Module.finrank K L := by rw [mul_comm]
  exact Nat.mul_left_cancel (Module.finrank_pos (R := K) (M := K')) hmul

theorem

compositum_finrank_over_left_eq_right_of_linearDisjoint

L816 ↗

DiscreteValuationField.FieldCompositum.compositum_finrank_over_left_eq_right_of_linearDisjoint

Documentation

Under linear disjointness, the degree of L K' / L equals the degree of K' / K.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
namespace DiscreteValuationField
namespace FieldCompositum
open scoped TensorProduct
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
/-- The algebraic first-isomorphism theorem with the source ring structure
fixed by its commutative-ring parent. -/
local instance tensorProductIdealHasQuotient
    (L K' : IntermediateField K Ω) :
    HasQuotient (K' ⊗[K] L) (Ideal (K' ⊗[K] L)) :=
  @Ideal.instHasQuotient (K' ⊗[K] L)
    (inferInstance : CommRing (K' ⊗[K] L)).toRing

Lean source · full declaration

theorem compositum_finrank_over_left_eq_right_of_linearDisjoint
    (L K' : IntermediateField K Ω)
    [FiniteDimensional K L]
    (hlin : L.LinearDisjoint K') :
    Module.finrank L
        (IntermediateField.extendScalars (show L ≤ L ⊔ K' from le_sup_left)) =
      Module.finrank K K' := by
  have hformula := left_finrank_mul_compositum_finrank (K := K) (Ω := Ω) L K'
  have hsup := hlin.finrank_sup
  have hmul :
      Module.finrank K L *
          Module.finrank L
            (IntermediateField.extendScalars (show L ≤ L ⊔ K' from le_sup_left)) =
        Module.finrank K L * Module.finrank K K' := by
    calc
      Module.finrank K L *
          Module.finrank L
            (IntermediateField.extendScalars (show L ≤ L ⊔ K' from le_sup_left)) =
          Module.finrank K (L ⊔ K' : IntermediateField K Ω) := hformula
      _ = Module.finrank K L * Module.finrank K K' := hsup
  exact Nat.mul_left_cancel (Module.finrank_pos (R := K) (M := L)) hmul

theorem

sup_finrank_over_right_eq_left_of_linearDisjoint

L840 ↗

DiscreteValuationField.FieldCompositum.sup_finrank_over_right_eq_left_of_linearDisjoint

Documentation

Common-top form of the degree equality for L ⊔ K' / K' under linear disjointness.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
namespace DiscreteValuationField
namespace FieldCompositum
open scoped TensorProduct
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
/-- The algebraic first-isomorphism theorem with the source ring structure
fixed by its commutative-ring parent. -/
local instance tensorProductIdealHasQuotient
    (L K' : IntermediateField K Ω) :
    HasQuotient (K' ⊗[K] L) (Ideal (K' ⊗[K] L)) :=
  @Ideal.instHasQuotient (K' ⊗[K] L)
    (inferInstance : CommRing (K' ⊗[K] L)).toRing

Lean source · statement

theorem sup_finrank_over_right_eq_left_of_linearDisjoint
    (L K' : IntermediateField K Ω)
    [FiniteDimensional K L] [FiniteDimensional K K']
    (hlin : L.LinearDisjoint K') :
    Module.finrank K' (L ⊔ K' : IntermediateField K Ω) =
      Module.finrank K L

theorem

sup_finrank_over_left_eq_right_of_linearDisjoint

L866 ↗

DiscreteValuationField.FieldCompositum.sup_finrank_over_left_eq_right_of_linearDisjoint

Documentation

Common-top form of the degree equality for L ⊔ K' / L under linear disjointness.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
namespace DiscreteValuationField
namespace FieldCompositum
open scoped TensorProduct
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
/-- The algebraic first-isomorphism theorem with the source ring structure
fixed by its commutative-ring parent. -/
local instance tensorProductIdealHasQuotient
    (L K' : IntermediateField K Ω) :
    HasQuotient (K' ⊗[K] L) (Ideal (K' ⊗[K] L)) :=
  @Ideal.instHasQuotient (K' ⊗[K] L)
    (inferInstance : CommRing (K' ⊗[K] L)).toRing

Lean source · statement

theorem sup_finrank_over_left_eq_right_of_linearDisjoint
    (L K' : IntermediateField K Ω)
    [FiniteDimensional K L] [FiniteDimensional K K']
    (hlin : L.LinearDisjoint K') :
    Module.finrank L (L ⊔ K' : IntermediateField K Ω) =
      Module.finrank K K'

theorem

compositum_finrank_over_right_eq_left_of_finrank_coprime

L890 ↗

DiscreteValuationField.FieldCompositum.compositum_finrank_over_right_eq_left_of_finrank_coprime

Documentation

Coprime-degree form of the degree equality for L K' / K'.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
namespace DiscreteValuationField
namespace FieldCompositum
open scoped TensorProduct
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
/-- The algebraic first-isomorphism theorem with the source ring structure
fixed by its commutative-ring parent. -/
local instance tensorProductIdealHasQuotient
    (L K' : IntermediateField K Ω) :
    HasQuotient (K' ⊗[K] L) (Ideal (K' ⊗[K] L)) :=
  @Ideal.instHasQuotient (K' ⊗[K] L)
    (inferInstance : CommRing (K' ⊗[K] L)).toRing

Lean source · full declaration

theorem compositum_finrank_over_right_eq_left_of_finrank_coprime
    (L K' : IntermediateField K Ω)
    [FiniteDimensional K K']
    (hcop : Nat.Coprime (Module.finrank K L) (Module.finrank K K')) :
    Module.finrank K'
        (IntermediateField.extendScalars (show K' ≤ L ⊔ K' from le_sup_right)) =
      Module.finrank K L :=
  compositum_finrank_over_right_eq_left_of_linearDisjoint L K'
    (linearDisjoint_of_finrank_coprime L K' hcop)

theorem

compositum_finrank_over_left_eq_right_of_finrank_coprime

L901 ↗

DiscreteValuationField.FieldCompositum.compositum_finrank_over_left_eq_right_of_finrank_coprime

Documentation

Coprime-degree form of the degree equality for L K' / L.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
namespace DiscreteValuationField
namespace FieldCompositum
open scoped TensorProduct
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
/-- The algebraic first-isomorphism theorem with the source ring structure
fixed by its commutative-ring parent. -/
local instance tensorProductIdealHasQuotient
    (L K' : IntermediateField K Ω) :
    HasQuotient (K' ⊗[K] L) (Ideal (K' ⊗[K] L)) :=
  @Ideal.instHasQuotient (K' ⊗[K] L)
    (inferInstance : CommRing (K' ⊗[K] L)).toRing

Lean source · full declaration

theorem compositum_finrank_over_left_eq_right_of_finrank_coprime
    (L K' : IntermediateField K Ω)
    [FiniteDimensional K L]
    (hcop : Nat.Coprime (Module.finrank K L) (Module.finrank K K')) :
    Module.finrank L
        (IntermediateField.extendScalars (show L ≤ L ⊔ K' from le_sup_left)) =
      Module.finrank K K' :=
  compositum_finrank_over_left_eq_right_of_linearDisjoint L K'
    (linearDisjoint_of_finrank_coprime L K' hcop)

theorem

sup_finrank_over_right_eq_left_of_finrank_coprime

L912 ↗

DiscreteValuationField.FieldCompositum.sup_finrank_over_right_eq_left_of_finrank_coprime

Documentation

Common-top coprime-degree form of the degree equality for L ⊔ K' / K'.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
namespace DiscreteValuationField
namespace FieldCompositum
open scoped TensorProduct
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
/-- The algebraic first-isomorphism theorem with the source ring structure
fixed by its commutative-ring parent. -/
local instance tensorProductIdealHasQuotient
    (L K' : IntermediateField K Ω) :
    HasQuotient (K' ⊗[K] L) (Ideal (K' ⊗[K] L)) :=
  @Ideal.instHasQuotient (K' ⊗[K] L)
    (inferInstance : CommRing (K' ⊗[K] L)).toRing

Lean source · statement

theorem sup_finrank_over_right_eq_left_of_finrank_coprime
    (L K' : IntermediateField K Ω)
    [FiniteDimensional K L] [FiniteDimensional K K']
    (hcop : Nat.Coprime (Module.finrank K L) (Module.finrank K K')) :
    Module.finrank K' (L ⊔ K' : IntermediateField K Ω) =
      Module.finrank K L

theorem

sup_finrank_over_left_eq_right_of_finrank_coprime

L922 ↗

DiscreteValuationField.FieldCompositum.sup_finrank_over_left_eq_right_of_finrank_coprime

Documentation

Common-top coprime-degree form of the degree equality for L ⊔ K' / L.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
namespace DiscreteValuationField
namespace FieldCompositum
open scoped TensorProduct
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
/-- The algebraic first-isomorphism theorem with the source ring structure
fixed by its commutative-ring parent. -/
local instance tensorProductIdealHasQuotient
    (L K' : IntermediateField K Ω) :
    HasQuotient (K' ⊗[K] L) (Ideal (K' ⊗[K] L)) :=
  @Ideal.instHasQuotient (K' ⊗[K] L)
    (inferInstance : CommRing (K' ⊗[K] L)).toRing

Lean source · statement

theorem sup_finrank_over_left_eq_right_of_finrank_coprime
    (L K' : IntermediateField K Ω)
    [FiniteDimensional K L] [FiniteDimensional K K']
    (hcop : Nat.Coprime (Module.finrank K L) (Module.finrank K K')) :
    Module.finrank L (L ⊔ K' : IntermediateField K Ω) =
      Module.finrank K K'

theorem

isSeparable_sup_over_right_of_left

L937 ↗

DiscreteValuationField.FieldCompositum.isSeparable_sup_over_right_of_left

Documentation

Field-level source for unramified base change: after arbitrary finite base change K'/K, the common top L ⊔ K' is separable over K' as soon as L/K is separable.

This uses formal unramifiedness of separable field extensions, stability under base change, and the surjective product map K' ⊗_K L -> L ⊔ K'.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
namespace DiscreteValuationField
namespace FieldCompositum
open scoped TensorProduct
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
/-- The algebraic first-isomorphism theorem with the source ring structure
fixed by its commutative-ring parent. -/
local instance tensorProductIdealHasQuotient
    (L K' : IntermediateField K Ω) :
    HasQuotient (K' ⊗[K] L) (Ideal (K' ⊗[K] L)) :=
  @Ideal.instHasQuotient (K' ⊗[K] L)
    (inferInstance : CommRing (K' ⊗[K] L)).toRing

Lean source · statement

theorem isSeparable_sup_over_right_of_left
    (L K' : IntermediateField K Ω)
    [FiniteDimensional K L] [FiniteDimensional K K']
    [Algebra.IsSeparable K L] :
    Algebra.IsSeparable K' (L ⊔ K' : IntermediateField K Ω)

theorem

isSeparable_compositum_over_right

L964 ↗

DiscreteValuationField.FieldCompositum.isSeparable_compositum_over_right

Documentation

The compositum is separable over the right factor after arbitrary finite base change, provided the left factor is separable over the base.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
namespace DiscreteValuationField
namespace FieldCompositum
open scoped TensorProduct
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
/-- The algebraic first-isomorphism theorem with the source ring structure
fixed by its commutative-ring parent. -/
local instance tensorProductIdealHasQuotient
    (L K' : IntermediateField K Ω) :
    HasQuotient (K' ⊗[K] L) (Ideal (K' ⊗[K] L)) :=
  @Ideal.instHasQuotient (K' ⊗[K] L)
    (inferInstance : CommRing (K' ⊗[K] L)).toRing

Lean source · full declaration

theorem isSeparable_compositum_over_right
    (L K' : IntermediateField K Ω)
    [FiniteDimensional K L] [FiniteDimensional K K']
    [Algebra.IsSeparable K L] :
    Algebra.IsSeparable K'
      (IntermediateField.extendScalars (show K' ≤ L ⊔ K' from le_sup_right)) := by
  change Algebra.IsSeparable K' (L ⊔ K' : IntermediateField K Ω)
  exact isSeparable_sup_over_right_of_left L K'

theorem

isSeparable_compositum_over_left

L974 ↗

DiscreteValuationField.FieldCompositum.isSeparable_compositum_over_left

Documentation

Symmetric separability statement for the compositum over the left factor.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
namespace DiscreteValuationField
namespace FieldCompositum
open scoped TensorProduct
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
/-- The algebraic first-isomorphism theorem with the source ring structure
fixed by its commutative-ring parent. -/
local instance tensorProductIdealHasQuotient
    (L K' : IntermediateField K Ω) :
    HasQuotient (K' ⊗[K] L) (Ideal (K' ⊗[K] L)) :=
  @Ideal.instHasQuotient (K' ⊗[K] L)
    (inferInstance : CommRing (K' ⊗[K] L)).toRing

Lean source · full declaration

theorem isSeparable_compositum_over_left
    (L K' : IntermediateField K Ω)
    [Algebra.IsSeparable K L] [Algebra.IsSeparable K K'] :
    Algebra.IsSeparable L
      (IntermediateField.extendScalars (show L ≤ L ⊔ K' from le_sup_left)) := by
  have : Algebra.IsSeparable K
      (IntermediateField.extendScalars (show L ≤ L ⊔ K' from le_sup_left)) := by
    change Algebra.IsSeparable K
      ((IntermediateField.extendScalars
        (show L ≤ L ⊔ K' from le_sup_left)).restrictScalars K)
    rw [IntermediateField.extendScalars_restrictScalars]
    infer_instance
  exact Algebra.isSeparable_tower_top_of_isSeparable K L
    (IntermediateField.extendScalars (show L ≤ L ⊔ K' from le_sup_left))

theorem

isSeparable_sup_over_right

L991 ↗

DiscreteValuationField.FieldCompositum.isSeparable_sup_over_right

Documentation

The common top field is separable over the right factor after arbitrary finite base change, provided the left factor is separable over the base.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
namespace DiscreteValuationField
namespace FieldCompositum
open scoped TensorProduct
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
/-- The algebraic first-isomorphism theorem with the source ring structure
fixed by its commutative-ring parent. -/
local instance tensorProductIdealHasQuotient
    (L K' : IntermediateField K Ω) :
    HasQuotient (K' ⊗[K] L) (Ideal (K' ⊗[K] L)) :=
  @Ideal.instHasQuotient (K' ⊗[K] L)
    (inferInstance : CommRing (K' ⊗[K] L)).toRing

Lean source · statement

theorem isSeparable_sup_over_right
    (L K' : IntermediateField K Ω)
    [FiniteDimensional K L] [FiniteDimensional K K']
    [Algebra.IsSeparable K L] :
    Algebra.IsSeparable K' (L ⊔ K' : IntermediateField K Ω)

theorem

isSeparable_sup_over_left

L1000 ↗

DiscreteValuationField.FieldCompositum.isSeparable_sup_over_left

Documentation

The common top field is separable over the left factor when both factors are separable over the base.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v
namespace DiscreteValuationField
namespace FieldCompositum
open scoped TensorProduct
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
/-- The algebraic first-isomorphism theorem with the source ring structure
fixed by its commutative-ring parent. -/
local instance tensorProductIdealHasQuotient
    (L K' : IntermediateField K Ω) :
    HasQuotient (K' ⊗[K] L) (Ideal (K' ⊗[K] L)) :=
  @Ideal.instHasQuotient (K' ⊗[K] L)
    (inferInstance : CommRing (K' ⊗[K] L)).toRing

Lean source · statement

theorem isSeparable_sup_over_left
    (L K' : IntermediateField K Ω)
    [Algebra.IsSeparable K L] [Algebra.IsSeparable K K'] :
    Algebra.IsSeparable L (L ⊔ K' : IntermediateField K Ω)

Module documentation

Field-theoretic composita for finite valued extensions

Declarations