Module

FiniteUnitBoundaryMuPPrimitive.lean

Nyll.GaloisCohomology.Kummer.FiniteUnitBoundaryMuPPrimitive

6 declarations indexed from sourceView source ↗

Module documentation

Correcting finite unit boundaries to absolute roots-of-unity boundaries

Suppose a finite Galois two-cochain with values in mu_p is the boundary of a unit-valued one-cochain b. Then b^p is a crossed homomorphism. Noether's Hilbert 90 produces its primitive u; a p-th root of u in the algebraic closure corrects b to a mu_p-valued primitive.

The resulting absolute primitive is continuous: both finite restriction and the orbit map of the chosen algebraic root are locally constant. The statement uses the natural Galois action and does not assume that the base contains mu_p or that the finite Galois group is a p-group. No new instances are introduced.

Imports2

Imported by3

theorem

finiteBoundary_power_isMulCocycle

L38 ↗

ClassFieldTower.Martinet.Shafarevich.finiteBoundary_power_isMulCocycle

Source context 8 commands

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

open scoped Pointwise Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory groupCohomology
variable (K : Type) [Field K] [CharZero K]
variable (p : ℕ) [Fact p.Prime]
variable (E : FiniteGaloisIntermediateField K (AlgebraicClosure K))
omit [CharZero K] [Fact p.Prime] in

Lean source · full declaration

theorem finiteBoundary_power_isMulCocycle
    (c : Gal(E/K) → Gal(E/K) → nthRootsSubgroup E p)
    (b : Gal(E/K) → Eˣ)
    (hb : ∀ s t : Gal(E/K),
      Units.map s (b t) * b s / b (s * t) = (c s t).1) :
    IsMulCocycle₁ (fun s => b s ^ p) := by
  intro s t
  have h := congrArg (fun x : Eˣ => x ^ p) (hb s t)
  rw [div_pow, mul_pow,
    (mem_nthRootsSubgroup_iff E).mp (c s t).2] at h
  rw [smul_pow', AlgEquiv.smul_units_def]
  exact (div_eq_one.mp h).symm

theorem

absoluteUnit_orbit_isLocallyConstant

L51 ↗

ClassFieldTower.Martinet.Shafarevich.absoluteUnit_orbit_isLocallyConstant

Source context 7 commands

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

open scoped Pointwise Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory groupCohomology
variable (K : Type) [Field K] [CharZero K]
variable (p : ℕ) [Fact p.Prime]
variable (E : FiniteGaloisIntermediateField K (AlgebraicClosure K))

Lean source · full declaration

theorem absoluteUnit_orbit_isLocallyConstant (u : (AlgebraicClosure K)ˣ) :
    IsLocallyConstant (fun sigma : Gal(AlgebraicClosure K/K) => sigma • u) := by
  rw [IsLocallyConstant.iff_exists_open]
  intro sigma
  let D := FiniteGaloisIntermediateField.adjoin K {(u : AlgebraicClosure K)}
  let H : Set Gal(AlgebraicClosure K/K) := D.fixingSubgroup
  refine ⟨sigma • H, (IntermediateField.fixingSubgroup_isOpen
    D.toIntermediateField).leftCoset sigma, ?_, ?_⟩
  · exact ⟨1, D.fixingSubgroup.one_mem, mul_one sigma⟩
  · intro tau htau
    rcases htau with ⟨h, hh, htau⟩
    have hfix : h • u = u := by
      apply Units.ext
      exact ((IntermediateField.mem_fixingSubgroup_iff D.toIntermediateField h).mp hh)
        (u : AlgebraicClosure K)
        (FiniteGaloisIntermediateField.subset_adjoin K {(u : AlgebraicClosure K)}
          (Set.mem_singleton _))
    change sigma * h = tau at htau
    rw [← htau, mul_smul, hfix]

theorem

finiteUnitInclusion_restriction_smul

L72 ↗

ClassFieldTower.Martinet.Shafarevich.finiteUnitInclusion_restriction_smul

Source context 8 commands

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

open scoped Pointwise Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory groupCohomology
variable (K : Type) [Field K] [CharZero K]
variable (p : ℕ) [Fact p.Prime]
variable (E : FiniteGaloisIntermediateField K (AlgebraicClosure K))
omit [CharZero K] in

Lean source · statement

theorem finiteUnitInclusion_restriction_smul
    (sigma : Gal(AlgebraicClosure K/K)) (u : Eˣ) :
    Units.map E.val.toMonoidHom
        (Units.map (AlgEquiv.restrictNormalHom E.toIntermediateField sigma) u) =
      sigma • Units.map E.val.toMonoidHom u

theorem

exists_absoluteUnit_root

L81 ↗

ClassFieldTower.Martinet.Shafarevich.exists_absoluteUnit_root

Source context 8 commands

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

open scoped Pointwise Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory groupCohomology
variable (K : Type) [Field K] [CharZero K]
variable (p : ℕ) [Fact p.Prime]
variable (E : FiniteGaloisIntermediateField K (AlgebraicClosure K))
omit [CharZero K] in

Lean source · statement

theorem exists_absoluteUnit_root (u : Eˣ) :
    ∃ v : (AlgebraicClosure K)ˣ,
      v ^ p = Units.map E.val.toMonoidHom u

theorem

divCochain_mulDiv

L94 ↗

ClassFieldTower.Martinet.Shafarevich.divCochain_mulDiv

Source context 7 commands

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

open scoped Pointwise Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory groupCohomology
variable (K : Type) [Field K] [CharZero K]
variable (p : ℕ) [Fact p.Prime]
variable (E : FiniteGaloisIntermediateField K (AlgebraicClosure K))

Lean source · statement

theorem divCochain_mulDiv {M : Type*} [CommGroup M] (a b c x y : M) :
    (a / x) * (b / y) / (c / (x * y)) = a * b / c

theorem

exists_absoluteMuP_primitive_of_finiteUnit_boundary

L102 ↗

ClassFieldTower.Martinet.Shafarevich.exists_absoluteMuP_primitive_of_finiteUnit_boundary

Documentation

A supplied finite unit boundary of a roots-of-unity two-cochain yields an actual continuous roots-of-unity primitive on the absolute Galois group. The boundary identity is recorded in the ambient unit group, whose inclusion of mu_p is injective.

Source context 7 commands

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

open scoped Pointwise Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory groupCohomology
variable (K : Type) [Field K] [CharZero K]
variable (p : ℕ) [Fact p.Prime]
variable (E : FiniteGaloisIntermediateField K (AlgebraicClosure K))

Lean source · statement

theorem exists_absoluteMuP_primitive_of_finiteUnit_boundary
    (c : Gal(E/K) → Gal(E/K) → nthRootsSubgroup E p)
    (b : Gal(E/K) → Eˣ)
    (hb : ∀ s t : Gal(E/K),
      Units.map s (b t) * b s / b (s * t) = (c s t).1) :
    ∃ a : C(Field.absoluteGaloisGroup K, AbsoluteMuP K p),
      ∀ s t : Field.absoluteGaloisGroup K,
        ((absoluteGaloisGroupContinuousMulEquiv K s) • (a t).toMul.1 :
            (AlgebraicClosure K)ˣ) *
            (a s).toMul.1 / (a (s * t)).toMul.1 =
          Units.map E.val.toMonoidHom
            (c (AlgEquiv.restrictNormalHom E.toIntermediateField
                (absoluteGaloisGroupContinuousMulEquiv K s))
              (AlgEquiv.restrictNormalHom E.toIntermediateField
                (absoluteGaloisGroupContinuousMulEquiv K t))).1

Module documentation

Correcting finite unit boundaries to absolute roots-of-unity boundaries

Declarations

finiteBoundary_power_isMulCocycle

absoluteUnit_orbit_isLocallyConstant

finiteUnitInclusion_restriction_smul

exists_absoluteUnit_root

divCochain_mulDiv

exists_absoluteMuP_primitive_of_finiteUnit_boundary