NYLL
Module

ActualCompositumComponent.lean

Nyll.EtaleFundamentalGroups.GenericTensor.ActualCompositumComponent
7 declarations indexed from sourceView source ↗

Module documentation

The literal generic component of an actual compositum

The finite-etale base-change theorem constructs a normalization in an actual compositum, but its proof previously hid the maximal generic-fibre component used to select that compositum. This file exposes the canonical map, its kernel, and the resulting quotient-field equivalence. A completed lower Kummer factor can therefore be followed into a later fixed tensor component without reselecting an abstract field.

Imports1
Imported by3

Declarations

def

actualCompositumGenericComponentMap

L32 ↗
EtaleFundamentalGroups.actualCompositumGenericComponentMap
Documentation

The canonical generic-fibre map from a finite algebra with generic field E to its actual compositum with K'.

Source context 5 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
open DiscreteValuationField.FieldCompositum
universe uA uT uF uOmega
Lean source · statement
def actualCompositumGenericComponentMap
    {A : Type uA} {T : Type uT} {F : Type uF} {Omega : Type uOmega}
    [CommRing A] [CommRing T] [Algebra A T]
    [Field F] [Algebra A F]
    [Field Omega] [Algebra F Omega]
    (E K' : IntermediateField F Omega)
    [Algebra A K'] [IsScalarTower A F K']
    (eGeneric : (F ⊗[A] T) ≃ₐ[F] E) :
    (K' ⊗[A] T) →ₐ[K']
      (E ⊔ K' : IntermediateField F Omega)
theorem

actualCompositumGenericComponentMap_tmul_right_coe

L48 ↗
EtaleFundamentalGroups.actualCompositumGenericComponentMap_tmul_right_coe
Documentation

On the right integral factor, the actual-compositum map is the original generic-fibre coordinate followed by the literal ambient inclusion.

Source context 5 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
open DiscreteValuationField.FieldCompositum
universe uA uT uF uOmega
Lean source · statement
theorem actualCompositumGenericComponentMap_tmul_right_coe
    {A : Type uA} {T : Type uT} {F : Type uF} {Omega : Type uOmega}
    [CommRing A] [CommRing T] [Algebra A T]
    [Field F] [Algebra A F]
    [Field Omega] [Algebra F Omega]
    (E K' : IntermediateField F Omega)
    [Algebra A K'] [IsScalarTower A F K']
    (eGeneric : (F ⊗[A] T) ≃ₐ[F] E) (c : T) :
    (((actualCompositumGenericComponentMap E K' eGeneric)
        (1 ⊗ₜ[A] c) :
          (E ⊔ K' : IntermediateField F Omega)) : Omega) =
      ((eGeneric (1 ⊗ₜ[A] c) : E) : Omega)
theorem

actualCompositumGenericComponentMap_surjective

L64 ↗
EtaleFundamentalGroups.actualCompositumGenericComponentMap_surjective
Documentation

The actual-compositum generic map is onto.

Source context 5 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
open DiscreteValuationField.FieldCompositum
universe uA uT uF uOmega
Lean source · statement
theorem actualCompositumGenericComponentMap_surjective
    {A : Type uA} {T : Type uT} {F : Type uF} {Omega : Type uOmega}
    [CommRing A] [CommRing T] [Algebra A T]
    [Field F] [Algebra A F]
    [Field Omega] [Algebra F Omega]
    (E K' : IntermediateField F Omega)
    [Algebra A K'] [IsScalarTower A F K']
    [FiniteDimensional F E]
    (eGeneric : (F ⊗[A] T) ≃ₐ[F] E) :
    Function.Surjective
      (actualCompositumGenericComponentMap E K' eGeneric)
def

actualCompositumGenericComponentIdeal

L80 ↗
EtaleFundamentalGroups.actualCompositumGenericComponentIdeal
Documentation

The literal maximal ideal selecting the actual compositum in the higher generic fibre.

Source context 5 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
open DiscreteValuationField.FieldCompositum
universe uA uT uF uOmega
Lean source · statement
def actualCompositumGenericComponentIdeal
    {A : Type uA} {T : Type uT} {F : Type uF} {Omega : Type uOmega}
    [CommRing A] [CommRing T] [Algebra A T]
    [Field F] [Algebra A F]
    [Field Omega] [Algebra F Omega]
    (E K' : IntermediateField F Omega)
    [Algebra A K'] [IsScalarTower A F K']
    (eGeneric : (F ⊗[A] T) ≃ₐ[F] E) :
    Ideal (K' ⊗[A] T)
theorem

actualCompositumGenericComponentIdeal_isMaximal

L94 ↗
EtaleFundamentalGroups.actualCompositumGenericComponentIdeal_isMaximal
Documentation

The kernel selecting the actual compositum is maximal, since the canonical product map is onto that field.

Source context 5 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
open DiscreteValuationField.FieldCompositum
universe uA uT uF uOmega
Lean source · statement
theorem actualCompositumGenericComponentIdeal_isMaximal
    {A : Type uA} {T : Type uT} {F : Type uF} {Omega : Type uOmega}
    [CommRing A] [CommRing T] [Algebra A T]
    [Field F] [Algebra A F]
    [Field Omega] [Algebra F Omega]
    (E K' : IntermediateField F Omega)
    [Algebra A K'] [IsScalarTower A F K']
    [FiniteDimensional F E]
    (eGeneric : (F ⊗[A] T) ≃ₐ[F] E) :
    (actualCompositumGenericComponentIdeal E K' eGeneric).IsMaximal
def

actualCompositumGenericComponentAlgEquiv

L110 ↗
EtaleFundamentalGroups.actualCompositumGenericComponentAlgEquiv
Documentation

The selected quotient field is canonically the actual compositum; the equivalence is induced by the same product map, not by field choice.

Source context 5 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
open DiscreteValuationField.FieldCompositum
universe uA uT uF uOmega
Lean source · statement
def actualCompositumGenericComponentAlgEquiv
    {A : Type uA} {T : Type uT} {F : Type uF} {Omega : Type uOmega}
    [CommRing A] [CommRing T] [Algebra A T]
    [Field F] [Algebra A F]
    [Field Omega] [Algebra F Omega]
    (E K' : IntermediateField F Omega)
    [Algebra A K'] [IsScalarTower A F K']
    [FiniteDimensional F E]
    (eGeneric : (F ⊗[A] T) ≃ₐ[F] E) :
    ((K' ⊗[A] T) ⧸
        actualCompositumGenericComponentIdeal E K' eGeneric) ≃ₐ[K']
      (E ⊔ K' : IntermediateField F Omega)
theorem

actualCompositumGenericComponentAlgEquiv_mk

L127 ↗
EtaleFundamentalGroups.actualCompositumGenericComponentAlgEquiv_mk
Documentation

The quotient comparison is induced by the literal compositum map.

Source context 5 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
open DiscreteValuationField.FieldCompositum
universe uA uT uF uOmega
Lean source · statement
theorem actualCompositumGenericComponentAlgEquiv_mk
    {A : Type uA} {T : Type uT} {F : Type uF} {Omega : Type uOmega}
    [CommRing A] [CommRing T] [Algebra A T]
    [Field F] [Algebra A F]
    [Field Omega] [Algebra F Omega]
    (E K' : IntermediateField F Omega)
    [Algebra A K'] [IsScalarTower A F K']
    [FiniteDimensional F E]
    (eGeneric : (F ⊗[A] T) ≃ₐ[F] E) (z : K' ⊗[A] T) :
    actualCompositumGenericComponentAlgEquiv E K' eGeneric
        (Ideal.Quotient.mk
          (actualCompositumGenericComponentIdeal E K' eGeneric) z) =
      actualCompositumGenericComponentMap E K' eGeneric z

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