Module

FieldCompositum.lean

Nyll.SchemeTheory.AbhyankarLemma.Geometry.Inertia.FieldCompositum

2 declarations indexed from sourceView source ↗

Module documentation

Inertia on a compositum

An automorphism of a field generated by two intermediate fields is determined by its restrictions to the two fields. This gives the injective map from the inertia group of a compositum to the product of the two lower inertia groups used in SGA 1, Expose X, Lemma 3.6.

Imports2

Imported by3

theorem

restrictNormalHom_prod_injective_of_sup_eq_top

L31 ↗

TameAbhyankar.SGA1.restrictNormalHom_prod_injective_of_sup_eq_top

Documentation

Restriction of field automorphisms to two normal intermediate fields is jointly injective when those fields generate the ambient field.

Source context 5 commands

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

noncomputable section
universe u v
namespace TameAbhyankar.SGA1
open RamificationTheory.HilbertRamification.ValuationSubring
variable (K : Type u) {E : Type v} [Field K] [Field E] [Algebra K E]

Lean source · statement

theorem restrictNormalHom_prod_injective_of_sup_eq_top
    (M N : IntermediateField K E) [Normal K M] [Normal K N]
    (hsup : M ⊔ N = ⊤) :
    Function.Injective
      ((AlgEquiv.restrictNormalHom (F := K) (K₁ := E) M).prod
        (AlgEquiv.restrictNormalHom (F := K) (K₁ := E) N))

theorem

inertiaRestriction_prod_injective_of_sup_eq_top

L43 ↗

TameAbhyankar.SGA1.inertiaRestriction_prod_injective_of_sup_eq_top