NYLL
Module

CharacterExact.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.CharacterExact
11 declarations indexed from sourceView source ↗

Module documentation

Hilbert ramification theory: character exactness

This file contains the exactness and quotient consequences of the character constructed in CharacterMap. It is the exactness part of the inertia-character exact sequence that does not require the finite-cardinality surjectivity argument onto the full group Hom(Delta/Gamma, lambda*).

Imports1
Imported by1

Declarations

abbrev

ramificationGroupInValueTrivialInertiaGroup

L33 ↗
RamificationTheory.HilbertRamification.ValuationSubring.ramificationGroupInValueTrivialInertiaGroup
Documentation

The ramification subgroup, viewed inside the value-trivial inertia group that carries the residue-unit character.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
Lean source · statement
abbrev ramificationGroupInValueTrivialInertiaGroup
    (A : _root_.ValuationSubring L) :
    Subgroup (valueTrivialInertiaGroup K A)
theorem

mem_ramificationGroupInValueTrivialInertiaGroup_iff

L39 ↗
RamificationTheory.HilbertRamification.ValuationSubring.mem_ramificationGroupInValueTrivialInertiaGroup_iff
Documentation

States the theorem mem_ramificationGroupInValueTrivialInertiaGroup_iff.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem mem_ramificationGroupInValueTrivialInertiaGroup_iff
    (A : _root_.ValuationSubring L) (σ : valueTrivialInertiaGroup K A) :
    σ ∈ ramificationGroupInValueTrivialInertiaGroup K A ↔
      (σ : inertiaGroup K A) ∈ ramificationGroup K A
instance

ramificationGroupInValueTrivialInertiaGroup_normal

L46 ↗
RamificationTheory.HilbertRamification.ValuationSubring.ramificationGroupInValueTrivialInertiaGroup_normal
Documentation

Provides the instance ramificationGroupInValueTrivialInertiaGroup_normal.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
Lean source · statement
instance ramificationGroupInValueTrivialInertiaGroup_normal
    (A : _root_.ValuationSubring L) :
    (ramificationGroupInValueTrivialInertiaGroup K A).Normal
theorem

ramificationGroupInValueTrivialInertiaGroup_eq_characterHom_ker

L54 ↗
RamificationTheory.HilbertRamification.ValuationSubring.ramificationGroupInValueTrivialInertiaGroup_eq_characterHom_ker
Documentation

Inertia-character exactness: inside value-trivial inertia, the kernel of the character map is exactly R_w.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem ramificationGroupInValueTrivialInertiaGroup_eq_characterHom_ker
    (A : _root_.ValuationSubring L) :
    ramificationGroupInValueTrivialInertiaGroup K A =
      (valueTrivialInertiaCharacterHom K A).ker
theorem

valueTrivialCharacter_mulExact

L65 ↗
RamificationTheory.HilbertRamification.ValuationSubring.valueTrivialCharacter_mulExact
Documentation

Inertia-character exactness: R_w -> I_w -> Hom(Delta/Gamma, lambda*) is exact at value-trivial inertia. The target is the concrete character group produced in CharacterMap.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem valueTrivialCharacter_mulExact
    (A : _root_.ValuationSubring L) :
    Function.MulExact
      (ramificationGroupInValueTrivialInertiaGroup K A).subtype
      (valueTrivialInertiaCharacterHom K A)
theorem

valueTrivialCharacter_mulExactRange

L78 ↗
RamificationTheory.HilbertRamification.ValuationSubring.valueTrivialCharacter_mulExactRange
Documentation

Inertia-character exactness: the same exactness after restricting the target to the range of the character map.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem valueTrivialCharacter_mulExactRange
    (A : _root_.ValuationSubring L) :
    Function.MulExact
      (ramificationGroupInValueTrivialInertiaGroup K A).subtype
      (valueTrivialInertiaCharacterHom K A).rangeRestrict
abbrev

valueTrivialInertiaCharacterRange

L89 ↗
RamificationTheory.HilbertRamification.ValuationSubring.valueTrivialInertiaCharacterRange
Documentation

The character map, with codomain restricted to its range.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
Lean source · statement
abbrev valueTrivialInertiaCharacterRange
    (A : _root_.ValuationSubring L) :
    Subgroup
      ((Lˣ ⧸ A.unitGroup) ⧸ baseUnitValueClassSubgroup K A →*
        (IsLocalRing.ResidueField A)ˣ)
theorem

valueTrivialInertiaCharacter_rangeRestrict_surjective

L97 ↗
RamificationTheory.HilbertRamification.ValuationSubring.valueTrivialInertiaCharacter_rangeRestrict_surjective
Documentation

The value-trivial character map is onto its range.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem valueTrivialInertiaCharacter_rangeRestrict_surjective
    (A : _root_.ValuationSubring L) :
    Function.Surjective
      (valueTrivialInertiaCharacterHom K A).rangeRestrict
theorem

valueTrivialCharacter_shortExactRange

L106 ↗
RamificationTheory.HilbertRamification.ValuationSubring.valueTrivialCharacter_shortExactRange
Documentation

The inertia-character exact sequence range form: 1 -> R_w -> I_w^{value=1} -> im(χ) -> 1.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem valueTrivialCharacter_shortExactRange
    (A : _root_.ValuationSubring L) :
    Function.Injective
        (ramificationGroupInValueTrivialInertiaGroup K A).subtype ∧
      Function.MulExact
        (ramificationGroupInValueTrivialInertiaGroup K A).subtype
        (valueTrivialInertiaCharacterHom K A).rangeRestrict ∧
      Function.Surjective
        (valueTrivialInertiaCharacterHom K A).rangeRestrict
def

valueTrivialInertiaQuotientRamificationEquivCharacterRange

L123 ↗
RamificationTheory.HilbertRamification.ValuationSubring.valueTrivialInertiaQuotientRamificationEquivCharacterRange
Documentation

The inertia-character exact sequence first-isomorphism form: I_w^{value=1}/R_w is canonically the range of the character map.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
Lean source · statement
def valueTrivialInertiaQuotientRamificationEquivCharacterRange
    (A : _root_.ValuationSubring L) :
    valueTrivialInertiaGroup K A ⧸
        ramificationGroupInValueTrivialInertiaGroup K A ≃*
      valueTrivialInertiaCharacterRange K A
theorem

valueTrivialInertiaQuotientRamificationEquivCharacterRange_mk

L135 ↗
RamificationTheory.HilbertRamification.ValuationSubring.valueTrivialInertiaQuotientRamificationEquivCharacterRange_mk
Documentation

States the theorem valueTrivialInertiaQuotientRamificationEquivCharacterRange_mk.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem valueTrivialInertiaQuotientRamificationEquivCharacterRange_mk
    (A : _root_.ValuationSubring L) (σ : valueTrivialInertiaGroup K A) :
    valueTrivialInertiaQuotientRamificationEquivCharacterRange
        (K := K) A
        (QuotientGroup.mk'
          (ramificationGroupInValueTrivialInertiaGroup K A) σ) =
      (valueTrivialInertiaCharacterHom K A).rangeRestrict σ

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