Module

IntermediateFieldRestriction.lean

Nyll.ValuedFieldTheory.Ramification.GaloisValuation.IntermediateFieldRestriction

2 declarations indexed from sourceView source ↗

Module documentation

Restriction between normal intermediate fields

This module packages the canonical restriction map between two intermediate fields in a common ambient extension without requiring callers to install the auxiliary algebra and scalar-tower instances.

Imports1

Mathlib.FieldTheory.Galois.Basic

Imported by8

def

intermediateFieldRestrictNormalHom

L30 ↗

RamificationTheory.intermediateFieldRestrictNormalHom

Documentation

Restriction Gal(F/K) → Gal(E/K) for two intermediate fields E ≤ F in one ambient extension.

Source context 4 commands

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

noncomputable section
namespace RamificationTheory
universe u v
variable {K : Type u} {Omega : Type v}
  [Field K] [Field Omega] [Algebra K Omega]

Lean source · statement

def intermediateFieldRestrictNormalHom
    (E F : IntermediateField K Omega) (hEF : E ≤ F) [Normal K E] :
    (F ≃ₐ[K] F) →* (E ≃ₐ[K] E)

theorem

intermediateFieldRestrictNormalHom_apply_val

L40 ↗

RamificationTheory.intermediateFieldRestrictNormalHom_apply_val