ModuleEquivariantMap.lean
Nyll.ValuedFieldTheory.Valuation.Completion.EquivariantMap
2 declarations indexed from sourceView source ↗ Module documentation
Equivariance of maps between discrete valued completions
A relative field automorphism carrying one prolongation to another induces a completion isomorphism commuting with the map from the completed base field.
Declarations
ValuationTheory.DiscreteValuationField.DVF.completionMap_continuous
DocumentationThe map induced by an extension of discrete valuations is continuous.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ValuationTheory.DiscreteValuationField.DVF
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
(base : DVF K) (source target : DVF L)
[base.valuation.HasExtension source.valuation]
[base.valuation.HasExtension target.valuation]
ValuationTheory.DiscreteValuationField.DVF.completionRingEquiv_comp_completionMap
DocumentationCompletion isomorphisms induced by relative field automorphisms commute with the embedding of the completed base field.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ValuationTheory.DiscreteValuationField.DVF
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
(base : DVF K) (source target : DVF L)
[base.valuation.HasExtension source.valuation]
[base.valuation.HasExtension target.valuation]