Class number one makes the actual unit-to-radical map surjective. The integral units of the rationals are ±1, so these two representatives exhaust the ideal-square radical. This identifies its unique possible obstruction coordinate without assuming a dimension bound or a comparison.
Surrounding namespaces, section variables, and local commands at this declaration.
open NumberField IsDedekindDomain
open scoped NumberField
namespace ClassFieldTower.Sawin
open ClassFieldTower.Martinet.Shafarevichtheorem rationalRingUnit_eq_one_or_neg_one (u : (𝓞 ℚ)ˣ) :
u = 1 ∨ u = -1Surrounding namespaces, section variables, and local commands at this declaration.
open NumberField IsDedekindDomain
open scoped NumberField
namespace ClassFieldTower.Sawin
open ClassFieldTower.Martinet.Shafarevichtheorem rationalIntegralUnitToIdealSquareRadical_surjective :
Function.Surjective (integralUnitToIdealNthPowerRadicalQuotient ℚ (2 : ℕ+))Every element of the rational ideal-square radical is zero or the actual class of the integral unit −1.
Surrounding namespaces, section variables, and local commands at this declaration.
open NumberField IsDedekindDomain
open scoped NumberField
namespace ClassFieldTower.Sawin
open ClassFieldTower.Martinet.Shafarevichtheorem rationalIdealSquareRadical_eq_zero_or_neg_one
(x : idealPowerRadicalModP ℚ 2) :
x = 0 ∨ x = Additive.ofMul
(integralUnitToIdealNthPowerRadicalQuotient ℚ (2 : ℕ+) (-1))