NYLL
Module

Basic.lean

Nyll.EtaleFundamentalGroups.GenericTensor.FieldComponent.Basic
22 declarations indexed from sourceView source ↗

Module documentation

Field components of a generic tensor product

Let K' / K be any field extension and let L / K be finite. A maximal ideal of K' ⊗_K L selects a field component. This file constructs the two canonical embeddings into that component, proves that their images generate the component, and records finiteness. If L / K is Galois, the selected component is Galois over K'.

The generation statement is what keeps this construction tied to the chosen maximal ideal: the quotient map itself is the product map of the two canonical embeddings. A later integral-localization argument can therefore supply a specific maximal ideal and retain its chosen-prime compatibility.

Imports2
Imported by11

Declarations

abbrev

GenericTensorFieldComponent

L38 ↗
EtaleFundamentalGroups.GenericTensorFieldComponent
Documentation

The field component of K' ⊗_K L selected by a maximal ideal.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe u v w
variable {K : Type u} {K' : Type v} {L : Type w}
variable [Field K] [Field K'] [Field L]
variable [Algebra K K'] [Algebra K L]
Lean source · statement
abbrev GenericTensorFieldComponent
    (m : Ideal (K' ⊗[K] L))
instance

genericTensorFieldComponentField

L42 ↗
EtaleFundamentalGroups.genericTensorFieldComponentField
Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe u v w
variable {K : Type u} {K' : Type v} {L : Type w}
variable [Field K] [Field K'] [Field L]
variable [Algebra K K'] [Algebra K L]
Lean source · statement
instance genericTensorFieldComponentField
    (m : Ideal (K' ⊗[K] L)) [m.IsMaximal] :
    Field (GenericTensorFieldComponent m)
def

genericTensorFieldComponentLeft

L48 ↗
EtaleFundamentalGroups.genericTensorFieldComponentLeft
Documentation

The canonical copy of the left factor in the selected component.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe u v w
variable {K : Type u} {K' : Type v} {L : Type w}
variable [Field K] [Field K'] [Field L]
variable [Algebra K K'] [Algebra K L]
Lean source · statement
def genericTensorFieldComponentLeft
    (m : Ideal (K' ⊗[K] L)) [m.IsMaximal] :
    K' →ₐ[K] GenericTensorFieldComponent m
def

genericTensorFieldComponentRight

L55 ↗
EtaleFundamentalGroups.genericTensorFieldComponentRight
Documentation

The canonical copy of the right factor in the selected component.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe u v w
variable {K : Type u} {K' : Type v} {L : Type w}
variable [Field K] [Field K'] [Field L]
variable [Algebra K K'] [Algebra K L]
Lean source · statement
def genericTensorFieldComponentRight
    (m : Ideal (K' ⊗[K] L)) [m.IsMaximal] :
    L →ₐ[K] GenericTensorFieldComponent m
def

genericTensorFieldComponentRightAlgebra

L66 ↗
EtaleFundamentalGroups.genericTensorFieldComponentRightAlgebra
Documentation

The algebra structure on a selected tensor component induced by the right tensor factor. It is kept explicit rather than installed globally, because the same component already carries its canonical algebra structure over the left tensor factor.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe u v w
variable {K : Type u} {K' : Type v} {L : Type w}
variable [Field K] [Field K'] [Field L]
variable [Algebra K K'] [Algebra K L]
Lean source · statement
def genericTensorFieldComponentRightAlgebra
    (m : Ideal (K' ⊗[K] L)) [m.IsMaximal] :
    Algebra L (GenericTensorFieldComponent m)
theorem

genericTensorFieldComponentRight_eq_algebraMap

L73 ↗
EtaleFundamentalGroups.genericTensorFieldComponentRight_eq_algebraMap
Documentation

With the explicit right-factor algebra structure, its algebra map is literally the canonical right tensor-factor embedding.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe u v w
variable {K : Type u} {K' : Type v} {L : Type w}
variable [Field K] [Field K'] [Field L]
variable [Algebra K K'] [Algebra K L]
Lean source · full declaration
theorem genericTensorFieldComponentRight_eq_algebraMap
    (m : Ideal (K' ⊗[K] L)) [m.IsMaximal] :
    letI : Algebra L (GenericTensorFieldComponent m) :=
      genericTensorFieldComponentRightAlgebra m
    genericTensorFieldComponentRight m =
      IsScalarTower.toAlgHom K L (GenericTensorFieldComponent m) := by
  rfl
theorem

genericTensorFieldComponent_right_isScalarTower

L83 ↗
EtaleFundamentalGroups.genericTensorFieldComponent_right_isScalarTower
Documentation

The direct K-algebra structure on a selected component agrees with the one obtained through the canonical copy of the right tensor factor.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe u v w
variable {K : Type u} {K' : Type v} {L : Type w}
variable [Field K] [Field K'] [Field L]
variable [Algebra K K'] [Algebra K L]
Lean source · full declaration
theorem genericTensorFieldComponent_right_isScalarTower
    (m : Ideal (K' ⊗[K] L)) [m.IsMaximal] :
    letI : Algebra L (GenericTensorFieldComponent m) :=
      genericTensorFieldComponentRightAlgebra m
    IsScalarTower K L (GenericTensorFieldComponent m) := by
  let : Algebra L (GenericTensorFieldComponent m) :=
    genericTensorFieldComponentRightAlgebra m
  apply IsScalarTower.of_algebraMap_eq
  intro x
  change Ideal.Quotient.mk m
      ((Algebra.TensorProduct.includeLeft : K' →ₐ[K] K' ⊗[K] L)
        (algebraMap K K' x)) =
    Ideal.Quotient.mk m
      ((Algebra.TensorProduct.includeRight : L →ₐ[K] K' ⊗[K] L)
        (algebraMap K L x))
  exact congrArg (Ideal.Quotient.mk m)
    (DFunLike.congr_fun
      Algebra.TensorProduct.includeLeftRingHom_comp_algebraMap x)
theorem

genericTensorFieldComponentLeft_apply

L103 ↗
EtaleFundamentalGroups.genericTensorFieldComponentLeft_apply
Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe u v w
variable {K : Type u} {K' : Type v} {L : Type w}
variable [Field K] [Field K'] [Field L]
variable [Algebra K K'] [Algebra K L]
Lean source · statement
theorem genericTensorFieldComponentLeft_apply
    (m : Ideal (K' ⊗[K] L)) [m.IsMaximal] (x : K') :
    genericTensorFieldComponentLeft m x =
      Ideal.Quotient.mk m
        ((Algebra.TensorProduct.includeLeft : K' →ₐ[K] K' ⊗[K] L) x)
theorem

genericTensorFieldComponentRight_apply

L111 ↗
EtaleFundamentalGroups.genericTensorFieldComponentRight_apply
Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe u v w
variable {K : Type u} {K' : Type v} {L : Type w}
variable [Field K] [Field K'] [Field L]
variable [Algebra K K'] [Algebra K L]
Lean source · statement
theorem genericTensorFieldComponentRight_apply
    (m : Ideal (K' ⊗[K] L)) [m.IsMaximal] (x : L) :
    genericTensorFieldComponentRight m x =
      Ideal.Quotient.mk m
        ((Algebra.TensorProduct.includeRight : L →ₐ[K] K' ⊗[K] L) x)
theorem

genericTensorFieldComponentLeft_eq_algebraMap

L119 ↗
EtaleFundamentalGroups.genericTensorFieldComponentLeft_eq_algebraMap
Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe u v w
variable {K : Type u} {K' : Type v} {L : Type w}
variable [Field K] [Field K'] [Field L]
variable [Algebra K K'] [Algebra K L]
Lean source · statement
theorem genericTensorFieldComponentLeft_eq_algebraMap
    (m : Ideal (K' ⊗[K] L)) [m.IsMaximal] (x : K') :
    genericTensorFieldComponentLeft m x =
      algebraMap K' (GenericTensorFieldComponent m) x
theorem

genericTensorFieldComponent_isScalarTower

L127 ↗
EtaleFundamentalGroups.genericTensorFieldComponent_isScalarTower
Documentation

The direct K-algebra structure on the quotient agrees with the one obtained through its canonical copy of K'.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe u v w
variable {K : Type u} {K' : Type v} {L : Type w}
variable [Field K] [Field K'] [Field L]
variable [Algebra K K'] [Algebra K L]
Lean source · statement
theorem genericTensorFieldComponent_isScalarTower
    (m : Ideal (K' ⊗[K] L)) [m.IsMaximal] :
    IsScalarTower K K' (GenericTensorFieldComponent m)
theorem

genericTensorFieldComponent_productMap_eq_quotient

L136 ↗
EtaleFundamentalGroups.genericTensorFieldComponent_productMap_eq_quotient
Documentation

The product map of the two canonical embeddings is literally the quotient map belonging to the specified maximal ideal.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe u v w
variable {K : Type u} {K' : Type v} {L : Type w}
variable [Field K] [Field K'] [Field L]
variable [Algebra K K'] [Algebra K L]
Lean source · statement
theorem genericTensorFieldComponent_productMap_eq_quotient
    (m : Ideal (K' ⊗[K] L)) [m.IsMaximal] :
    Algebra.TensorProduct.productMap
        (genericTensorFieldComponentLeft m)
        (genericTensorFieldComponentRight m) =
      Ideal.Quotient.mkₐ K m
theorem

genericTensorFieldComponent_productMap_ker

L156 ↗
EtaleFundamentalGroups.genericTensorFieldComponent_productMap_ker
Documentation

Consequently the selected maximal ideal is exactly the kernel of the canonical product map into its field component.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe u v w
variable {K : Type u} {K' : Type v} {L : Type w}
variable [Field K] [Field K'] [Field L]
variable [Algebra K K'] [Algebra K L]
Lean source · statement
theorem genericTensorFieldComponent_productMap_ker
    (m : Ideal (K' ⊗[K] L)) [m.IsMaximal] :
    RingHom.ker
        (Algebra.TensorProduct.productMap
          (genericTensorFieldComponentLeft m)
          (genericTensorFieldComponentRight m)).toRingHom = m
theorem

genericTensorFieldComponentLeft_injective

L166 ↗
EtaleFundamentalGroups.genericTensorFieldComponentLeft_injective
Documentation

Both field factors embed in every selected tensor component.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe u v w
variable {K : Type u} {K' : Type v} {L : Type w}
variable [Field K] [Field K'] [Field L]
variable [Algebra K K'] [Algebra K L]
Lean source · statement
theorem genericTensorFieldComponentLeft_injective
    (m : Ideal (K' ⊗[K] L)) [m.IsMaximal] :
    Function.Injective (genericTensorFieldComponentLeft m)
theorem

genericTensorFieldComponentRight_injective

L172 ↗
EtaleFundamentalGroups.genericTensorFieldComponentRight_injective
Documentation

Both field factors embed in every selected tensor component.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe u v w
variable {K : Type u} {K' : Type v} {L : Type w}
variable [Field K] [Field K'] [Field L]
variable [Algebra K K'] [Algebra K L]
Lean source · statement
theorem genericTensorFieldComponentRight_injective
    (m : Ideal (K' ⊗[K] L)) [m.IsMaximal] :
    Function.Injective (genericTensorFieldComponentRight m)
theorem

genericTensorFieldComponent_fieldRange_sup_eq_top

L182 ↗
EtaleFundamentalGroups.genericTensorFieldComponent_fieldRange_sup_eq_top
Documentation

The images of K' and L generate the field component selected by m.

This is proved directly from surjectivity of the quotient map, so it retains the identity of the specified maximal ideal rather than replacing the component by an abstract common overfield.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe u v w
variable {K : Type u} {K' : Type v} {L : Type w}
variable [Field K] [Field K'] [Field L]
variable [Algebra K K'] [Algebra K L]
Lean source · statement
theorem genericTensorFieldComponent_fieldRange_sup_eq_top
    (m : Ideal (K' ⊗[K] L)) [m.IsMaximal] :
    (genericTensorFieldComponentLeft m).fieldRange ⊔
        (genericTensorFieldComponentRight m).fieldRange = ⊤
instance

genericTensorFieldComponentFiniteDimensional

L218 ↗
EtaleFundamentalGroups.genericTensorFieldComponentFiniteDimensional
Documentation

A selected component is finite over the left tensor factor whenever the right tensor factor is finite over the original base.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe u v w
variable {K : Type u} {K' : Type v} {L : Type w}
variable [Field K] [Field K'] [Field L]
variable [Algebra K K'] [Algebra K L]
Lean source · statement
instance genericTensorFieldComponentFiniteDimensional
    (m : Ideal (K' ⊗[K] L)) [m.IsMaximal]
    [FiniteDimensional K L] :
    FiniteDimensional K' (GenericTensorFieldComponent m)
instance

genericTensorFieldComponentIsSeparable

L262 ↗
EtaleFundamentalGroups.genericTensorFieldComponentIsSeparable
Documentation

Separability also survives passage to an arbitrary selected component.

This is the quotient-component version of the CFT compositum theorem DiscreteValuationField.FieldCompositum.isSeparable_sup_over_right_of_left; the formally-unramified base-change proof removes any finiteness requirement on K' / K.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe u v w
variable {K : Type u} {K' : Type v} {L : Type w}
variable [Field K] [Field K'] [Field L]
variable [Algebra K K'] [Algebra K L]
Lean source · statement
instance genericTensorFieldComponentIsSeparable
    (m : Ideal (K' ⊗[K] L)) [m.IsMaximal]
    [FiniteDimensional K L] [Algebra.IsSeparable K L] :
    Algebra.IsSeparable K' (GenericTensorFieldComponent m)
instance

genericTensorFieldComponentIsGalois

L284 ↗
EtaleFundamentalGroups.genericTensorFieldComponentIsGalois
Documentation

A field component of the base change of a finite Galois extension is Galois over the new base field.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe u v w
variable {K : Type u} {K' : Type v} {L : Type w}
variable [Field K] [Field K'] [Field L]
variable [Algebra K K'] [Algebra K L]
Lean source · statement
instance genericTensorFieldComponentIsGalois
    (m : Ideal (K' ⊗[K] L)) [m.IsMaximal]
    [FiniteDimensional K L] [IsGalois K L] :
    IsGalois K' (GenericTensorFieldComponent m)
theorem

genericTensorFieldComponentFiniteDimensionalOverRight

L323 ↗
EtaleFundamentalGroups.genericTensorFieldComponentFiniteDimensionalOverRight
Documentation

A selected component is finite over the right tensor factor whenever the left tensor factor is finite over the original base. This is the right-hand counterpart of genericTensorFieldComponentFiniteDimensional; it is stated as an explicit producer to avoid installing a second global algebra structure on the quotient component.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe u v w
variable {K : Type u} {K' : Type v} {L : Type w}
variable [Field K] [Field K'] [Field L]
variable [Algebra K K'] [Algebra K L]
Lean source · full declaration
theorem genericTensorFieldComponentFiniteDimensionalOverRight
    (m : Ideal (K' ⊗[K] L)) [m.IsMaximal]
    [FiniteDimensional K K'] :
    letI : Algebra L (GenericTensorFieldComponent m) :=
      genericTensorFieldComponentRightAlgebra m
    FiniteDimensional L (GenericTensorFieldComponent m) := by
  let : Algebra L (GenericTensorFieldComponent m) :=
    genericTensorFieldComponentRightAlgebra m
  let T := K' ⊗[K] L
  let : Algebra L T := Algebra.TensorProduct.rightAlgebra
  let e : (L ⊗[K] K') ≃ₐ[L] T :=
    Algebra.TensorProduct.commRight K L K'
  let : Module.Finite L (L ⊗[K] K') :=
    Module.Finite.base_change K L K'
  let : Module.Finite L T := Module.Finite.equiv e.toLinearEquiv
  let q : T →ₐ[L] GenericTensorFieldComponent m :=
    Ideal.Quotient.mkₐ L m
  exact Module.Finite.of_surjective q.toLinearMap
    Ideal.Quotient.mk_surjective
def

genericTensorMaximalIdeal

L345 ↗
EtaleFundamentalGroups.genericTensorMaximalIdeal
Documentation

A canonical maximal ideal, used when no previously chosen integral prime specifies a component.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe u v w
variable {K : Type u} {K' : Type v} {L : Type w}
variable [Field K] [Field K'] [Field L]
variable [Algebra K K'] [Algebra K L]
Lean source · statement
def genericTensorMaximalIdeal : Ideal (K' ⊗[K] L)
instance

genericTensorMaximalIdeal_isMaximal

L348 ↗
EtaleFundamentalGroups.genericTensorMaximalIdeal_isMaximal
Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe u v w
variable {K : Type u} {K' : Type v} {L : Type w}
variable [Field K] [Field K'] [Field L]
variable [Algebra K K'] [Algebra K L]
Lean source · statement
instance genericTensorMaximalIdeal_isMaximal :
    (genericTensorMaximalIdeal (K := K) (K' := K') (L := L)).IsMaximal

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.