ModuleContinuousRootCocycleLifting.lean
Nyll.GaloisCohomology.Kummer.Concrete.ContinuousRootCocycleLifting
3 declarations indexed from sourceView source ↗ Module documentation
Lifting continuous cocycles through power maps
Over a separably closed Galois extension, Hilbert 90 writes a continuous multiplicative cocycle as a coboundary. Taking a root of that actual coboundary parameter lifts the cocycle, preserving local constancy and the root-of-unity coefficient bound.
Declarations
KummerTheory.isLocallyConstant_rootQuotient
DocumentationA root quotient is locally constant in the Krull topology.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace KummerTheory
open groupCohomology
universe u v
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
[IsGalois K Ω]
KummerTheory.exists_mulCocycle_root_of_isLocallyConstant
DocumentationEvery continuous multiplicative cocycle has a continuous root of an exponent invertible in the separably closed coefficient field.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace KummerTheory
open groupCohomology
universe u v
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
[IsGalois K Ω]
variable [IsSepClosed Ω]
KummerTheory.exists_mulCocycle_rootsOfUnity_lift
DocumentationA cocycle in n-th roots lifts to a cocycle in (n*m)-th roots, compatibly with the m-th-power reduction.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace KummerTheory
open groupCohomology
universe u v
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
[IsGalois K Ω]
variable [IsSepClosed Ω]