NYLL
Module

UnramifiedDegreeBaseChange.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Local.UnramifiedDegreeBaseChange
2 declarations indexed from sourceView source ↗

Module documentation

Base change of standard unramified degree kernels

If an extension has relative residue degree f, then intersecting its absolute subgroup with the standard unramified degree-f * m subgroup produces its own standard unramified degree-m subgroup. Both sides use the actual normalized degree maps.

Imports7
Imported by2

Declarations

theorem

zHatReduction_mul_nsmul_eq_zero_iff

L26 ↗
ClassFormation.zHatReduction_mul_nsmul_eq_zero_iff
Source context 1 command

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

namespace ClassFormation
Lean source · statement
theorem zHatReduction_mul_nsmul_eq_zero_iff
    (f m : ℕ) (hf : 0 < f) (hm : 0 < m) (z : ZHat) :
    zHatReduction (f * m) (Nat.mul_pos hf hm) (f • z) = 0 ↔
      zHatReduction m hm z = 0
theorem

unramifiedExtensionOfDegree_baseChange_mul

L63 ↗
ClassFormation.DegreeData.unramifiedExtensionOfDegree_baseChange_mul
Documentation

The actual unramified degree kernels commute with base change after multiplying the downstairs degree by the relative residue degree.

Source context 4 commands

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

namespace ClassFormation
namespace DegreeData
universe u
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem unramifiedExtensionOfDegree_baseChange_mul
    (D : DegreeData G) (E : FiniteResidueAbstractExtension D)
    (m : ℕ) (hm : 0 < m) :
    D.unramifiedExtensionOfDegree E.field m hm =
      E.field.field ⊓ D.unramifiedExtensionOfDegree E.base
        ((E.residueDegree : ℕ) * m) (Nat.mul_pos E.residueDegree.property hm)

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