NYLL
Module

Tower.lean

Nyll.EtaleFundamentalGroups.GenericTensor.FieldComponent.Tower
16 declarations indexed from sourceView source ↗

Module documentation

Selected tensor components through an intermediate field

A component of F' ⊗[K] L canonically determines a component after first extending only to an intermediate field F. This file keeps the original maximal ideal and constructs the second-stage quotient map rather than postulating a comparison of abstract fields.

Imports3
Imported by6

Declarations

def

genericTensorTowerMap

L37 ↗
EtaleFundamentalGroups.genericTensorTowerMap
Documentation

The canonical map from the intermediate tensor product to the final tensor product.

Source context 9 commands

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

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

genericTensorTowerAlgebra

L44 ↗
EtaleFundamentalGroups.genericTensorTowerAlgebra
Documentation

The final tensor product as an algebra over the intermediate tensor product.

Source context 9 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uK uF uF' uL
section BaseChange
variable {K : Type uK} {F : Type uF} {F' : Type uF'} {L : Type uL}
variable [Field K] [Field F] [Field F'] [CommRing L]
variable [Algebra K F] [Algebra F F'] [Algebra K F']
variable [IsScalarTower K F F'] [Algebra K L]
Lean source · statement
def genericTensorTowerAlgebra :
    Algebra (F ⊗[K] L) (F' ⊗[K] L)
def

genericTensorTowerBaseChangeAlgEquiv

L50 ↗
EtaleFundamentalGroups.genericTensorTowerBaseChangeAlgEquiv
Documentation

The canonical base-change equivalence, read over the intermediate tensor product.

Source context 9 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uK uF uF' uL
section BaseChange
variable {K : Type uK} {F : Type uF} {F' : Type uF'} {L : Type uL}
variable [Field K] [Field F] [Field F'] [CommRing L]
variable [Algebra K F] [Algebra F F'] [Algebra K F']
variable [IsScalarTower K F F'] [Algebra K L]
Lean source · full declaration
def genericTensorTowerBaseChangeAlgEquiv :
    let A := F ⊗[K] L
    letI : Algebra A (F' ⊗[K] L) := genericTensorTowerAlgebra
    (A ⊗[F] F') ≃ₐ[A] (F' ⊗[K] L) := by
  let A := F ⊗[K] L
  letI : Algebra A (F' ⊗[K] L) := genericTensorTowerAlgebra
  let eRing : (A ⊗[F] F') ≃+* (F' ⊗[K] L) :=
    (Algebra.TensorProduct.comm F A F').toRingEquiv.trans
      (Algebra.TensorProduct.cancelBaseChange K F F' F' L).toRingEquiv
  exact AlgEquiv.ofRingEquiv (R := A) (f := eRing) fun x => by
    induction x using TensorProduct.inductionOn with
    | tmul x y =>
        change
          Algebra.TensorProduct.cancelBaseChange K F F' F' L
              ((1 : F') ⊗ₜ[F] (x ⊗ₜ[K] y)) =
            genericTensorTowerMap (K := K) (F := F) (F' := F') (L := L)
              (x ⊗ₜ[K] y)
        rw [Algebra.TensorProduct.cancelBaseChange_tmul]
        simp only [genericTensorTowerMap, Algebra.TensorProduct.map_tmul,
          IsScalarTower.toAlgHom_apply, AlgHom.id_apply, Algebra.smul_def, mul_one]
    | add x y hx hy => simpa only [map_add] using congrArg₂ (· + ·) hx hy
theorem

genericTensorTower_moduleFinite

L74 ↗
EtaleFundamentalGroups.genericTensorTower_moduleFinite
Documentation

A finite intermediate field extension makes the canonical tensor tower finite.

Source context 9 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uK uF uF' uL
section BaseChange
variable {K : Type uK} {F : Type uF} {F' : Type uF'} {L : Type uL}
variable [Field K] [Field F] [Field F'] [CommRing L]
variable [Algebra K F] [Algebra F F'] [Algebra K F']
variable [IsScalarTower K F F'] [Algebra K L]
Lean source · full declaration
theorem genericTensorTower_moduleFinite [FiniteDimensional F F'] :
    letI : Algebra (F ⊗[K] L) (F' ⊗[K] L) := genericTensorTowerAlgebra
    Module.Finite (F ⊗[K] L) (F' ⊗[K] L) := by
  let A := F ⊗[K] L
  let : Algebra A (F' ⊗[K] L) := genericTensorTowerAlgebra
  let : Module.Finite A (A ⊗[F] F') := Module.Finite.base_change F A F'
  exact Module.Finite.equiv
    (genericTensorTowerBaseChangeAlgEquiv (K := K) (F := F) (F' := F') (L := L)).toLinearEquiv
def

genericTensorTowerIntermediateIdeal

L94 ↗
EtaleFundamentalGroups.genericTensorTowerIntermediateIdeal
Documentation

The contraction of a selected final tensor component to the intermediate tensor product.

Source context 9 commands

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

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

genericTensorTowerIntermediateIdeal_isMaximal

L101 ↗
EtaleFundamentalGroups.genericTensorTowerIntermediateIdeal_isMaximal
Documentation

A maximal final component contracts to a maximal intermediate component when the second field extension is finite.

Source context 9 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uK uF uF' uL
section FieldComponents
variable {K : Type uK} {F : Type uF} {F' : Type uF'} {L : Type uL}
variable [Field K] [Field F] [Field F'] [Field L]
variable [Algebra K F] [Algebra F F'] [Algebra K F']
variable [IsScalarTower K F F'] [Algebra K L]
Lean source · statement
theorem genericTensorTowerIntermediateIdeal_isMaximal
    [FiniteDimensional F F'] (m : Ideal (F' ⊗[K] L)) [m.IsMaximal] :
    (genericTensorTowerIntermediateIdeal
      (K := K) (F := F) (F' := F') (L := L) m).IsMaximal
def

genericTensorTowerIntermediateComponentMap

L116 ↗
EtaleFundamentalGroups.genericTensorTowerIntermediateComponentMap
Documentation

The canonical embedding of the contracted intermediate component into the originally selected final component.

Source context 9 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uK uF uF' uL
section FieldComponents
variable {K : Type uK} {F : Type uF} {F' : Type uF'} {L : Type uL}
variable [Field K] [Field F] [Field F'] [Field L]
variable [Algebra K F] [Algebra F F'] [Algebra K F']
variable [IsScalarTower K F F'] [Algebra K L]
Lean source · full declaration
def genericTensorTowerIntermediateComponentMap
    [FiniteDimensional F F'] (m : Ideal (F' ⊗[K] L)) [m.IsMaximal] :
    let n := genericTensorTowerIntermediateIdeal
      (K := K) (F := F) (F' := F') (L := L) m
    letI : n.IsMaximal :=
      genericTensorTowerIntermediateIdeal_isMaximal
        (K := K) (F := F) (F' := F') (L := L) m
    GenericTensorFieldComponent n →ₐ[K] GenericTensorFieldComponent m := by
  let n := genericTensorTowerIntermediateIdeal
    (K := K) (F := F) (F' := F') (L := L) m
  letI : n.IsMaximal :=
    genericTensorTowerIntermediateIdeal_isMaximal
      (K := K) (F := F) (F' := F') (L := L) m
  let g : (F ⊗[K] L) →ₐ[K] GenericTensorFieldComponent m :=
    (Ideal.Quotient.mkₐ K m).comp
      (genericTensorTowerMap (K := K) (F := F) (F' := F') (L := L))
  exact Ideal.Quotient.liftₐ n g fun x hx ↦ by
    exact Ideal.Quotient.eq_zero_iff_mem.mpr hx
theorem

genericTensorTowerIntermediateComponentMap_mk

L136 ↗
EtaleFundamentalGroups.genericTensorTowerIntermediateComponentMap_mk
Source context 9 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uK uF uF' uL
section FieldComponents
variable {K : Type uK} {F : Type uF} {F' : Type uF'} {L : Type uL}
variable [Field K] [Field F] [Field F'] [Field L]
variable [Algebra K F] [Algebra F F'] [Algebra K F']
variable [IsScalarTower K F F'] [Algebra K L]
Lean source · statement
theorem genericTensorTowerIntermediateComponentMap_mk
    [FiniteDimensional F F'] (m : Ideal (F' ⊗[K] L)) [m.IsMaximal]
    (x : F ⊗[K] L) :
    genericTensorTowerIntermediateComponentMap
        (K := K) (F := F) (F' := F') (L := L) m
        (Ideal.Quotient.mk
          (genericTensorTowerIntermediateIdeal
            (K := K) (F := F) (F' := F') (L := L) m) x) =
      Ideal.Quotient.mk m
        (genericTensorTowerMap (K := K) (F := F) (F' := F') (L := L) x)
def

genericTensorTowerFinalComponentAlgebra

L151 ↗
EtaleFundamentalGroups.genericTensorTowerFinalComponentAlgebra
Documentation

The intermediate-field algebra structure on the final selected component, induced through the canonical copy of F'.

Source context 9 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uK uF uF' uL
section FieldComponents
variable {K : Type uK} {F : Type uF} {F' : Type uF'} {L : Type uL}
variable [Field K] [Field F] [Field F'] [Field L]
variable [Algebra K F] [Algebra F F'] [Algebra K F']
variable [IsScalarTower K F F'] [Algebra K L]
Lean source · statement
def genericTensorTowerFinalComponentAlgebra
    (m : Ideal (F' ⊗[K] L)) [m.IsMaximal] :
    Algebra F (GenericTensorFieldComponent m)
def

genericTensorTowerFinalLeftAlgHom

L159 ↗
EtaleFundamentalGroups.genericTensorTowerFinalLeftAlgHom
Documentation

The canonical copy of F' in the final component, read as an F-algebra map.

Source context 9 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uK uF uF' uL
section FieldComponents
variable {K : Type uK} {F : Type uF} {F' : Type uF'} {L : Type uL}
variable [Field K] [Field F] [Field F'] [Field L]
variable [Algebra K F] [Algebra F F'] [Algebra K F']
variable [IsScalarTower K F F'] [Algebra K L]
Lean source · full declaration
def genericTensorTowerFinalLeftAlgHom
    (m : Ideal (F' ⊗[K] L)) [m.IsMaximal] :
    letI : Algebra F (GenericTensorFieldComponent m) :=
      genericTensorTowerFinalComponentAlgebra
        (K := K) (F := F) (F' := F') (L := L) m
    F' →ₐ[F] GenericTensorFieldComponent m := by
  letI : Algebra F (GenericTensorFieldComponent m) :=
    genericTensorTowerFinalComponentAlgebra
      (K := K) (F := F) (F' := F') (L := L) m
  exact
    { (genericTensorFieldComponentLeft m).toRingHom with
      commutes' := fun _ ↦ rfl }
def

genericTensorTowerIntermediateComponentAlgHom

L174 ↗
EtaleFundamentalGroups.genericTensorTowerIntermediateComponentAlgHom
Documentation

The contracted component embeds into the final component over the intermediate field.

Source context 9 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uK uF uF' uL
section FieldComponents
variable {K : Type uK} {F : Type uF} {F' : Type uF'} {L : Type uL}
variable [Field K] [Field F] [Field F'] [Field L]
variable [Algebra K F] [Algebra F F'] [Algebra K F']
variable [IsScalarTower K F F'] [Algebra K L]
Lean source · full declaration
def genericTensorTowerIntermediateComponentAlgHom
    [FiniteDimensional F F'] (m : Ideal (F' ⊗[K] L)) [m.IsMaximal] :
    let n := genericTensorTowerIntermediateIdeal
      (K := K) (F := F) (F' := F') (L := L) m
    letI : n.IsMaximal :=
      genericTensorTowerIntermediateIdeal_isMaximal
        (K := K) (F := F) (F' := F') (L := L) m
    letI : Algebra F (GenericTensorFieldComponent m) :=
      genericTensorTowerFinalComponentAlgebra
        (K := K) (F := F) (F' := F') (L := L) m
    GenericTensorFieldComponent n →ₐ[F] GenericTensorFieldComponent m := by
  let n := genericTensorTowerIntermediateIdeal
    (K := K) (F := F) (F' := F') (L := L) m
  letI : n.IsMaximal :=
    genericTensorTowerIntermediateIdeal_isMaximal
      (K := K) (F := F) (F' := F') (L := L) m
  letI : Algebra F (GenericTensorFieldComponent m) :=
    genericTensorTowerFinalComponentAlgebra
      (K := K) (F := F) (F' := F') (L := L) m
  exact
    { (genericTensorTowerIntermediateComponentMap
        (K := K) (F := F) (F' := F') (L := L) m).toRingHom with
      commutes' := by
        intro x
        change
          Ideal.Quotient.mk m
              (genericTensorTowerMap
                (K := K) (F := F) (F' := F') (L := L)
                ((Algebra.TensorProduct.includeLeft :
                  F →ₐ[K] F ⊗[K] L) x)) =
            genericTensorFieldComponentLeft m (algebraMap F F' x)
        simp [genericTensorTowerMap] }
def

genericTensorTowerSecondComponentMap

L209 ↗
EtaleFundamentalGroups.genericTensorTowerSecondComponentMap
Documentation

The second-stage tensor product maps canonically onto the originally selected final component.

Source context 9 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uK uF uF' uL
section FieldComponents
variable {K : Type uK} {F : Type uF} {F' : Type uF'} {L : Type uL}
variable [Field K] [Field F] [Field F'] [Field L]
variable [Algebra K F] [Algebra F F'] [Algebra K F']
variable [IsScalarTower K F F'] [Algebra K L]
Lean source · full declaration
def genericTensorTowerSecondComponentMap
    [FiniteDimensional F F'] (m : Ideal (F' ⊗[K] L)) [m.IsMaximal] :
    let n := genericTensorTowerIntermediateIdeal
      (K := K) (F := F) (F' := F') (L := L) m
    letI : n.IsMaximal :=
      genericTensorTowerIntermediateIdeal_isMaximal
        (K := K) (F := F) (F' := F') (L := L) m
    (F' ⊗[F] GenericTensorFieldComponent n) →ₐ[F']
      GenericTensorFieldComponent m := by
  let n := genericTensorTowerIntermediateIdeal
    (K := K) (F := F) (F' := F') (L := L) m
  letI : n.IsMaximal :=
    genericTensorTowerIntermediateIdeal_isMaximal
      (K := K) (F := F) (F' := F') (L := L) m
  letI : Algebra F (GenericTensorFieldComponent m) :=
    genericTensorTowerFinalComponentAlgebra
      (K := K) (F := F) (F' := F') (L := L) m
  let gF : (F' ⊗[F] GenericTensorFieldComponent n) →ₐ[F]
      GenericTensorFieldComponent m :=
    Algebra.TensorProduct.productMap
      (genericTensorTowerFinalLeftAlgHom
        (K := K) (F := F) (F' := F') (L := L) m)
      (genericTensorTowerIntermediateComponentAlgHom
        (K := K) (F := F) (F' := F') (L := L) m)
  exact
    { gF.toRingHom with
      commutes' := by
        intro x
        simp only [AlgHom.toRingHom_eq_coe, RingHom.toMonoidHom_eq_coe,
          AlgHom.toRingHom_toMonoidHom, Algebra.TensorProduct.algebraMap_apply,
          Algebra.algebraMap_self, RingHom.id_apply, OneHom.toFun_eq_coe,
          MonoidHom.toOneHom_coe, MonoidHom.coe_ofClass]
        change genericTensorFieldComponentLeft m x *
            genericTensorTowerIntermediateComponentAlgHom
              (K := K) (F := F) (F' := F') (L := L) m
              (1 : GenericTensorFieldComponent n) =
          algebraMap F' (GenericTensorFieldComponent m) x
        rw [map_one, mul_one]
        exact genericTensorFieldComponentLeft_eq_algebraMap m x }
theorem

genericTensorTowerSecondComponentMap_surjective

L251 ↗
EtaleFundamentalGroups.genericTensorTowerSecondComponentMap_surjective
Documentation

The canonical second-stage map is onto the originally selected component.

Source context 9 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uK uF uF' uL
section FieldComponents
variable {K : Type uK} {F : Type uF} {F' : Type uF'} {L : Type uL}
variable [Field K] [Field F] [Field F'] [Field L]
variable [Algebra K F] [Algebra F F'] [Algebra K F']
variable [IsScalarTower K F F'] [Algebra K L]
Lean source · statement
theorem genericTensorTowerSecondComponentMap_surjective
    [FiniteDimensional F F'] (m : Ideal (F' ⊗[K] L)) [m.IsMaximal] :
    Function.Surjective
      (genericTensorTowerSecondComponentMap
        (K := K) (F := F) (F' := F') (L := L) m)
abbrev

genericTensorTowerSecondIdeal

L286 ↗
EtaleFundamentalGroups.genericTensorTowerSecondIdeal
Documentation

The maximal ideal selecting the second-stage component corresponding to the original final component.

Source context 9 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uK uF uF' uL
section FieldComponents
variable {K : Type uK} {F : Type uF} {F' : Type uF'} {L : Type uL}
variable [Field K] [Field F] [Field F'] [Field L]
variable [Algebra K F] [Algebra F F'] [Algebra K F']
variable [IsScalarTower K F F'] [Algebra K L]
Lean source · full declaration
abbrev genericTensorTowerSecondIdeal
    [FiniteDimensional F F'] (m : Ideal (F' ⊗[K] L)) [m.IsMaximal] :
    let n := genericTensorTowerIntermediateIdeal
      (K := K) (F := F) (F' := F') (L := L) m
    letI : n.IsMaximal :=
      genericTensorTowerIntermediateIdeal_isMaximal
        (K := K) (F := F) (F' := F') (L := L) m
    Ideal (F' ⊗[F] GenericTensorFieldComponent n) :=
  RingHom.ker
    (genericTensorTowerSecondComponentMap
      (K := K) (F := F) (F' := F') (L := L) m).toRingHom
theorem

genericTensorTowerSecondIdeal_isMaximal

L300 ↗
EtaleFundamentalGroups.genericTensorTowerSecondIdeal_isMaximal
Documentation

The second-stage ideal is maximal because its canonical quotient map is surjective onto the selected field component.

Source context 9 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uK uF uF' uL
section FieldComponents
variable {K : Type uK} {F : Type uF} {F' : Type uF'} {L : Type uL}
variable [Field K] [Field F] [Field F'] [Field L]
variable [Algebra K F] [Algebra F F'] [Algebra K F']
variable [IsScalarTower K F F'] [Algebra K L]
Lean source · statement
theorem genericTensorTowerSecondIdeal_isMaximal
    [FiniteDimensional F F'] (m : Ideal (F' ⊗[K] L)) [m.IsMaximal] :
    (genericTensorTowerSecondIdeal
      (K := K) (F := F) (F' := F') (L := L) m).IsMaximal
def

genericTensorTowerSecondComponentAlgEquiv

L312 ↗
EtaleFundamentalGroups.genericTensorTowerSecondComponentAlgEquiv
Documentation

Factoring a selected tensor component through the intermediate field does not change the final field component.

Source context 9 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uK uF uF' uL
section FieldComponents
variable {K : Type uK} {F : Type uF} {F' : Type uF'} {L : Type uL}
variable [Field K] [Field F] [Field F'] [Field L]
variable [Algebra K F] [Algebra F F'] [Algebra K F']
variable [IsScalarTower K F F'] [Algebra K L]
Lean source · full declaration
def genericTensorTowerSecondComponentAlgEquiv
    [FiniteDimensional F F'] (m : Ideal (F' ⊗[K] L)) [m.IsMaximal] :
    let n := genericTensorTowerIntermediateIdeal
      (K := K) (F := F) (F' := F') (L := L) m
    letI : n.IsMaximal :=
      genericTensorTowerIntermediateIdeal_isMaximal
        (K := K) (F := F) (F' := F') (L := L) m
    let m₂ := genericTensorTowerSecondIdeal
      (K := K) (F := F) (F' := F') (L := L) m
    letI : m₂.IsMaximal :=
      genericTensorTowerSecondIdeal_isMaximal
        (K := K) (F := F) (F' := F') (L := L) m
    GenericTensorFieldComponent m₂ ≃ₐ[F'] GenericTensorFieldComponent m := by
  let n := genericTensorTowerIntermediateIdeal
    (K := K) (F := F) (F' := F') (L := L) m
  letI : n.IsMaximal :=
    genericTensorTowerIntermediateIdeal_isMaximal
      (K := K) (F := F) (F' := F') (L := L) m
  let m₂ := genericTensorTowerSecondIdeal
    (K := K) (F := F) (F' := F') (L := L) m
  letI : m₂.IsMaximal :=
    genericTensorTowerSecondIdeal_isMaximal
      (K := K) (F := F) (F' := F') (L := L) m
  exact Ideal.quotientKerAlgEquivOfSurjective
    (genericTensorTowerSecondComponentMap_surjective
      (K := K) (F := F) (F' := F') (L := L) m)

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