Module

Degree.lean

Nyll.EtaleFundamentalGroups.GenericTensor.FieldComponent.Degree

1 declaration indexed from sourceView source ↗

Module documentation

Degree bounds for selected generic tensor components

A field component selected from K' tensor[K] L is a quotient of that base-changed finite-dimensional algebra. Its degree over K' is therefore bounded by the original degree of L / K. This supplies one common factorial exponent for all completed local components.

Imports1

Nyll.EtaleFundamentalGroups.GenericTensor.FieldComponent.Basic

Imported by2

theorem

genericTensorFieldComponent_finrank_le

L28 ↗

EtaleFundamentalGroups.genericTensorFieldComponent_finrank_le

Documentation

Every selected field component of a finite field extension after base change has degree at most the original field degree.

Source context 4 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uK uK' uL

Lean source · statement

theorem genericTensorFieldComponent_finrank_le
    {K : Type uK} {K' : Type uK'} {L : Type uL}
    [Field K] [Field K'] [Field L]
    [Algebra K K'] [Algebra K L] [FiniteDimensional K L]
    (m : Ideal (K' ⊗[K] L)) [m.IsMaximal] :
    Module.finrank K' (GenericTensorFieldComponent m) ≤
      Module.finrank K L

Module documentation

Degree bounds for selected generic tensor components

Declarations

genericTensorFieldComponent_finrank_le