Module

ValuationInertiaAlgEquiv.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.ValuationInertiaAlgEquiv

3 declarations indexed from sourceView source ↗

Module documentation

Valuation inertia under algebra equivalences

An algebra equivalence transports the ambient copy of valuation-subring inertia to the corresponding ambient inertia subgroup for the pulled-back valuation subring.

Imports1

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.BaseChange

Imported by2

theorem

autCongr_mem_valuationInertiaGroupInAut

L26 ↗

ClassFieldTower.Martinet.Shafarevich.autCongr_mem_valuationInertiaGroupInAut

Documentation

Conjugation by an algebra equivalence sends ambient valuation inertia to ambient valuation inertia for the transported valuation subring.

Source context 4 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open HilbertRamification
universe u v w

Lean source · statement

theorem autCongr_mem_valuationInertiaGroupInAut
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [Field L] [Field M]
    [Algebra K L] [Algebra K M]
    [Normal K M]
    (e : L ≃ₐ[K] M) (B : ValuationSubring M)
    (sigma : L ≃ₐ[K] L)
    (hsigma : sigma ∈
      RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroupInAut K
        (B.comap e.toRingHom)) :
    AlgEquiv.autCongr e sigma ∈
      RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroupInAut K B

theorem

autCongr_mem_valuationInertiaGroupInAut_iff

L87 ↗

ClassFieldTower.Martinet.Shafarevich.autCongr_mem_valuationInertiaGroupInAut_iff

Documentation

Membership in ambient valuation inertia is invariant under conjugation by an algebra equivalence.

Source context 4 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open HilbertRamification
universe u v w

Lean source · statement

theorem autCongr_mem_valuationInertiaGroupInAut_iff
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [Field L] [Field M]
    [Algebra K L] [Algebra K M]
    [Normal K L] [Normal K M]
    (e : L ≃ₐ[K] M) (B : ValuationSubring M)
    (sigma : L ≃ₐ[K] L) :
    AlgEquiv.autCongr e sigma ∈
        RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroupInAut K B ↔
      sigma ∈
        RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroupInAut K
          (B.comap e.toRingHom)

theorem

valuationInertiaGroupInAut_map_autCongr

L122 ↗

ClassFieldTower.Martinet.Shafarevich.valuationInertiaGroupInAut_map_autCongr

Documentation

Conjugation by an algebra equivalence maps the whole ambient valuation-inertia subgroup onto the target ambient inertia subgroup.

Source context 4 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open HilbertRamification
universe u v w

Lean source · statement

theorem valuationInertiaGroupInAut_map_autCongr
    {K : Type u} {L : Type v} {M : Type w}
    [Field K] [Field L] [Field M]
    [Algebra K L] [Algebra K M]
    [Normal K L] [Normal K M]
    (e : L ≃ₐ[K] M) (B : ValuationSubring M) :
    Subgroup.map (AlgEquiv.autCongr e).toMonoidHom
        (RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroupInAut K
          (B.comap e.toRingHom)) =
      RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroupInAut K B

Module documentation

Valuation inertia under algebra equivalences

Declarations

autCongr_mem_valuationInertiaGroupInAut

autCongr_mem_valuationInertiaGroupInAut_iff

valuationInertiaGroupInAut_map_autCongr