Module

CompositumRestriction.lean

Nyll.ValuedFieldTheory.Ramification.GaloisValuation.CompositumRestriction

3 declarations indexed from sourceView source ↗

Module documentation

Restriction from a compositum

An automorphism of a field generated by two normal intermediate fields is determined by its restrictions to those fields.

Imports2

Mathlib.FieldTheory.Galois.Basic
Nyll.ValuedFieldTheory.Ramification.GaloisValuation.IntermediateFieldRestriction

Imported by5

theorem

restrictNormalHom_prod_injective_of_sup_eq_top

L30 ↗

LocalClassFieldTheory.restrictNormalHom_prod_injective_of_sup_eq_top

Documentation

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

Source context 6 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalClassFieldTheory
open RamificationTheory
universe u v
variable (K : Type u) {P : Type v} [Field K] [Field P] [Algebra K P]

Lean source · statement

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

theorem

intermediateFieldRestrictNormalHom_prod_injective_of_sup_eq

L59 ↗

LocalClassFieldTheory.intermediateFieldRestrictNormalHom_prod_injective_of_sup_eq

Documentation

If two normal intermediate fields generate a third intermediate field in a common ambient extension, restriction from the generated field to the two factors is jointly injective.

Source context 7 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalClassFieldTheory
open RamificationTheory
universe u v
variable (K : Type u) {P : Type v} [Field K] [Field P] [Algebra K P]
universe w

Lean source · statement

theorem intermediateFieldRestrictNormalHom_prod_injective_of_sup_eq
    {Omega : Type w} [Field Omega] [Algebra K Omega]
    (E₁ E₂ F : IntermediateField K Omega)
    (hE₁ : E₁ ≤ F) (hE₂ : E₂ ≤ F)
    [Normal K E₁] [Normal K E₂]
    (hsup : E₁ ⊔ E₂ = F) :
    Function.Injective
      ((intermediateFieldRestrictNormalHom E₁ F hE₁ :
          (F ≃ₐ[K] F) →* (E₁ ≃ₐ[K] E₁)).prod
        (intermediateFieldRestrictNormalHom E₂ F hE₂ :
          (F ≃ₐ[K] F) →* (E₂ ≃ₐ[K] E₂)))

theorem

subgroup_eq_of_prod_map_injective_of_left_maps_eq_bot

L151 ↗

LocalClassFieldTheory.subgroup_eq_of_prod_map_injective_of_left_maps_eq_bot

Documentation

Two subgroups are equal when one jointly injective pair of homomorphisms has equal right images and both left images are trivial.

Source context 7 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalClassFieldTheory
open RamificationTheory
universe u v
variable (K : Type u) {P : Type v} [Field K] [Field P] [Algebra K P]
universe w

Lean source · statement

theorem subgroup_eq_of_prod_map_injective_of_left_maps_eq_bot
    {G G₁ G₂ : Type*} [Group G] [Group G₁] [Group G₂]
    (f₁ : G →* G₁) (f₂ : G →* G₂)
    (hinjective : Function.Injective (f₁.prod f₂))
    (A B : Subgroup G)
    (hA₁ : A.map f₁ = ⊥) (hB₁ : B.map f₁ = ⊥)
    (h₂ : A.map f₂ = B.map f₂) :
    A = B

Module documentation

Restriction from a compositum

Declarations

restrictNormalHom_prod_injective_of_sup_eq_top

intermediateFieldRestrictNormalHom_prod_injective_of_sup_eq

subgroup_eq_of_prod_map_injective_of_left_maps_eq_bot