theorem
L26 ↗completionAlgHom_ext
ValuationTheory.DiscreteValuationField.DVF.completionAlgHom_ext
Homomorphisms from a finite extension completion over the base completion are equal if they agree on the original extension 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) (target : DVF L)
[hExtension : base.valuation.HasExtension target.valuation]Lean source · statement
theorem completionAlgHom_ext [FiniteDimensional K L]
{B : Type*} [CommRing B] [Algebra base.valuation.Completion B]
(f g : @AlgHom base.valuation.Completion target.valuation.Completion B _ _ _
(completionAlgebra base target) _)
(h : ∀ l : L, f (l : target.valuation.Completion) = g (l : target.valuation.Completion)) :
f = g