Standalone Lean project
A Lean development of local and global class field theory and its algebraic foundations.
Flagship declarations
continuous_algebraMap_of_density
Plain-language statement
Maddy's Lemma : Density implies continuity.
Source project: Class Field Theory
Person-level attribution pending.
exists_valuation_algebraMap_eq_valuation_pow
Plain-language statement
Andrew's Lemma : Density for algebraic extensions.
Source project: Class Field Theory
Person-level attribution pending.
groupCohomology.exists_of_surjective
Plain-language statement
Given map f: M ⟶ N and q : ℕ, if H^{q+1}(M) ⟶ H^{q+1}(N) is surjective, then any z : Z^{q+1}(N) can be written as f(z') + d(y) for some z' : Z^{q+1}(M) and y : C^q(M). Note that d is spelled as toCocycles.
Source project: Class Field Theory
Person-level attribution pending.
groupCohomology.infl_δ_naturality
Plain-language statement
Assume that we have a short exact sequence 0 → A → B → C → 0 in Rep R G and that the sequence of H- invariants is also a short exact in Rep R (G ⧸ H) : 0 → Aᴴ → Bᴴ → Cᴴ → 0. Then we have a commuting square Hⁿ(G ⧸ H, Cᴴ) ⟶ H^{n+1}(G ⧸ H, Aᴴ) | | ↓ ↓ Hⁿ(G , C) ⟶ H^{n+1}(G,A) where the horizontal maps are connecting homomorphisms an...
Source project: Class Field Theory
Person-level attribution pending.
groupCohomology.rest_δ_naturality
Plain-language statement
Given any short exact sewuence 0 → A → B → C → 0 in Rep R G and any subgroup H of G, the following diagram is commutative Hⁿ(G,C) ⟶ H^{n+1}(G A) | | ↓ ↓ Hⁿ(H,C) ⟶ H^{n+1}(G A). The vertical arrows are restriction and the horizontals are connecting homomorphisms. For this, it would be sensible to define restriction as a natural transformation, so t...
Source project: Class Field Theory
Person-level attribution pending.
groupCohomology.trivialCohomology_of_even_of_odd
Project documentation
If H²ⁿ⁺²(H,M) and H²ᵐ⁺¹(H,M) are both zero for every subgroup H of G then M is acyclic. -/ theorem groupCohomology.trivialCohomology_of_even_of_odd_of_solvable [Finite G] [Group.IsSolvable G] (M : Rep R G) (n m : ℕ) -- todo: don't quantify over all types (h_even : ∀ (H : Type) [Group H] {φ : H →* G} (_ : Function.Injective φ), IsZero (groupCohom...
Source project: Class Field Theory
Person-level attribution pending.
Project index
Showing 8 of 14 additional declarations. Use project search for the complete index.
groupCohomology.trivialCohomology_of_even_of_odd_of_solvable
Plain-language statement
If H²ⁿ⁺²(H,M) and H²ᵐ⁺¹(H,M) are both zero for every subgroup H of G then M is acyclic.
Source project: Class Field Theory
Person-level attribution pending.
IsNonarchimedeanLocalField.exists_pow_smul_integer_mem_span
Plain-language statement
Bounded denominators: if b is any finite K-basis of L and ϖ is a uniformiser of K, then a large enough power of ϖ multiplies every integer of L into the 𝒪[K]-lattice spanned by b. This is the key analytic input both for Module.Finite 𝒪[K] 𝒪[L] (see below) and, applied to a normal basis, for the construction of an open cohomologi...
Source project: Class Field Theory
Person-level attribution pending.
IsNonarchimedeanLocalField.exists_pow_smul_mem_integer
Plain-language statement
Every element of L is carried into the integers 𝒪[L] by a large enough power of a uniformiser of K.
Source project: Class Field Theory
Person-level attribution pending.
IsNonarchimedeanLocalField.le_maximalUnramified_iff
Plain-language statement
The maximal unramified subextension is maximal.
Source project: Class Field Theory
Person-level attribution pending.
IsNonarchimedeanLocalField.nonempty_unramifiedExtension_algEquiv_of_isUnramified
Plain-language statement
If L/K is unramified, then L is isomorphic to Kn where n = [L:K].
Source project: Class Field Theory
Person-level attribution pending.
IsNonarchimedeanLocalField.nonempty_unramifiedExtension_alghom_of_dvd_f
Plain-language statement
If Kn denotes the unramified extension of K of degree n, then Kn embeds into L if n ∣ f K L. This is half of the universal property.
Source project: Class Field Theory
Person-level attribution pending.
Padic.mulValuation_lt_iff_norm_lt
Plain-language statement
Strict comparison of Padic.mulValuation matches strict comparison of the norm.
Source project: Class Field Theory
Person-level attribution pending.
Rep.herbrandQuotient_isNonarchimedeanLocalField_units
Plain-language statement
herbrand quotient of Lˣ is [L:K]
Source project: Class Field Theory
Person-level attribution pending.