ModuleCoefficientFrobenius.lean
Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.Frobenius.CoefficientFrobenius
5 declarations indexed from sourceView source ↗ Module documentation
The equal-characteristic completed-unramified construction: equal-characteristic Frobenius on
the completed unramified ring
For a finite field k, arithmetic Frobenius acts on AlgebraicClosure k by the #k-power map and hence coefficientwise on (AlgebraicClosure k)[[T]]. These definitions belong to the completed maximal-unramified source used in the equal-characteristic completed-unramified construction; the theta construction of the equal-characteristic theta construction depends on them, not conversely.
This is an equal-characteristic specialization of the general local-field construction, not a claim that Lemma the equal-characteristic completed-unramified construction is complete in general.
Declarations
LubinTate.EqualCharacteristic.equalCharacteristicCoefficientFrobenius
DocumentationArithmetic Frobenius on the algebraic closure of the finite coefficient field.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped PowerSeries
universe u
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
LubinTate.EqualCharacteristic.equalCharacteristicCoefficientFrobenius_apply
DocumentationStates the theorem equalCharacteristicCoefficientFrobenius_apply.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped PowerSeries
universe u
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
LubinTate.EqualCharacteristic.equalCharacteristicPowerSeriesFrobenius
DocumentationArithmetic Frobenius on the completed maximal-unramified coefficient ring, acting coefficientwise and fixing T.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped PowerSeries
universe u
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
LubinTate.EqualCharacteristic.equalCharacteristicPowerSeriesFrobenius_coeff
DocumentationStates the theorem equalCharacteristicPowerSeriesFrobenius_coeff.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped PowerSeries
universe u
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
LubinTate.EqualCharacteristic.equalCharacteristicPowerSeriesFrobenius_X
DocumentationStates the theorem equalCharacteristicPowerSeriesFrobenius_X.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped PowerSeries
universe u
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]