Module

ClosedFixingSubgroup.lean

Nyll.ValuedFieldTheory.Ramification.GaloisValuation.ClosedFixingSubgroup

1 declaration indexed from sourceView source ↗

Module documentation

This module packages the closed subgroup attached to an intermediate field in the Krull topology.

Imports2

Imported by7

def

RamificationTheory.closedFixingSubgroup

Documentation

The closed fixing subgroup attached to an intermediate field.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace RamificationTheory

Lean source · statement

def closedFixingSubgroup
    (k Ω : Type*) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
    (K : IntermediateField k Ω) : ClosedSubgroup Gal(Ω/k)