Skip to content

WIP: Import Local and global class field theory #506

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
Vilin97 wants to merge 47 commits into
base: main
Choose a base branch
from
Open

WIP: Import Local and global class field theory #506

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
47 commits
Select commit Hold shift + click to select a range
3a6be8e
Import Local and global class field theory with source attribution an…
Vilin97 Sep 21, 2026
2e2b5b3
Port complete upstream content to current Mathlib and improve lint co…
Vilin97 Sep 21, 2026
09a5f03
Split Kummer localization proof and simplify tensor composition
Vilin97 Sep 21, 2026
301da9a
Port finite-level idele class compositions and direct-limit actions
Vilin97 Sep 21, 2026
f19037f
Extract ambient field-equivariance compatibility for fixed points
Vilin97 Sep 21, 2026
9204a81
Make direct-limit action and transport elaboration explicit
Vilin97 Sep 21, 2026
e398ce1
Preserve local representative construction through existence and choice
Vilin97 Sep 21, 2026
3631110
Factor norm range transport for intrinsic Hilbert fields
Vilin97 Sep 21, 2026
a96861a
Apply checked whitespace suggestions and normalize source typography
Vilin97 Sep 21, 2026
d196ba5
Document and generalize the complete class field theory import
Vilin97 Sep 22, 2026
eff7466
Refactor valuation and principal-unit constructions into reusable lemmas
Vilin97 Sep 22, 2026
6a676d7
Factor norm transport and reciprocity proofs; isolate local instance …
Vilin97 Sep 22, 2026
ec39237
Refactor class field comparisons and clarify local imports
Vilin97 Sep 22, 2026
1e23d1b
Extract class field norm calculations and Frobenius fixed-field trans…
Vilin97 Sep 22, 2026
f4bc899
Split class field norm transports and primitive valuation calculations
Vilin97 Sep 22, 2026
1a19b5c
Merge remote-tracking branch 'origin/main' into pr-506
github-actions[bot] Sep 22, 2026
57b50b3
Merge remote-tracking branch 'origin/main' into pr-506
github-actions[bot] Sep 23, 2026
e65ff6b
Merge remote-tracking branch 'origin/main' into pr-506
github-actions[bot] Sep 23, 2026
7a2d402
Merge remote-tracking branch 'origin/main' into pr-506
github-actions[bot] Sep 24, 2026
6f5d337
Merge remote-tracking branch 'origin/main' into pr-506
github-actions[bot] Sep 24, 2026
92c3141
Restore project registration lost during automatic main merge
Vilin97 Sep 24, 2026
2d9fff9
Extract class field norm and reciprocity proof boundaries
Vilin97 Sep 25, 2026
2c77613
Migrate class field theory to public Lean modules
Vilin97 Sep 25, 2026
613413d
Preserve class field theory module interface repairs
Vilin97 Sep 25, 2026
523174b
Fix ClassFieldTheory module interfaces and preserve proof boundaries
Vilin97 Sep 25, 2026
b73a25b
Complete ClassFieldTheory interface and line-length cleanup
Vilin97 Sep 25, 2026
fc14845
Merge remote-tracking branch 'origin/main' into codex/import42-classf…
Vilin97 Sep 25, 2026
795dca4
Repair ClassFieldTheory interfaces and remove unused assumptions
Vilin97 Sep 25, 2026
c74f410
Repair ClassField public interfaces and owned import index
Vilin97 Sep 25, 2026
c8be341
Finish residue and localization proof boundaries
Vilin97 Sep 25, 2026
dcb924d
Preserve class field interfaces across public module boundaries
Vilin97 Sep 25, 2026
5977b41
Preserve ClassField public signatures and simplify unused assumptions
Vilin97 Sep 25, 2026
1fdec6c
Repair remaining class-field module interfaces and Herbrand callers
Vilin97 Sep 26, 2026
fcfa34e
Merge remote-tracking branch 'origin/main' into codex/import42-classf…
Vilin97 Sep 26, 2026
eb5525e
Remove identical duplicate Hasse–Minkowski registry card
Vilin97 Sep 26, 2026
f8639ee
Merge main and preserve all YAML project registrations
Vilin97 Sep 26, 2026
f9255fd
Repair class field module interfaces and retain finite witnesses
Vilin97 Sep 26, 2026
d96ba88
Merge remote-tracking branch 'origin/main' into pr-506
github-actions[bot] Sep 26, 2026
2dabf82
Merge remote-tracking branch 'origin/main' into pr-506
github-actions[bot] Sep 26, 2026
cbed49b
Merge remote-tracking branch 'origin/main' into pr-506
github-actions[bot] Sep 26, 2026
9a2bc40
Fix class field reciprocity and characteristic instances
Vilin97 Sep 26, 2026
702b005
fix(ClassFieldTheory): complete canonical instance and module boundaries
Vilin97 Sep 26, 2026
ae50279
Merge remote-tracking branch 'origin/main' into pr-506
github-actions[bot] Sep 26, 2026
e344974
Fix class field completion and fixed-field elaboration
Vilin97 Sep 26, 2026
b998eee
Merge remote-tracking branch 'origin/main' into pr-506
github-actions[bot] Sep 26, 2026
0598625
Merge remote-tracking branch 'origin/main' into pr-506
github-actions[bot] Sep 26, 2026
73ef392
Merge remote-tracking branch 'origin/main' into pr-506
github-actions[bot] Sep 26, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
The table of contents is too big for display.
Diff view
Diff view
  •  
  •  
  •  
1,822 changes: 1,822 additions & 0 deletions LeanPool.lean
View file
Open in desktop

Large diffs are not rendered by default.

1,840 changes: 1,840 additions & 0 deletions LeanPool/ClassFieldTheory.lean
View file
Open in desktop

Large diffs are not rendered by default.

25 changes: 25 additions & 0 deletions LeanPool/ClassFieldTheory/ClassFieldTheory.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,25 @@
/-
Copyright (c) 2026 n-yamaguchi-0729. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: n-yamaguchi-0729
-/
module


public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory
public import LeanPool.ClassFieldTheory.ClassFieldTheory.Algebra
public import LeanPool.ClassFieldTheory.ClassFieldTheory.AlgebraicNumberTheory
public import LeanPool.ClassFieldTheory.ClassFieldTheory.All
public import LeanPool.ClassFieldTheory.ClassFieldTheory.Definitions
public import LeanPool.ClassFieldTheory.ClassFieldTheory.GlobalClassFieldTheory
public import LeanPool.ClassFieldTheory.ClassFieldTheory.HasseArf
public import LeanPool.ClassFieldTheory.ClassFieldTheory.KroneckerWeber
public import LeanPool.ClassFieldTheory.ClassFieldTheory.KummerTheory
public import LeanPool.ClassFieldTheory.ClassFieldTheory.LocalClassFieldTheory
public import LeanPool.ClassFieldTheory.ClassFieldTheory.LocalFieldTheory
public import LeanPool.ClassFieldTheory.ClassFieldTheory.LubinTate
public import LeanPool.ClassFieldTheory.ClassFieldTheory.RamificationTheory
public import LeanPool.ClassFieldTheory.ClassFieldTheory.Theorems

/-! Supporting modules for Local and global class field theory. -/

14 changes: 14 additions & 0 deletions LeanPool/ClassFieldTheory/ClassFieldTheory/AbstractClassFieldTheory.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
/-
Copyright (c) 2026 n-yamaguchi-0729. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: n-yamaguchi-0729
-/
module


public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.All
public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Degree
public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity

/-! Supporting modules for Local and global class field theory. -/

24 changes: 24 additions & 0 deletions LeanPool/ClassFieldTheory/ClassFieldTheory/AbstractClassFieldTheory/All.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,24 @@
/-
Copyright (c) 2026 n-yamaguchi-0729. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: n-yamaguchi-0729
-/
module


public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Degree.All
public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.All
/-!
# Abstract class field theory

Public root for abstract degree data, class formations, reciprocity, and the construction and
naturality of Artin maps. The public declarations live in the `ClassFormation` namespace. This
library is independent of local class field theory.

The representation-free degree, field, extension, and topological-generation
APIs are universe-polymorphic. The boundary that uses Mathlib's `Rep ℤ G` is
necessarily universe zero because `Rep` currently places its coefficient ring
and acting group in the same universe; the affected source sections state that
constraint explicitly.
-/

25 changes: 25 additions & 0 deletions LeanPool/ClassFieldTheory/ClassFieldTheory/AbstractClassFieldTheory/Degree.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,25 @@
/-
Copyright (c) 2026 n-yamaguchi-0729. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: n-yamaguchi-0729
-/
module


public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Degree.All
public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Degree.Fields
public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Degree.Frobenius
public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Degree.FrobeniusFixedField
public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Degree.FrobeniusLift
public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Degree.Indices
public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Degree.Norm
public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Degree.NormConjugation
public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Degree.NormLaws
public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Degree.PadicCyclicClosure
public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Degree.PrimeElements
public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Degree.ProfiniteIntegerFiniteQuotient
public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Degree.Valuation
public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Degree.ValuationLaws

/-! Supporting modules for Local and global class field theory. -/

28 changes: 28 additions & 0 deletions LeanPool/ClassFieldTheory/ClassFieldTheory/AbstractClassFieldTheory/Degree/All.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,28 @@
/-
Copyright (c) 2026 n-yamaguchi-0729. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: n-yamaguchi-0729
-/
module


public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Degree.Fields
public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Degree.Frobenius
public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Degree.FrobeniusFixedField
public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Degree.FrobeniusLift
public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Degree.Indices
public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Degree.Norm
public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Degree.NormConjugation
public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Degree.NormLaws
public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Degree.PadicCyclicClosure
public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Degree.PrimeElements
public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Degree.ProfiniteIntegerFiniteQuotient
public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Degree.Valuation
public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Degree.ValuationLaws
/-!
# Degree and valuation data

Focused aggregate for abstract fields, normalized degrees, Frobenius, norms, prime elements, and
valuation laws used by class formations.
-/

Loading
Loading