NYLL
Module

AbsoluteMuPKummerComparison.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Kummer.AbsoluteMuPKummerComparison
15 declarations indexed from sourceView source ↗

Module documentation

Comparing natural and trivial-coefficient absolute Kummer H¹

Over a field containing a primitive p-th root of unity, the natural mu_p representation is trivial. This file transports its continuous cohomology through that trivialization and proves that the natural coefficient Kummer map becomes the usual ZMod p-character Kummer map.

Imports4
Imported by4

Declarations

instance

absoluteMuPComparisonH1Module

L30 ↗
ClassFieldTower.Martinet.Shafarevich.absoluteMuPComparisonH1Module
Source context 5 commands

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

open scoped Pointwise Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open CategoryTheory KummerTheory TopRep ContRepresentation
open ClassFieldTower.ProP
Lean source · statement
instance absoluteMuPComparisonH1Module
    {q : ℕ} {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G))
def

absoluteMuPCochainsIsoTrivial

L40 ↗
ClassFieldTower.Martinet.Shafarevich.absoluteMuPCochainsIsoTrivial
Documentation

The coefficient trivialization induces an isomorphism on homogeneous continuous cochain complexes.

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 CategoryTheory KummerTheory TopRep ContRepresentation
open ClassFieldTower.ProP
local instance absoluteMuPComparisonH1Module
    {q : ℕ} {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G)) :=
  continuousH1ZModModule
variable (K : Type) [Field K] [CharZero K]
variable (p : ℕ) [Fact p.Prime]
Lean source · full declaration
def absoluteMuPCochainsIsoTrivial
    (hmu : (primitiveRoots p K).Nonempty) :
    TopRep.homogeneousCochains (absoluteMuPTopRep K p) ≅
      TopRep.homogeneousCochains
        (ClassFieldTower.Cohomology.trivialZModP p
          (Field.absoluteGaloisGroup K)) where
  hom := ContinuousCohomology.cochainsMap
    (ContinuousMonoidHom.id (Field.absoluteGaloisGroup K))
    (absoluteMuPTopRepTrivialIso K p hmu).hom
  inv := ContinuousCohomology.cochainsMap
    (ContinuousMonoidHom.id (Field.absoluteGaloisGroup K))
    (absoluteMuPTopRepTrivialIso K p hmu).inv
  hom_inv_id := by
    refine (ContinuousCohomology.cochainsMap_comp
      (X := absoluteMuPTopRep K p)
      (Y := ClassFieldTower.Cohomology.trivialZModP p
        (Field.absoluteGaloisGroup K))
      (Z := absoluteMuPTopRep K p)
      (ContinuousMonoidHom.id (Field.absoluteGaloisGroup K))
      (ContinuousMonoidHom.id (Field.absoluteGaloisGroup K))
      (absoluteMuPTopRepTrivialIso K p hmu).hom
      (absoluteMuPTopRepTrivialIso K p hmu).inv).symm.trans ?_
    have hcoeff :
        (TopRep.resFunctor
          ((ContinuousMonoidHom.id (Field.absoluteGaloisGroup K)) :
            Field.absoluteGaloisGroup K →* Field.absoluteGaloisGroup K)).map
            (absoluteMuPTopRepTrivialIso K p hmu).hom ≫
          (absoluteMuPTopRepTrivialIso K p hmu).inv =
        𝟙 (absoluteMuPTopRep K p) := by
      exact (absoluteMuPTopRepTrivialIso K p hmu).hom_inv_id
    exact (congrArg
      (fun f : absoluteMuPTopRep K p ⟶ absoluteMuPTopRep K p =>
        ContinuousCohomology.cochainsMap
          (X := absoluteMuPTopRep K p) (Y := absoluteMuPTopRep K p)
          (ContinuousMonoidHom.id (Field.absoluteGaloisGroup K)) f) hcoeff).trans
      (ContinuousCohomology.cochainsMap_id (absoluteMuPTopRep K p))
  inv_hom_id := by
    refine (ContinuousCohomology.cochainsMap_comp
      (X := ClassFieldTower.Cohomology.trivialZModP p
        (Field.absoluteGaloisGroup K))
      (Y := absoluteMuPTopRep K p)
      (Z := ClassFieldTower.Cohomology.trivialZModP p
        (Field.absoluteGaloisGroup K))
      (ContinuousMonoidHom.id (Field.absoluteGaloisGroup K))
      (ContinuousMonoidHom.id (Field.absoluteGaloisGroup K))
      (absoluteMuPTopRepTrivialIso K p hmu).inv
      (absoluteMuPTopRepTrivialIso K p hmu).hom).symm.trans ?_
    have hcoeff :
        (TopRep.resFunctor
          ((ContinuousMonoidHom.id (Field.absoluteGaloisGroup K)) :
            Field.absoluteGaloisGroup K →* Field.absoluteGaloisGroup K)).map
            (absoluteMuPTopRepTrivialIso K p hmu).inv ≫
          (absoluteMuPTopRepTrivialIso K p hmu).hom =
        𝟙 (ClassFieldTower.Cohomology.trivialZModP p
          (Field.absoluteGaloisGroup K)) := by
      exact (absoluteMuPTopRepTrivialIso K p hmu).inv_hom_id
    exact (congrArg
      (fun f : ClassFieldTower.Cohomology.trivialZModP p
          (Field.absoluteGaloisGroup K) ⟶
          ClassFieldTower.Cohomology.trivialZModP p
            (Field.absoluteGaloisGroup K) =>
        ContinuousCohomology.cochainsMap
          (X := ClassFieldTower.Cohomology.trivialZModP p
            (Field.absoluteGaloisGroup K))
          (Y := ClassFieldTower.Cohomology.trivialZModP p
            (Field.absoluteGaloisGroup K))
          (ContinuousMonoidHom.id (Field.absoluteGaloisGroup K)) f) hcoeff).trans
      (ContinuousCohomology.cochainsMap_id
        (ClassFieldTower.Cohomology.trivialZModP p
          (Field.absoluteGaloisGroup K)))
def

absoluteMuPContinuousCohomologyIsoTrivial

L113 ↗
ClassFieldTower.Martinet.Shafarevich.absoluteMuPContinuousCohomologyIsoTrivial
Documentation

Cohomology with natural mu_p coefficients transported to the standard trivial ZMod p coefficient representation.

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 CategoryTheory KummerTheory TopRep ContRepresentation
open ClassFieldTower.ProP
local instance absoluteMuPComparisonH1Module
    {q : ℕ} {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G)) :=
  continuousH1ZModModule
variable (K : Type) [Field K] [CharZero K]
variable (p : ℕ) [Fact p.Prime]
Lean source · statement
def absoluteMuPContinuousCohomologyIsoTrivial
    (hmu : (primitiveRoots p K).Nonempty) (n : ℕ) :
    continuousCohomology n (absoluteMuPTopRep K p) ≅
      ClassFieldTower.Cohomology.continuousCohomologyZModP p
        (Field.absoluteGaloisGroup K) n
def

absoluteMuPContinuousCohomologyLinearEquivTrivial

L124 ↗
ClassFieldTower.Martinet.Shafarevich.absoluteMuPContinuousCohomologyLinearEquivTrivial
Documentation

Linear form of the cohomology transport induced by coefficient trivialization.

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 CategoryTheory KummerTheory TopRep ContRepresentation
open ClassFieldTower.ProP
local instance absoluteMuPComparisonH1Module
    {q : ℕ} {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G)) :=
  continuousH1ZModModule
variable (K : Type) [Field K] [CharZero K]
variable (p : ℕ) [Fact p.Prime]
Lean source · statement
def absoluteMuPContinuousCohomologyLinearEquivTrivial
    (hmu : (primitiveRoots p K).Nonempty) (n : ℕ) :
    continuousCohomology n (absoluteMuPTopRep K p) ≃ₗ[ZMod p]
      ClassFieldTower.Cohomology.continuousCohomologyZModP p
        (Field.absoluteGaloisGroup K) n
theorem

absoluteMuPContinuousCohomologyLinearEquivTrivial_apply

L134 ↗
ClassFieldTower.Martinet.Shafarevich.absoluteMuPContinuousCohomologyLinearEquivTrivial_apply
Source context 9 commands

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

open scoped Pointwise Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open CategoryTheory KummerTheory TopRep ContRepresentation
open ClassFieldTower.ProP
local instance absoluteMuPComparisonH1Module
    {q : ℕ} {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G)) :=
  continuousH1ZModModule
variable (K : Type) [Field K] [CharZero K]
variable (p : ℕ) [Fact p.Prime]
omit [CharZero K] in
Lean source · statement
theorem absoluteMuPContinuousCohomologyLinearEquivTrivial_apply
    (hmu : (primitiveRoots p K).Nonempty) (n : ℕ)
    (x : continuousCohomology n (absoluteMuPTopRep K p)) :
    absoluteMuPContinuousCohomologyLinearEquivTrivial K p hmu n x =
      ContinuousCohomology.map
        (ContinuousMonoidHom.id (Field.absoluteGaloisGroup K))
        (absoluteMuPTopRepTrivialIso K p hmu).hom n x
theorem

absoluteMuPCochainsIsoTrivial_hom_f_one_apply

L145 ↗
ClassFieldTower.Martinet.Shafarevich.absoluteMuPCochainsIsoTrivial_hom_f_one_apply
Source context 9 commands

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

open scoped Pointwise Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open CategoryTheory KummerTheory TopRep ContRepresentation
open ClassFieldTower.ProP
local instance absoluteMuPComparisonH1Module
    {q : ℕ} {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G)) :=
  continuousH1ZModModule
variable (K : Type) [Field K] [CharZero K]
variable (p : ℕ) [Fact p.Prime]
omit [CharZero K] in
Lean source · statement
theorem absoluteMuPCochainsIsoTrivial_hom_f_one_apply
    (hmu : (primitiveRoots p K).Nonempty)
    (c : (TopRep.homogeneousCochains (absoluteMuPTopRep K p)).X 1)
    (g h : Field.absoluteGaloisGroup K) :
    (((ContinuousCohomology.cochainsMap
      (ContinuousMonoidHom.id (Field.absoluteGaloisGroup K))
      (absoluteMuPTopRepTrivialIso K p hmu).hom).f 1).hom c).1 g h =
      absoluteMuPLinearEquivZMod K p hmu (c.1 g h)
def

absoluteMuPH1EquivContinuousH1ZMod

L157 ↗
ClassFieldTower.Martinet.Shafarevich.absoluteMuPH1EquivContinuousH1ZMod
Documentation

In degree one, coefficient trivialization followed by the standard cohomology-character bridge.

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 CategoryTheory KummerTheory TopRep ContRepresentation
open ClassFieldTower.ProP
local instance absoluteMuPComparisonH1Module
    {q : ℕ} {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G)) :=
  continuousH1ZModModule
variable (K : Type) [Field K] [CharZero K]
variable (p : ℕ) [Fact p.Prime]
Lean source · statement
def absoluteMuPH1EquivContinuousH1ZMod
    (hmu : (primitiveRoots p K).Nonempty) :
    continuousCohomology 1 (absoluteMuPTopRep K p) ≃ₗ[ZMod p]
      ContinuousH1ZMod
        (p := p) (G := Field.absoluteGaloisGroup K)
def

absoluteContinuousZModCharacterH1LinearEquiv

L167 ↗
ClassFieldTower.Martinet.Shafarevich.absoluteContinuousZModCharacterH1LinearEquiv
Documentation

Continuous multiplicative ZMod p characters, reinterpreted as additive continuous H¹ classes.

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 CategoryTheory KummerTheory TopRep ContRepresentation
open ClassFieldTower.ProP
local instance absoluteMuPComparisonH1Module
    {q : ℕ} {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G)) :=
  continuousH1ZModModule
variable (K : Type) [Field K] [CharZero K]
variable (p : ℕ) [Fact p.Prime]
Lean source · statement
def absoluteContinuousZModCharacterH1LinearEquiv :
    absoluteContinuousZModCharacterModP K p ≃ₗ[ZMod p]
      ContinuousH1ZMod
        (p := p) (G := Field.absoluteGaloisGroup K)
theorem

absoluteContinuousZModCharacterH1LinearEquiv_apply

L187 ↗
ClassFieldTower.Martinet.Shafarevich.absoluteContinuousZModCharacterH1LinearEquiv_apply
Source context 9 commands

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

open scoped Pointwise Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open CategoryTheory KummerTheory TopRep ContRepresentation
open ClassFieldTower.ProP
local instance absoluteMuPComparisonH1Module
    {q : ℕ} {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G)) :=
  continuousH1ZModModule
variable (K : Type) [Field K] [CharZero K]
variable (p : ℕ) [Fact p.Prime]
omit [CharZero K] [Fact p.Prime] in
Lean source · full declaration
theorem absoluteContinuousZModCharacterH1LinearEquiv_apply
    (chi : absoluteContinuousZModCharacterModP K p)
    (sigma : Field.absoluteGaloisGroup K) :
    absoluteContinuousZModCharacterH1LinearEquiv K p chi
        (Additive.ofMul sigma) =
      (Additive.toMul
        (show Additive
            (Field.absoluteGaloisGroup K →ₜ* Multiplicative (ZMod p))
          from chi) sigma).toAdd :=
  rfl
def

absoluteKummerContinuousH1LinearEquiv

L200 ↗
ClassFieldTower.Martinet.Shafarevich.absoluteKummerContinuousH1LinearEquiv
Documentation

The usual character-valued absolute Kummer equivalence, expressed in the additive continuous-H¹ convention.

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 CategoryTheory KummerTheory TopRep ContRepresentation
open ClassFieldTower.ProP
local instance absoluteMuPComparisonH1Module
    {q : ℕ} {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G)) :=
  continuousH1ZModModule
variable (K : Type) [Field K] [CharZero K]
variable (p : ℕ) [Fact p.Prime]
Lean source · statement
def absoluteKummerContinuousH1LinearEquiv
    (hmu : (primitiveRoots p K).Nonempty) :
    absolutePowerClassModP K p ≃ₗ[ZMod p]
      ContinuousH1ZMod
        (p := p) (G := Field.absoluteGaloisGroup K)
theorem

absoluteKummerContinuousZModCharacterLinearEquiv_mk_apply

L208 ↗
ClassFieldTower.Martinet.Shafarevich.absoluteKummerContinuousZModCharacterLinearEquiv_mk_apply
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 CategoryTheory KummerTheory TopRep ContRepresentation
open ClassFieldTower.ProP
local instance absoluteMuPComparisonH1Module
    {q : ℕ} {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G)) :=
  continuousH1ZModModule
variable (K : Type) [Field K] [CharZero K]
variable (p : ℕ) [Fact p.Prime]
Lean source · full declaration
theorem absoluteKummerContinuousZModCharacterLinearEquiv_mk_apply
    (hmu : (primitiveRoots p K).Nonempty) (a : Kˣ)
    (sigma : Field.absoluteGaloisGroup K) :
    ((show Additive
        (Field.absoluteGaloisGroup K →ₜ* Multiplicative (ZMod p)) from
      absoluteKummerContinuousZModCharacterLinearEquiv K p hmu
        (Additive.ofMul
          (QuotientGroup.mk'
            (powMonoidHom p : Kˣ →* Kˣ).range a))).toMul sigma).toAdd =
      absoluteMuPLinearEquivZMod K p hmu
        (absoluteKummerMuPRootCocycle K p a sigma) := by
  rfl
theorem

absoluteKummerContinuousH1LinearEquiv_mk_apply

L222 ↗
ClassFieldTower.Martinet.Shafarevich.absoluteKummerContinuousH1LinearEquiv_mk_apply
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 CategoryTheory KummerTheory TopRep ContRepresentation
open ClassFieldTower.ProP
local instance absoluteMuPComparisonH1Module
    {q : ℕ} {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G)) :=
  continuousH1ZModModule
variable (K : Type) [Field K] [CharZero K]
variable (p : ℕ) [Fact p.Prime]
Lean source · statement
theorem absoluteKummerContinuousH1LinearEquiv_mk_apply
    (hmu : (primitiveRoots p K).Nonempty) (a : Kˣ)
    (sigma : Field.absoluteGaloisGroup K) :
    absoluteKummerContinuousH1LinearEquiv K p hmu
        (Additive.ofMul
          (QuotientGroup.mk'
            (powMonoidHom p : Kˣ →* Kˣ).range a))
        (Additive.ofMul sigma) =
      absoluteMuPLinearEquivZMod K p hmu
        (absoluteKummerMuPRootCocycle K p a sigma)
theorem

absoluteMuPCocyclesMap_kummer_eq

L237 ↗
ClassFieldTower.Martinet.Shafarevich.absoluteMuPCocyclesMap_kummer_eq
Documentation

Mapping the natural-coefficient Kummer cocycle through coefficient trivialization gives the cocycle attached to the usual Kummer character.

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 CategoryTheory KummerTheory TopRep ContRepresentation
open ClassFieldTower.ProP
local instance absoluteMuPComparisonH1Module
    {q : ℕ} {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G)) :=
  continuousH1ZModModule
variable (K : Type) [Field K] [CharZero K]
variable (p : ℕ) [Fact p.Prime]
Lean source · statement
theorem absoluteMuPCocyclesMap_kummer_eq
    (hmu : (primitiveRoots p K).Nonempty) (a : Kˣ) :
    ContinuousCohomology.cocyclesMap
        (ContinuousMonoidHom.id (Field.absoluteGaloisGroup K))
        (absoluteMuPTopRepTrivialIso K p hmu).hom 1
        (absoluteKummerMuPHomogeneousOneCocycle K p a) =
      ClassFieldTower.Cohomology.cocycleOfH1
        (absoluteKummerContinuousH1LinearEquiv K p hmu
          (Additive.ofMul
            (QuotientGroup.mk'
              (powMonoidHom p : Kˣ →* Kˣ).range a)))
theorem

absoluteMuPH1EquivContinuousH1ZMod_kummerClass

L274 ↗
ClassFieldTower.Martinet.Shafarevich.absoluteMuPH1EquivContinuousH1ZMod_kummerClass
Documentation

The natural mu_p Kummer class becomes the standard continuous character-valued Kummer class after coefficient trivialization.

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 CategoryTheory KummerTheory TopRep ContRepresentation
open ClassFieldTower.ProP
local instance absoluteMuPComparisonH1Module
    {q : ℕ} {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G)) :=
  continuousH1ZModModule
variable (K : Type) [Field K] [CharZero K]
variable (p : ℕ) [Fact p.Prime]
Lean source · statement
theorem absoluteMuPH1EquivContinuousH1ZMod_kummerClass
    (hmu : (primitiveRoots p K).Nonempty) (a : Kˣ) :
    absoluteMuPH1EquivContinuousH1ZMod K p hmu
        (absoluteKummerMuPH1Class K p a) =
      absoluteKummerContinuousH1LinearEquiv K p hmu
        (Additive.ofMul
          (QuotientGroup.mk'
            (powMonoidHom p : Kˣ →* Kˣ).range a))
theorem

absoluteMuPKummerH1LinearMap_compare

L320 ↗
ClassFieldTower.Martinet.Shafarevich.absoluteMuPKummerH1LinearMap_compare
Documentation

Linear-map form of the absolute Kummer comparison.

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 CategoryTheory KummerTheory TopRep ContRepresentation
open ClassFieldTower.ProP
local instance absoluteMuPComparisonH1Module
    {q : ℕ} {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G)) :=
  continuousH1ZModModule
variable (K : Type) [Field K] [CharZero K]
variable (p : ℕ) [Fact p.Prime]
Lean source · statement
theorem absoluteMuPKummerH1LinearMap_compare
    (hmu : (primitiveRoots p K).Nonempty) :
    (absoluteMuPH1EquivContinuousH1ZMod K p hmu).toLinearMap.comp
        (absoluteKummerMuPH1LinearMap K p) =
      (absoluteKummerContinuousH1LinearEquiv K p hmu).toLinearMap

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