ModuleHenselianHomDescent.lean
Nyll.ValuedFieldTheory.Valuation.Completion.HenselianHomDescent
2 declarations indexed from sourceView source ↗ Module documentation
Descending homomorphisms between valuation completions
The image of a separable element under a homomorphism of completions is separable over the target field. Henselianity places that image in the original target field, producing a unique homomorphism before completion.
Declarations
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ValuationTheory.DiscreteValuationField.HenselianDVF
variable {K L M : Type*} [Field K] [Field L] [Field M]
[Algebra K L] [Algebra K M]
(base : HenselianDVF K) (targetL : DVF L) (targetM : DVF M)
[hM : base.toDVF.valuation.HasExtension targetM.valuation]
ValuationTheory.DiscreteValuationField.HenselianDVF.existsUnique_algHom_of_completionAlgHom
DocumentationA homomorphism between the actual valuation completions over the original ground field restricts uniquely to the original fields. Separability of the source and algebraicity of the target suffice; neither extension is required to be finite, and only the target valuation must extend the base valuation.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ValuationTheory.DiscreteValuationField.HenselianDVF
variable {K L M : Type*} [Field K] [Field L] [Field M]
[Algebra K L] [Algebra K M]
(base : HenselianDVF K) (targetL : DVF L) (targetM : DVF M)
[hM : base.toDVF.valuation.HasExtension targetM.valuation]
local instance : UniformContinuousConstSMul K (WithVal targetL.valuation) :=
WithVal.uniformContinuousConstSMul_algebra targetL.valuation
include hM