ModuleArithmeticStageH2RadicalEmbedding.lean
Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.RelationRank.ArithmeticStageH2RadicalEmbedding
2 declarations indexed from sourceView source ↗ Module documentation
Embedding actual finite-stage inflation ranges in the radical dual
The radical functional detects zero after inflation. A linear section of the map onto the inflation range therefore gives an injective map from that range to the radical dual. This uses only the proved kernel inclusion; no compatibility of sections at different finite stages is required.
Declarations
ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2RadicalEmbeddingCanonicalZModAddCommGroup
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.Martinet ProCGroups ProCGroups.ProC
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2InflationRange_exists_radicalDual_embedding
DocumentationEvery actual finite-stage inflation range embeds in the fixed arithmetic dual.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.Martinet ProCGroups ProCGroups.ProC
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
local instance arithmeticStageH2RadicalEmbeddingCanonicalZModAddCommGroup :
AddCommGroup (ZMod (n : ℕ)) :=
(ZMod.instField (n : ℕ)).toDivisionRing.toAddCommGroup
include hpOdd