NYLL
Module

HenselianSeparableAutExtension.lean

Nyll.ValuedFieldTheory.Valuation.Completion.HenselianSeparableAutExtension
3 declarations indexed from sourceView source ↗

Module documentation

Extending automorphisms through the separable tensor comparison

The automorphism is transported from id ⊗ σ through the actual tensor comparison. Its values on the chosen separable closure determine it, so the resulting extension preserves composition.

Imports4
Imported by2

Declarations

def

extendSeparableClosedAut

L34 ↗
ValuationTheory.DiscreteValuationField.HenselianDVF.extendSeparableClosedAut
Documentation

Extend an automorphism of the embedded separable closure by tensoring with the identity of the actual completion and transporting back to E.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace ValuationTheory.DiscreteValuationField.HenselianDVF
open scoped TensorProduct
variable {K : Type*} [Field K] (base : HenselianDVF K)
  {S E : Type*} [Field S] [Field E] [Algebra K S]
  [Algebra base.valuation.Completion E] [Algebra K E]
  [IsScalarTower K base.valuation.Completion E] [Algebra.IsSeparable K S]
  [IsSepClosed S] [Algebra.IsSeparable base.valuation.Completion E]
Lean source · statement
def extendSeparableClosedAut (i : S →ₐ[K] E) (σ : S ≃ₐ[K] S) :
    E ≃ₐ[base.valuation.Completion] E
theorem

extendSeparableClosedAut_apply

L42 ↗
ValuationTheory.DiscreteValuationField.HenselianDVF.extendSeparableClosedAut_apply
Documentation

Extension agrees with the original action through the chosen embedding.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace ValuationTheory.DiscreteValuationField.HenselianDVF
open scoped TensorProduct
variable {K : Type*} [Field K] (base : HenselianDVF K)
  {S E : Type*} [Field S] [Field E] [Algebra K S]
  [Algebra base.valuation.Completion E] [Algebra K E]
  [IsScalarTower K base.valuation.Completion E] [Algebra.IsSeparable K S]
  [IsSepClosed S] [Algebra.IsSeparable base.valuation.Completion E]
Lean source · statement
theorem extendSeparableClosedAut_apply (i : S →ₐ[K] E)
    (σ : S ≃ₐ[K] S) (s : S) :
    base.extendSeparableClosedAut i σ (i s) = i (σ s)
theorem

extendSeparableClosedAut_mul

L58 ↗
ValuationTheory.DiscreteValuationField.HenselianDVF.extendSeparableClosedAut_mul
Documentation

The extension preserves composition of the original automorphisms.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace ValuationTheory.DiscreteValuationField.HenselianDVF
open scoped TensorProduct
variable {K : Type*} [Field K] (base : HenselianDVF K)
  {S E : Type*} [Field S] [Field E] [Algebra K S]
  [Algebra base.valuation.Completion E] [Algebra K E]
  [IsScalarTower K base.valuation.Completion E] [Algebra.IsSeparable K S]
  [IsSepClosed S] [Algebra.IsSeparable base.valuation.Completion E]
Lean source · statement
theorem extendSeparableClosedAut_mul (i : S →ₐ[K] E) (σ τ : S ≃ₐ[K] S) :
    base.extendSeparableClosedAut i (σ * τ) =
      base.extendSeparableClosedAut i σ * base.extendSeparableClosedAut i τ

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.