Module

FiberActionComparison.lean

Nyll.AnabelianGeometry.GeometricFundamentalGroup.FiberActionComparison

4 declarations indexed from sourceView source ↗

Module documentation

Root fields detected by equivalent fibre actions

Equivariant identifications of actual Kummer fibres preserve their root fields. Simultaneous pointwise stabilizers detect the compositum of two root fields; their common-twist family detects the root field of the ratio.

Imports2

Imported by2

theorem

iInf_stabilizer_eq_of_equivariant_equiv

L27 ↗

AnabelianGeometry.GeometricFundamentalGroup.iInf_stabilizer_eq_of_equivariant_equiv

Documentation

Equivariant bijections preserve the pointwise stabilizer of an entire action.

Source context 4 commands

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

noncomputable section
namespace AnabelianGeometry.GeometricFundamentalGroup
open AnabelianGeometry.KummerTheory
universe u v w

Lean source · statement

theorem iInf_stabilizer_eq_of_equivariant_equiv
    {G : Type u} [Group G] {X : Type v} {Y : Type w}
    [MulAction G X] [MulAction G Y] (e : X ≃ Y)
    (he : ∀ (g : G) (x : X), e (g • x) = g • e x) :
    (⨅ x : X, MulAction.stabilizer G x) = ⨅ y : Y, MulAction.stabilizer G y

theorem

rootField_eq_of_equivariant_fiber_equiv

L45 ↗

AnabelianGeometry.GeometricFundamentalGroup.rootField_eq_of_equivariant_fiber_equiv

Documentation

Equivariantly equivalent actual Kummer fibres have the same full root field.

Source context 5 commands

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

noncomputable section
namespace AnabelianGeometry.GeometricFundamentalGroup
open AnabelianGeometry.KummerTheory
universe u v w
variable {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]

Lean source · statement

theorem rootField_eq_of_equivariant_fiber_equiv [IsGalois K L]
    (n : ℕ) (a b : Kˣ)
    (e : LaurentKummerFiberHom (L := L) n a ≃ LaurentKummerFiberHom (L := L) n b)
    (he : ∀ (σ : L ≃ₐ[K] L) (f : LaurentKummerFiberHom (L := L) n a),
      e (σ • f) = σ • e f) :
    rootField (L := L) n (a : K) = rootField (L := L) n (b : K)

theorem

fixedField_two_fiber_stabilizers

L56 ↗

AnabelianGeometry.GeometricFundamentalGroup.fixedField_two_fiber_stabilizers

Documentation

Simultaneous pointwise fixing of two fibres detects their compositum.

Source context 5 commands

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

noncomputable section
namespace AnabelianGeometry.GeometricFundamentalGroup
open AnabelianGeometry.KummerTheory
universe u v w
variable {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]

Lean source · statement

theorem fixedField_two_fiber_stabilizers [IsGalois K L] (n : ℕ) (a b : Kˣ) :
    IntermediateField.fixedField
      ((⨅ f : LaurentKummerFiberHom (L := L) n a,
        MulAction.stabilizer (L ≃ₐ[K] L) f) ⊓
       (⨅ f : LaurentKummerFiberHom (L := L) n b,
        MulAction.stabilizer (L ≃ₐ[K] L) f)) =
      rootField (L := L) n (a : K) ⊔ rootField (L := L) n (b : K)

theorem

rootField_ratio_eq_of_twisted_stabilizers

L68 ↗

AnabelianGeometry.GeometricFundamentalGroup.rootField_ratio_eq_of_twisted_stabilizers

Documentation

Equality of the simultaneous fibre stabilizers for all common twists forces equality of the full root fields of the two ratios.

Source context 5 commands

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

noncomputable section
namespace AnabelianGeometry.GeometricFundamentalGroup
open AnabelianGeometry.KummerTheory
universe u v w
variable {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]

Lean source · statement

theorem rootField_ratio_eq_of_twisted_stabilizers [IsGalois K L] [IsAlgClosed L]
    (n : ℕ) (hn : 0 < n) (x y x' y' : Kˣ)
    (h : ∀ c : Kˣ,
      ((⨅ f : LaurentKummerFiberHom (L := L) n (c * x),
        MulAction.stabilizer (L ≃ₐ[K] L) f) ⊓
       (⨅ f : LaurentKummerFiberHom (L := L) n (c * y),
        MulAction.stabilizer (L ≃ₐ[K] L) f)) =
      ((⨅ f : LaurentKummerFiberHom (L := L) n (c * x'),
        MulAction.stabilizer (L ≃ₐ[K] L) f) ⊓
       (⨅ f : LaurentKummerFiberHom (L := L) n (c * y'),
        MulAction.stabilizer (L ≃ₐ[K] L) f))) :
    rootField (L := L) n ((y / x : Kˣ) : K) =
      rootField (L := L) n ((y' / x' : Kˣ) : K)

Module documentation

Root fields detected by equivalent fibre actions

Declarations

iInf_stabilizer_eq_of_equivariant_equiv

rootField_eq_of_equivariant_fiber_equiv

fixedField_two_fiber_stabilizers

rootField_ratio_eq_of_twisted_stabilizers