NYLL
Module

OfFieldTower.lean

Nyll.EtaleFundamentalGroups.GenericTensor.FieldComponent.OfFieldTower
9 declarations indexed from sourceView source ↗

Module documentation

The tensor component selected by an existing field-tower action

If K' already acts on L over K, multiplication gives a surjective map K' ⊗[K] L → L. Its kernel is therefore a maximal ideal, and the corresponding generic tensor component is canonically L as a K'-algebra.

This is the component-selection producer used when a radical fraction field has been embedded in the chosen normalization field. The component and its comparison equivalence are constructed from that action; neither is an additional choice or an assumed comparison.

Imports1
Imported by6

Declarations

def

fieldTowerTensorProductMap

L36 ↗
EtaleFundamentalGroups.fieldTowerTensorProductMap
Documentation

Multiplication after the given K'-action on L.

Source context 8 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uB uK uK' uL
variable {K : Type uK} {K' : Type uK'} {L : Type uL}
variable [Field K] [Field K'] [Field L]
variable [Algebra K K'] [Algebra K L]
variable [Algebra K' L] [IsScalarTower K K' L]
Lean source · statement
def fieldTowerTensorProductMap :
    (K' ⊗[K] L) →ₐ[K'] L
def

fieldTowerTensorComponentIdeal

L49 ↗
EtaleFundamentalGroups.fieldTowerTensorComponentIdeal
Documentation

The tensor component cut out by the existing K'-action on L.

Source context 8 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uB uK uK' uL
variable {K : Type uK} {K' : Type uK'} {L : Type uL}
variable [Field K] [Field K'] [Field L]
variable [Algebra K K'] [Algebra K L]
variable [Algebra K' L] [IsScalarTower K K' L]
Lean source · statement
def fieldTowerTensorComponentIdeal : Ideal (K' ⊗[K] L)
theorem

fieldTowerTensorProductMap_surjective

L56 ↗
EtaleFundamentalGroups.fieldTowerTensorProductMap_surjective
Documentation

The multiplication map is onto, since every l : L is the image of 1 ⊗ l.

Source context 8 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uB uK uK' uL
variable {K : Type uK} {K' : Type uK'} {L : Type uL}
variable [Field K] [Field K'] [Field L]
variable [Algebra K K'] [Algebra K L]
variable [Algebra K' L] [IsScalarTower K K' L]
Lean source · statement
theorem fieldTowerTensorProductMap_surjective :
    Function.Surjective
      (fieldTowerTensorProductMap (K := K) (K' := K') (L := L))
theorem

fieldTowerTensorComponentIdeal_isMaximal

L65 ↗
EtaleFundamentalGroups.fieldTowerTensorComponentIdeal_isMaximal
Documentation

The kernel of multiplication selects an actual field component.

Source context 8 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uB uK uK' uL
variable {K : Type uK} {K' : Type uK'} {L : Type uL}
variable [Field K] [Field K'] [Field L]
variable [Algebra K K'] [Algebra K L]
variable [Algebra K' L] [IsScalarTower K K' L]
Lean source · statement
theorem fieldTowerTensorComponentIdeal_isMaximal :
    (fieldTowerTensorComponentIdeal
      (K := K) (K' := K') (L := L)).IsMaximal
def

fieldTowerTensorComponentAlgEquiv

L75 ↗
EtaleFundamentalGroups.fieldTowerTensorComponentAlgEquiv
Documentation

The component selected by the tower action is the original ambient field, compatibly with its K'-algebra structure.

Source context 8 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uB uK uK' uL
variable {K : Type uK} {K' : Type uK'} {L : Type uL}
variable [Field K] [Field K'] [Field L]
variable [Algebra K K'] [Algebra K L]
variable [Algebra K' L] [IsScalarTower K K' L]
Lean source · full declaration
def fieldTowerTensorComponentAlgEquiv :
    let m := fieldTowerTensorComponentIdeal
      (K := K) (K' := K') (L := L)
    letI : m.IsMaximal :=
      fieldTowerTensorComponentIdeal_isMaximal
        (K := K) (K' := K') (L := L)
    GenericTensorFieldComponent m ≃ₐ[K'] L :=
  Ideal.quotientKerAlgEquivOfSurjective
    (f := fieldTowerTensorProductMap
      (K := K) (K' := K') (L := L))
    fieldTowerTensorProductMap_surjective
def

fieldTowerTensorComponentIntegralClosureAlgEquiv

L90 ↗
EtaleFundamentalGroups.fieldTowerTensorComponentIntegralClosureAlgEquiv
Documentation

Integral closures over any base acting through K' are identified on the selected component and on the original ambient field. The base action on the component is the literal left-factor action.

Source context 8 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uB uK uK' uL
variable {K : Type uK} {K' : Type uK'} {L : Type uL}
variable [Field K] [Field K'] [Field L]
variable [Algebra K K'] [Algebra K L]
variable [Algebra K' L] [IsScalarTower K K' L]
Lean source · full declaration
def fieldTowerTensorComponentIntegralClosureAlgEquiv
    {B : Type uB} [CommRing B]
    [Algebra B K'] [Algebra B L] [IsScalarTower B K' L] :
    let m := fieldTowerTensorComponentIdeal
      (K := K) (K' := K') (L := L)
    letI : m.IsMaximal :=
      fieldTowerTensorComponentIdeal_isMaximal
        (K := K) (K' := K') (L := L)
    let M := GenericTensorFieldComponent m
    letI : Algebra B M :=
      genericTensorFieldComponentLeftScalarAlgebra (R := B) m
    integralClosure B M ≃ₐ[B] integralClosure B L := by
  dsimp only
  let m := fieldTowerTensorComponentIdeal
    (K := K) (K' := K') (L := L)
  letI : m.IsMaximal :=
    fieldTowerTensorComponentIdeal_isMaximal
      (K := K) (K' := K') (L := L)
  let M := GenericTensorFieldComponent m
  letI : Algebra B M :=
    genericTensorFieldComponentLeftScalarAlgebra (R := B) m
  let eK' : M ≃ₐ[K'] L :=
    fieldTowerTensorComponentAlgEquiv
      (K := K) (K' := K') (L := L)
  let eB : M ≃ₐ[B] L :=
    { toRingEquiv := eK'.toRingEquiv
      commutes' := by
        intro b
        change eK' (algebraMap K' M (algebraMap B K' b)) =
          algebraMap B L b
        rw [eK'.commutes]
        exact (IsScalarTower.algebraMap_apply B K' L b).symm }
  exact eB.mapIntegralClosure
def

fieldTowerTensorComponentIntegralClosurePrime

L126 ↗
EtaleFundamentalGroups.fieldTowerTensorComponentIntegralClosurePrime
Documentation

Pull a normalization prime on the ambient field back to the literal tensor component selected by the field-tower action.

Source context 8 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uB uK uK' uL
variable {K : Type uK} {K' : Type uK'} {L : Type uL}
variable [Field K] [Field K'] [Field L]
variable [Algebra K K'] [Algebra K L]
variable [Algebra K' L] [IsScalarTower K K' L]
Lean source · full declaration
def fieldTowerTensorComponentIntegralClosurePrime
    {B : Type uB} [CommRing B]
    [Algebra B K'] [Algebra B L] [IsScalarTower B K' L]
    (q : Ideal (integralClosure B L)) :
    let m := fieldTowerTensorComponentIdeal
      (K := K) (K' := K') (L := L)
    letI : m.IsMaximal :=
      fieldTowerTensorComponentIdeal_isMaximal
        (K := K) (K' := K') (L := L)
    let M := GenericTensorFieldComponent m
    letI : Algebra B M :=
      genericTensorFieldComponentLeftScalarAlgebra (R := B) m
    Ideal (integralClosure B M) := by
  dsimp only
  exact q.comap
    (fieldTowerTensorComponentIntegralClosureAlgEquiv
      (B := B) (K := K) (K' := K') (L := L)).toRingHom
theorem

fieldTowerTensorComponentIntegralClosurePrime_isPrime

L146 ↗
EtaleFundamentalGroups.fieldTowerTensorComponentIntegralClosurePrime_isPrime
Documentation

Pullback along the produced normalization equivalence preserves primality.

Source context 8 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uB uK uK' uL
variable {K : Type uK} {K' : Type uK'} {L : Type uL}
variable [Field K] [Field K'] [Field L]
variable [Algebra K K'] [Algebra K L]
variable [Algebra K' L] [IsScalarTower K K' L]
Lean source · full declaration
theorem fieldTowerTensorComponentIntegralClosurePrime_isPrime
    {B : Type uB} [CommRing B]
    [Algebra B K'] [Algebra B L] [IsScalarTower B K' L]
    (q : Ideal (integralClosure B L)) [q.IsPrime] :
    let m := fieldTowerTensorComponentIdeal
      (K := K) (K' := K') (L := L)
    letI : m.IsMaximal :=
      fieldTowerTensorComponentIdeal_isMaximal
        (K := K) (K' := K') (L := L)
    let M := GenericTensorFieldComponent m
    letI : Algebra B M :=
      genericTensorFieldComponentLeftScalarAlgebra (R := B) m
    (fieldTowerTensorComponentIntegralClosurePrime
      (B := B) (K := K) (K' := K') (L := L) q).IsPrime := by
  dsimp only
  exact Ideal.comap_isPrime
    (fieldTowerTensorComponentIntegralClosureAlgEquiv
      (B := B) (K := K) (K' := K') (L := L)).toRingHom q
def

fieldTowerTensorComponentIntegralClosureLocalizationAlgEquiv

L167 ↗
EtaleFundamentalGroups.fieldTowerTensorComponentIntegralClosureLocalizationAlgEquiv
Documentation

The chosen normalization localization on the produced tensor component is the original chosen localization on the ambient field.

Source context 8 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uB uK uK' uL
variable {K : Type uK} {K' : Type uK'} {L : Type uL}
variable [Field K] [Field K'] [Field L]
variable [Algebra K K'] [Algebra K L]
variable [Algebra K' L] [IsScalarTower K K' L]
Lean source · full declaration
def
    fieldTowerTensorComponentIntegralClosureLocalizationAlgEquiv
    {B : Type uB} [CommRing B]
    [Algebra B K'] [Algebra B L] [IsScalarTower B K' L]
    (q : Ideal (integralClosure B L)) [q.IsPrime] :
    let m := fieldTowerTensorComponentIdeal
      (K := K) (K' := K') (L := L)
    letI : m.IsMaximal :=
      fieldTowerTensorComponentIdeal_isMaximal
        (K := K) (K' := K') (L := L)
    let M := GenericTensorFieldComponent m
    letI : Algebra B M :=
      genericTensorFieldComponentLeftScalarAlgebra (R := B) m
    let p := fieldTowerTensorComponentIntegralClosurePrime
      (B := B) (K := K) (K' := K') (L := L) q
    letI : p.IsPrime :=
      fieldTowerTensorComponentIntegralClosurePrime_isPrime
        (B := B) (K := K) (K' := K') (L := L) q
    Localization.AtPrime p ≃ₐ[B] Localization.AtPrime q := by
  dsimp only
  let E := fieldTowerTensorComponentIntegralClosureAlgEquiv
    (B := B) (K := K) (K' := K') (L := L)
  let p := fieldTowerTensorComponentIntegralClosurePrime
    (B := B) (K := K) (K' := K') (L := L) q
  letI : p.IsPrime :=
    fieldTowerTensorComponentIntegralClosurePrime_isPrime
      (B := B) (K := K) (K' := K') (L := L) q
  exact Localization.localAlgEquiv p q E rfl

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