NYLL
Module

TowerIdealOver.lean

Nyll.EtaleFundamentalGroups.GenericTensor.FieldComponent.TowerIdealOver
4 declarations indexed from sourceView source ↗

Module documentation

A final tensor component above a fixed intermediate component

For a finite field extension F'/F, scalar extension makes F' ⊗[K] L a finite faithfully-flat algebra over F ⊗[K] L. Consequently every fixed maximal intermediate component has a maximal final component above it. This file packages one canonical choice and records that the contraction used by GenericTensorFieldComponentTower is exactly the original component.

Imports2
Imported by2

Declarations

theorem

exists_genericTensorTowerIdeal_over

L39 ↗
EtaleFundamentalGroups.exists_genericTensorTowerIdeal_over
Documentation

A maximal final tensor component exists above every maximal intermediate component.

Source context 10 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uK uF uF' uL
section
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]
variable [FiniteDimensional F F']
Lean source · statement
theorem exists_genericTensorTowerIdeal_over
    (n : Ideal (F ⊗[K] L)) [n.IsMaximal] :
    ∃ m : Ideal (F' ⊗[K] L),
      m.IsMaximal ∧
        genericTensorTowerIntermediateIdeal
          (K := K) (F := F) (F' := F') (L := L) m = n
def

genericTensorTowerIdealOver

L68 ↗
EtaleFundamentalGroups.genericTensorTowerIdealOver
Documentation

A canonical maximal final tensor ideal above n.

Source context 10 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uK uF uF' uL
section
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]
variable [FiniteDimensional F F']
Lean source · statement
def genericTensorTowerIdealOver
    (n : Ideal (F ⊗[K] L)) [n.IsMaximal] :
    Ideal (F' ⊗[K] L)
theorem

genericTensorTowerIdealOver_isMaximal

L76 ↗
EtaleFundamentalGroups.genericTensorTowerIdealOver_isMaximal
Documentation

The chosen final tensor ideal is maximal.

Source context 10 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uK uF uF' uL
section
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]
variable [FiniteDimensional F F']
Lean source · statement
theorem genericTensorTowerIdealOver_isMaximal
    (n : Ideal (F ⊗[K] L)) [n.IsMaximal] :
    (genericTensorTowerIdealOver
      (K := K) (F := F) (F' := F') (L := L) n).IsMaximal
theorem

genericTensorTowerIntermediateIdeal_idealOver

L85 ↗
EtaleFundamentalGroups.genericTensorTowerIntermediateIdeal_idealOver
Documentation

Contracting the chosen final ideal recovers n exactly.

Source context 10 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uK uF uF' uL
section
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]
variable [FiniteDimensional F F']
Lean source · statement
theorem genericTensorTowerIntermediateIdeal_idealOver
    (n : Ideal (F ⊗[K] L)) [n.IsMaximal] :
    genericTensorTowerIntermediateIdeal
        (K := K) (F := F) (F' := F') (L := L)
        (genericTensorTowerIdealOver
          (K := K) (F := F) (F' := F') (L := L) n) = n

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