ModuleIntertwiner.lean
Nyll.ClassFieldTheory.LubinTate.FormalModule.Intertwiner
7 declarations indexed from sourceView source ↗ Module documentation
Intertwining equations for Lubin--Tate series
For two Lubin--Tate series with the same prescribed linear coefficient, this module defines the multivariable intertwining equation and its additive defect.
Declarations
LubinTate.SameUniformizer.inVariable
DocumentationInsert a one-variable Lubin--Tate series into the variable X_i.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace LubinTate
namespace SameUniformizer
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
variable {σ : Type*}
LubinTate.SameUniformizer.constantCoeff_inVariable
DocumentationStates the theorem constantCoeff_inVariable.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace LubinTate
namespace SameUniformizer
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
variable {σ : Type*}
LubinTate.SameUniformizer.inVariable_hasSubst
DocumentationThe family i |-> e(X_i) admits genuine multivariable substitution.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace LubinTate
namespace SameUniformizer
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
variable {σ : Type*}
LubinTate.SameUniformizer.Intertwines
DocumentationThe literal same-uniformizer equation e(H(X_i)) = H(ebar(X_i)).
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace LubinTate
namespace SameUniformizer
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
variable {σ : Type*}
LubinTate.SameUniformizer.defect
DocumentationThe coefficientwise defect whose vanishing is the intertwining equation.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace LubinTate
namespace SameUniformizer
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
variable {σ : Type*}
LubinTate.SameUniformizer.intertwines_iff_defect_eq_zero
DocumentationStates the theorem intertwines_iff_defect_eq_zero.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace LubinTate
namespace SameUniformizer
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
variable {σ : Type*}
LubinTate.SameUniformizer.intertwines_X
DocumentationEach variable itself intertwines a Lubin--Tate series with itself.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace LubinTate
namespace SameUniformizer
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
variable {σ : Type*}