Module

GaloisIntegerRing.lean

Nyll.ValuedFieldTheory.LocalField.NonarchimedeanLocalField.GaloisIntegerRing

38 declarations indexed from sourceView source ↗

Module documentation

Galois actions on valuation rings

Restricts Galois automorphisms to valuation rings and transports their action to ideals, ideal-power quotients, principal units, and successive quotients.

Imports5

Imported by7

theorem

galoisGroup_mem_integerRing_of_isIntegralClosure

L34 ↗

LocalFieldTheory.galoisGroup_mem_integerRing_of_isIntegralClosure

Documentation

A real Galois automorphism preserves the valuation integer ring when that ring is the integral closure of the base valuation integer ring.

This is the source-producing replacement for proving integer-ring preservation from a valuation-invariance certificate: integrality is transported by the K-algebra automorphism, and integral-closure membership brings the element back to 𝒪[L].

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem galoisGroup_mem_integerRing_of_isIntegralClosure
    (K L : Type u) [Field K] [ValuativeRel K] [Field L] [ValuativeRel L]
    [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    (σ : Gal(L/K)) (x : 𝒪[L]) :
    σ (x : L) ∈ 𝒪[L]

def

galoisGroupIntegerRingEquivOfIsIntegralClosure

L52 ↗

LocalFieldTheory.galoisGroupIntegerRingEquivOfIsIntegralClosure

Documentation

Restrict a real Galois automorphism to the valuation integer ring using the actual integral-closure property of valuation integer rings.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · full declaration

def galoisGroupIntegerRingEquivOfIsIntegralClosure
    (K L : Type u) [Field K] [ValuativeRel K] [Field L] [ValuativeRel L]
    [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L] (σ : Gal(L/K)) :
    𝒪[L] ≃+* 𝒪[L] where
  toFun x :=
    ⟨σ (x : L), galoisGroup_mem_integerRing_of_isIntegralClosure K L σ x⟩
  invFun x :=
    ⟨σ.symm (x : L), galoisGroup_mem_integerRing_of_isIntegralClosure K L σ.symm x⟩
  left_inv := by
    intro x
    ext
    simp
  right_inv := by
    intro x
    ext
    simp
  map_mul' := by
    intro x y
    ext
    simp
  map_add' := by
    intro x y
    ext
    simp

theorem

galoisGroupIntegerRingEquivOfIsIntegralClosure_apply

L82 ↗

LocalFieldTheory.galoisGroupIntegerRingEquivOfIsIntegralClosure_apply

Documentation

Restriction sends a field automorphism to the corresponding automorphism of the integral-closure valuation ring.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem galoisGroupIntegerRingEquivOfIsIntegralClosure_apply
    (K L : Type u) [Field K] [ValuativeRel K] [Field L] [ValuativeRel L]
    [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    (σ : Gal(L/K)) (x : 𝒪[L]) :
    ((galoisGroupIntegerRingEquivOfIsIntegralClosure K L σ x : 𝒪[L]) : L) =
      σ (x : L)

theorem

galoisGroupIntegerRingEquivOfIsIntegralClosure_symm_apply

L95 ↗

LocalFieldTheory.galoisGroupIntegerRingEquivOfIsIntegralClosure_symm_apply

Documentation

The inverse restriction equivalence extends an integer-ring automorphism to the ambient field.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem galoisGroupIntegerRingEquivOfIsIntegralClosure_symm_apply
    (K L : Type u) [Field K] [ValuativeRel K] [Field L] [ValuativeRel L]
    [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    (σ : Gal(L/K)) (x : 𝒪[L]) :
    (((galoisGroupIntegerRingEquivOfIsIntegralClosure K L σ).symm x : 𝒪[L]) : L) =
      σ.symm (x : L)

def

galoisGroupIntegerRingEquivHomOfIsIntegralClosure

L107 ↗

LocalFieldTheory.galoisGroupIntegerRingEquivHomOfIsIntegralClosure

Documentation

Real Galois automorphisms act on 𝒪[L] through the actual integral-closure restriction.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · full declaration

def galoisGroupIntegerRingEquivHomOfIsIntegralClosure
    (K L : Type u) [Field K] [ValuativeRel K] [Field L] [ValuativeRel L]
    [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L] :
    Gal(L / K) →* (𝒪[L] ≃+* 𝒪[L]) where
  toFun := galoisGroupIntegerRingEquivOfIsIntegralClosure K L
  map_one' := by
    ext x
    rfl
  map_mul' := by
    intro σ τ
    ext x
    rfl

def

galoisGroupIntegerRingMulSemiringActionOfIsIntegralClosure

L125 ↗

LocalFieldTheory.galoisGroupIntegerRingMulSemiringActionOfIsIntegralClosure

Documentation

The semiring action on the valuation integer ring induced by the actual integral-closure restriction of Gal(L / K).

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

def galoisGroupIntegerRingMulSemiringActionOfIsIntegralClosure
    (K L : Type u) [Field K] [ValuativeRel K] [Field L] [ValuativeRel L]
    [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L] :
    MulSemiringAction (Gal(L / K)) 𝒪[L]

theorem

galoisGroupIntegerRingEquivOfIsIntegralClosure_integerRingMap

L135 ↗

LocalFieldTheory.galoisGroupIntegerRingEquivOfIsIntegralClosure_integerRingMap

Documentation

Restriction of a Galois automorphism commutes with the inclusion of the integer ring into the field.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem galoisGroupIntegerRingEquivOfIsIntegralClosure_integerRingMap
    (K L : Type u) [Field K] [ValuativeRel K] [Field L] [ValuativeRel L]
    [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    (σ : Gal(L/K)) (x : 𝒪[K]) :
    galoisGroupIntegerRingEquivOfIsIntegralClosure K L σ
        (integerRingMapOfValuationExtension K L x) =
      integerRingMapOfValuationExtension K L x

theorem

galoisGroupIntegerRingMulSemiringActionOfIsIntegralClosure_integerRingMap

L149 ↗

LocalFieldTheory.galoisGroupIntegerRingMulSemiringActionOfIsIntegralClosure_integerRingMap

Documentation

The actual Gal(L / K) action on 𝒪[L] fixes the image of 𝒪[K].

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · full declaration

theorem galoisGroupIntegerRingMulSemiringActionOfIsIntegralClosure_integerRingMap
    (K L : Type u) [Field K] [ValuativeRel K] [Field L] [ValuativeRel L]
    [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    (σ : Gal(L/K)) (x : 𝒪[K]) :
    letI := galoisGroupIntegerRingMulSemiringActionOfIsIntegralClosure K L
    σ • integerRingMapOfValuationExtension K L x =
      integerRingMapOfValuationExtension K L x := by
  change galoisGroupIntegerRingEquivOfIsIntegralClosure K L σ
      (integerRingMapOfValuationExtension K L x) =
    integerRingMapOfValuationExtension K L x
  exact galoisGroupIntegerRingEquivOfIsIntegralClosure_integerRingMap K L σ x

theorem

galoisGroupIntegerRingSMulCommClassOfIsIntegralClosure

L165 ↗

LocalFieldTheory.galoisGroupIntegerRingSMulCommClassOfIsIntegralClosure

Documentation

The actual integral-closure action commutes with the canonical 𝒪[K]-scalar action on 𝒪[L].

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · full declaration

theorem galoisGroupIntegerRingSMulCommClassOfIsIntegralClosure
    (K L : Type u) [Field K] [ValuativeRel K] [Field L] [ValuativeRel L]
    [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L] :
    letI := galoisGroupIntegerRingMulSemiringActionOfIsIntegralClosure K L
    SMulCommClass (Gal(L / K)) 𝒪[K] 𝒪[L] := by
  let := galoisGroupIntegerRingMulSemiringActionOfIsIntegralClosure K L
  refine ⟨?_⟩
  intro σ x y
  rw [Algebra.smul_def, Algebra.smul_def]
  change galoisGroupIntegerRingEquivOfIsIntegralClosure K L σ
      (algebraMap 𝒪[K] 𝒪[L] x * y) =
    algebraMap 𝒪[K] 𝒪[L] x *
      galoisGroupIntegerRingEquivOfIsIntegralClosure K L σ y
  rw [map_mul]
  have hx : galoisGroupIntegerRingEquivOfIsIntegralClosure K L σ
      (algebraMap 𝒪[K] 𝒪[L] x) = algebraMap 𝒪[K] 𝒪[L] x := by
    simpa [integerRingMapOfValuationExtension] using
      galoisGroupIntegerRingEquivOfIsIntegralClosure_integerRingMap K L σ x
  rw [hx]

theorem

galoisGroupIntegerRingFieldSMulDistribClassOfIsIntegralClosure

L189 ↗

LocalFieldTheory.galoisGroupIntegerRingFieldSMulDistribClassOfIsIntegralClosure

Documentation

The actual integral-closure action is compatible with the field-level Gal(L / K) action after coercion to L.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · full declaration

theorem galoisGroupIntegerRingFieldSMulDistribClassOfIsIntegralClosure
    (K L : Type u) [Field K] [ValuativeRel K] [Field L] [ValuativeRel L]
    [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L] :
    letI := galoisGroupIntegerRingMulSemiringActionOfIsIntegralClosure K L
    SMulDistribClass (Gal(L / K)) 𝒪[L] L := by
  let := galoisGroupIntegerRingMulSemiringActionOfIsIntegralClosure K L
  refine ⟨?_⟩
  intro σ r s
  change σ (((r : 𝒪[L]) : L) * s) =
    ((galoisGroupIntegerRingEquivOfIsIntegralClosure K L σ r : 𝒪[L]) : L) * σ s
  rw [map_mul]
  rw [galoisGroupIntegerRingEquivOfIsIntegralClosure_apply]

theorem

galoisGroupIntegerRing_isGaloisGroup_of_isIntegralClosure

L207 ↗

LocalFieldTheory.galoisGroupIntegerRing_isGaloisGroup_of_isIntegralClosure

Documentation

The actual integral-closure action on valuation integer rings is a mathlib Galois group. This is the source-producing version of the ring-level Galois input needed for inertia/cardinality arguments.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · full declaration

theorem galoisGroupIntegerRing_isGaloisGroup_of_isIntegralClosure
    (K L : Type u) [Field K] [ValuativeRel K] [Field L] [ValuativeRel L]
    [Algebra K L] [IsGalois K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L] :
    letI := galoisGroupIntegerRingMulSemiringActionOfIsIntegralClosure K L
    IsGaloisGroup (Gal(L / K)) 𝒪[K] 𝒪[L] := by
  let := galoisGroupIntegerRingMulSemiringActionOfIsIntegralClosure K L
  let := galoisGroupIntegerRingFieldSMulDistribClassOfIsIntegralClosure K L
  let : Algebra.IsIntegral 𝒪[K] 𝒪[L] :=
    IsIntegralClosure.isIntegral_algebra 𝒪[K] L
  exact IsGaloisGroup.of_isFractionRing (Gal(L / K)) 𝒪[K] 𝒪[L] K L

def

galoisGroupIntegerRingIdealDistribMulActionOfIsIntegralClosure

L222 ↗

LocalFieldTheory.galoisGroupIntegerRingIdealDistribMulActionOfIsIntegralClosure

Documentation

The ideal action induced by the actual integral-closure restriction.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

def galoisGroupIntegerRingIdealDistribMulActionOfIsIntegralClosure
    (K L : Type u) [Field K] [ValuativeRel K] [Field L] [ValuativeRel L]
    [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L] :
    DistribMulAction (Gal(L / K)) (Ideal 𝒪[L])

def

galoisGroupIntegerRingIdealMulActionOfIsIntegralClosure

L234 ↗

LocalFieldTheory.galoisGroupIntegerRingIdealMulActionOfIsIntegralClosure

Documentation

The multiplicative ideal action induced by the actual integral-closure restriction.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

def galoisGroupIntegerRingIdealMulActionOfIsIntegralClosure
    (K L : Type u) [Field K] [ValuativeRel K] [Field L] [ValuativeRel L]
    [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L] :
    MulAction (Gal(L / K)) (Ideal 𝒪[L])

theorem

galoisGroupIntegerRingAction_map_maximalIdeal_of_isIntegralClosure

L243 ↗

LocalFieldTheory.galoisGroupIntegerRingAction_map_maximalIdeal_of_isIntegralClosure

Documentation

The Galois action on an integral-closure valuation ring preserves its maximal ideal.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem galoisGroupIntegerRingAction_map_maximalIdeal_of_isIntegralClosure
    (K L : Type u) [Field K] [ValuativeRel K] [Field L] [ValuativeRel L]
    [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    (σ : Gal(L/K)) :
    Ideal.map (@MulSemiringAction.toRingHom (Gal(L / K)) _ 𝒪[L] _
        (galoisGroupIntegerRingMulSemiringActionOfIsIntegralClosure K L) σ)
      (𝓂[L] : Ideal 𝒪[L]) =
      (𝓂[L] : Ideal 𝒪[L])

theorem

galoisGroupIntegerRingAction_mem_maximalIdeal_stabilizer_of_isIntegralClosure

L262 ↗

LocalFieldTheory.galoisGroupIntegerRingAction_mem_maximalIdeal_stabilizer_of_isIntegralClosure

Documentation

Every Galois automorphism belongs to the stabilizer of the maximal ideal of the integral-closure valuation ring.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem galoisGroupIntegerRingAction_mem_maximalIdeal_stabilizer_of_isIntegralClosure
    (K L : Type u) [Field K] [ValuativeRel K] [Field L] [ValuativeRel L]
    [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    (σ : Gal(L/K)) :
    σ ∈ @MulAction.stabilizer (Gal(L / K)) (Ideal 𝒪[L]) _
      (galoisGroupIntegerRingIdealMulActionOfIsIntegralClosure K L)
      (𝓂[L] : Ideal 𝒪[L])

def

galoisGroupMaximalIdealStabilizerHomOfIsIntegralClosure

L281 ↗

LocalFieldTheory.galoisGroupMaximalIdealStabilizerHomOfIsIntegralClosure

Documentation

Real Galois automorphisms, viewed inside the maximal-ideal stabilizer, using the actual integral-closure restriction.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · full declaration

def galoisGroupMaximalIdealStabilizerHomOfIsIntegralClosure
    (K L : Type u) [Field K] [ValuativeRel K] [Field L] [ValuativeRel L]
    [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L] :
    Gal(L / K) →* @MulAction.stabilizer (Gal(L / K)) (Ideal 𝒪[L]) _
      (galoisGroupIntegerRingIdealMulActionOfIsIntegralClosure K L)
      (𝓂[L] : Ideal 𝒪[L]) where
  toFun σ :=
    ⟨σ, galoisGroupIntegerRingAction_mem_maximalIdeal_stabilizer_of_isIntegralClosure K L σ⟩
  map_one' := by
    ext
    rfl
  map_mul' σ τ := by
    ext
    rfl

def

galoisGroupPrincipalUnitsMapEquivOfIsIntegralClosure

L300 ↗

LocalFieldTheory.galoisGroupPrincipalUnitsMapEquivOfIsIntegralClosure

Documentation

Actual integral-closure real Galois action on the n-th principal-unit group.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

def galoisGroupPrincipalUnitsMapEquivOfIsIntegralClosure
    (K L : Type u) [Field K] [ValuativeRel K] [Field L] [ValuativeRel L]
    [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    (n : Nat) (σ : Gal(L/K)) :
    principalUnits L n ≃* principalUnits L n

theorem

galoisGroupPrincipalUnitsMapEquivOfIsIntegralClosure_apply

L312 ↗

LocalFieldTheory.galoisGroupPrincipalUnitsMapEquivOfIsIntegralClosure_apply

Documentation

The induced equivalence on principal units applies the restricted Galois automorphism to the underlying unit.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem galoisGroupPrincipalUnitsMapEquivOfIsIntegralClosure_apply
    (K L : Type u) [Field K] [ValuativeRel K] [Field L] [ValuativeRel L]
    [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    (n : Nat) (σ : Gal(L/K)) (u : principalUnits L n) :
    ((galoisGroupPrincipalUnitsMapEquivOfIsIntegralClosure K L n σ u :
        principalUnits L n) : 𝒪[L]ˣ) =
      Units.mapEquiv
        (galoisGroupIntegerRingEquivOfIsIntegralClosure K L σ).toMulEquiv u.1

def

galoisGroupPrincipalUnitsMapEquivHomOfIsIntegralClosure

L326 ↗

LocalFieldTheory.galoisGroupPrincipalUnitsMapEquivHomOfIsIntegralClosure

Documentation

Integral-closure Galois action on principal units as a group homomorphism.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · full declaration

def galoisGroupPrincipalUnitsMapEquivHomOfIsIntegralClosure
    (K L : Type u) [Field K] [ValuativeRel K] [Field L] [ValuativeRel L]
    [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    (n : Nat) :
    Gal(L / K) →* (principalUnits L n ≃* principalUnits L n) where
  toFun := galoisGroupPrincipalUnitsMapEquivOfIsIntegralClosure K L n
  map_one' := by
    ext u
    rfl
  map_mul' := by
    intro σ τ
    ext u
    rfl

def

galoisGroupMaximalIdealPowSuccQuotMapEquivOfIsIntegralClosure

L343 ↗

LocalFieldTheory.galoisGroupMaximalIdealPowSuccQuotMapEquivOfIsIntegralClosure

Documentation

Integral-closure Galois action on 𝓂_L^n/𝓂_L^(n+1).

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

def galoisGroupMaximalIdealPowSuccQuotMapEquivOfIsIntegralClosure
    (K L : Type u) [Field K] [ValuativeRel K] [Field L] [ValuativeRel L]
    [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    (n : Nat) (σ : Gal(L/K)) :
    MaximalIdealPowSuccQuot L n ≃+ MaximalIdealPowSuccQuot L n

theorem

galoisGroupMaximalIdealPowSuccQuotMapEquivOfIsIntegralClosure_mk

L355 ↗

LocalFieldTheory.galoisGroupMaximalIdealPowSuccQuotMapEquivOfIsIntegralClosure_mk

Documentation

The Galois equivalence on a successive maximal-ideal quotient maps the class of a representative to the class of its conjugate.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem galoisGroupMaximalIdealPowSuccQuotMapEquivOfIsIntegralClosure_mk
    (K L : Type u) [Field K] [ValuativeRel K] [Field L] [ValuativeRel L]
    [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    (n : Nat) (σ : Gal(L/K))
    (a : ((𝓂[L] ^ n : Ideal 𝒪[L]) : Type u)) :
    galoisGroupMaximalIdealPowSuccQuotMapEquivOfIsIntegralClosure K L n σ
        (maximalIdealPowSuccQuotMk L n a) =
      maximalIdealPowSuccQuotMk L n
        (maximalIdealPowMapEquivOfIntegerRingEquiv L n
          (galoisGroupIntegerRingEquivOfIsIntegralClosure K L σ) a)

def

galoisGroupMaximalIdealPowSuccQuotMapEquivHomOfIsIntegralClosure

L371 ↗

LocalFieldTheory.galoisGroupMaximalIdealPowSuccQuotMapEquivHomOfIsIntegralClosure

Documentation

Integral-closure Galois action on maximal-ideal graded pieces.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · full declaration

def galoisGroupMaximalIdealPowSuccQuotMapEquivHomOfIsIntegralClosure
    (K L : Type u) [Field K] [ValuativeRel K] [Field L] [ValuativeRel L]
    [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    (n : Nat) :
    Gal(L / K) →*
      Multiplicative
        (AddAut (MaximalIdealPowSuccQuot L n)) where
  toFun σ := Multiplicative.ofAdd
    (galoisGroupMaximalIdealPowSuccQuotMapEquivOfIsIntegralClosure K L n σ)
  map_one' := by
    ext x
    refine MaximalIdealPowSuccQuot.inductionOn n
      (motive := fun x =>
        galoisGroupMaximalIdealPowSuccQuotMapEquivOfIsIntegralClosure
            K L n 1 x = x)
      x ?_
    intro a
    rw [galoisGroupMaximalIdealPowSuccQuotMapEquivOfIsIntegralClosure_mk]
    rfl
  map_mul' := by
    intro σ τ
    ext x
    refine MaximalIdealPowSuccQuot.inductionOn n
      (motive := fun x =>
        galoisGroupMaximalIdealPowSuccQuotMapEquivOfIsIntegralClosure
            K L n (σ * τ) x =
          galoisGroupMaximalIdealPowSuccQuotMapEquivOfIsIntegralClosure
            K L n σ
            (galoisGroupMaximalIdealPowSuccQuotMapEquivOfIsIntegralClosure
              K L n τ x))
      x ?_
    intro a
    rw [galoisGroupMaximalIdealPowSuccQuotMapEquivOfIsIntegralClosure_mk]
    rw [galoisGroupMaximalIdealPowSuccQuotMapEquivOfIsIntegralClosure_mk,
      galoisGroupMaximalIdealPowSuccQuotMapEquivOfIsIntegralClosure_mk]
    rfl

def

galoisGroupMaximalIdealPowSuccQuotDistribMulActionOfIsIntegralClosure

L413 ↗

LocalFieldTheory.galoisGroupMaximalIdealPowSuccQuotDistribMulActionOfIsIntegralClosure

Documentation

Integral-closure Galois action on maximal-ideal graded pieces, packaged as an additive action.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · full declaration

def galoisGroupMaximalIdealPowSuccQuotDistribMulActionOfIsIntegralClosure
    (K L : Type u) [Field K] [ValuativeRel K] [Field L] [ValuativeRel L]
    [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    (n : Nat) :
    DistribMulAction (Gal(L / K)) (MaximalIdealPowSuccQuot L n) where
  smul σ x := galoisGroupMaximalIdealPowSuccQuotMapEquivOfIsIntegralClosure K L n σ x
  one_smul := by
    intro x
    change galoisGroupMaximalIdealPowSuccQuotMapEquivOfIsIntegralClosure K L n 1 x = x
    have h := congrArg (fun e :
        Multiplicative (AddAut (MaximalIdealPowSuccQuot L n)) =>
          Multiplicative.toAdd e x)
      (map_one (galoisGroupMaximalIdealPowSuccQuotMapEquivHomOfIsIntegralClosure K L n))
    exact h
  mul_smul := by
    intro σ τ x
    change galoisGroupMaximalIdealPowSuccQuotMapEquivOfIsIntegralClosure K L n (σ * τ) x =
      galoisGroupMaximalIdealPowSuccQuotMapEquivOfIsIntegralClosure K L n σ
        (galoisGroupMaximalIdealPowSuccQuotMapEquivOfIsIntegralClosure K L n τ x)
    have h := congrArg (fun e :
        Multiplicative (AddAut (MaximalIdealPowSuccQuot L n)) =>
          Multiplicative.toAdd e x)
      (map_mul (galoisGroupMaximalIdealPowSuccQuotMapEquivHomOfIsIntegralClosure K L n) σ τ)
    exact h
  smul_zero := by
    intro σ
    exact map_zero (galoisGroupMaximalIdealPowSuccQuotMapEquivOfIsIntegralClosure K L n σ)
  smul_add := by
    intro σ x y
    exact map_add (galoisGroupMaximalIdealPowSuccQuotMapEquivOfIsIntegralClosure K L n σ) x y

theorem

galoisGroupMaximalIdealPowSuccQuotDistribMulActionOfIsIntegralClosure_smul

L448 ↗

LocalFieldTheory.galoisGroupMaximalIdealPowSuccQuotDistribMulActionOfIsIntegralClosure_smul

Documentation

The distributive Galois action on a successive maximal-ideal quotient is computed by conjugating representatives.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · full declaration

theorem galoisGroupMaximalIdealPowSuccQuotDistribMulActionOfIsIntegralClosure_smul
    (K L : Type u) [Field K] [ValuativeRel K] [Field L] [ValuativeRel L]
    [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    (n : Nat) (σ : Gal(L/K)) (x : MaximalIdealPowSuccQuot L n) :
    letI := galoisGroupMaximalIdealPowSuccQuotDistribMulActionOfIsIntegralClosure K L n
    σ • x = galoisGroupMaximalIdealPowSuccQuotMapEquivOfIsIntegralClosure K L n σ x :=
  rfl

def

galoisGroupMaximalIdealPowSuccQuotMultiplicativeMulDistribMulActionOfIsIntegralClosure

L461 ↗

LocalFieldTheory.galoisGroupMaximalIdealPowSuccQuotMultiplicativeMulDistribMulActionOfIsIntegralClosure

Documentation

Actual integral-closure real Galois action on the multiplicative form of maximal-ideal graded pieces.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · full declaration

def galoisGroupMaximalIdealPowSuccQuotMultiplicativeMulDistribMulActionOfIsIntegralClosure
    (K L : Type u) [Field K] [ValuativeRel K] [Field L] [ValuativeRel L]
    [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    (n : Nat) :
    MulDistribMulAction (Gal(L / K)) (Multiplicative (MaximalIdealPowSuccQuot L n)) where
  smul σ x :=
    maximalIdealPowSuccQuotMultiplicativeMapEquivOfIntegerRingEquiv L n
      (galoisGroupIntegerRingEquivOfIsIntegralClosure K L σ) x
  one_smul := by
    intro x
    change maximalIdealPowSuccQuotMultiplicativeMapEquivOfIntegerRingEquiv L n
        (galoisGroupIntegerRingEquivOfIsIntegralClosure K L 1) x = x
    have h := congrArg (fun e :
        Multiplicative (AddAut (MaximalIdealPowSuccQuot L n)) =>
          Multiplicative.toAdd e (Multiplicative.toAdd x))
      (map_one (galoisGroupMaximalIdealPowSuccQuotMapEquivHomOfIsIntegralClosure K L n))
    exact congrArg Multiplicative.ofAdd h
  mul_smul := by
    intro σ τ x
    change maximalIdealPowSuccQuotMultiplicativeMapEquivOfIntegerRingEquiv L n
        (galoisGroupIntegerRingEquivOfIsIntegralClosure K L (σ * τ)) x =
      maximalIdealPowSuccQuotMultiplicativeMapEquivOfIntegerRingEquiv L n
        (galoisGroupIntegerRingEquivOfIsIntegralClosure K L σ)
        (maximalIdealPowSuccQuotMultiplicativeMapEquivOfIntegerRingEquiv L n
          (galoisGroupIntegerRingEquivOfIsIntegralClosure K L τ) x)
    have h := congrArg (fun e :
        Multiplicative (AddAut (MaximalIdealPowSuccQuot L n)) =>
          Multiplicative.toAdd e (Multiplicative.toAdd x))
      (map_mul (galoisGroupMaximalIdealPowSuccQuotMapEquivHomOfIsIntegralClosure K L n) σ τ)
    exact congrArg Multiplicative.ofAdd h
  smul_mul := by
    intro σ x y
    exact map_mul
      (maximalIdealPowSuccQuotMultiplicativeMapEquivOfIntegerRingEquiv L n
        (galoisGroupIntegerRingEquivOfIsIntegralClosure K L σ)) x y
  smul_one := by
    intro σ
    exact map_one
      (maximalIdealPowSuccQuotMultiplicativeMapEquivOfIntegerRingEquiv L n
        (galoisGroupIntegerRingEquivOfIsIntegralClosure K L σ))

theorem

galoisGroupMaximalIdealPowSuccQuotMultiplicativeMulDistribMulActionOfIsIntegralClosure_smul

L506 ↗

LocalFieldTheory.galoisGroupMaximalIdealPowSuccQuotMultiplicativeMulDistribMulActionOfIsIntegralClosure_smul

Documentation

After multiplicative re-encoding, the Galois action on a maximal-ideal quotient is still induced by conjugation.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · full declaration

theorem galoisGroupMaximalIdealPowSuccQuotMultiplicativeMulDistribMulActionOfIsIntegralClosure_smul
    (K L : Type u) [Field K] [ValuativeRel K] [Field L] [ValuativeRel L]
    [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    (n : Nat) (σ : Gal(L/K))
    (x : Multiplicative (MaximalIdealPowSuccQuot L n)) :
    letI := galoisGroupMaximalIdealPowSuccQuotMultiplicativeMulDistribMulActionOfIsIntegralClosure
      K L n
    σ • x = maximalIdealPowSuccQuotMultiplicativeMapEquivOfIntegerRingEquiv L n
      (galoisGroupIntegerRingEquivOfIsIntegralClosure K L σ) x :=
  rfl

def

galoisGroupPrincipalUnitsSuccQuotMapEquivOfIsIntegralClosure

L520 ↗

LocalFieldTheory.galoisGroupPrincipalUnitsSuccQuotMapEquivOfIsIntegralClosure

Documentation

Actual integral-closure action on U^n/U^(n+1).

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

def galoisGroupPrincipalUnitsSuccQuotMapEquivOfIsIntegralClosure
    (K L : Type u) [Field K] [ValuativeRel K] [Field L] [ValuativeRel L]
    [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    (n : Nat) (σ : Gal(L/K)) :
    PrincipalUnitsSuccQuot L n ≃* PrincipalUnitsSuccQuot L n

theorem

galoisGroupPrincipalUnitsSuccQuotMapEquivOfIsIntegralClosure_apply

L532 ↗

LocalFieldTheory.galoisGroupPrincipalUnitsSuccQuotMapEquivOfIsIntegralClosure_apply

Documentation

The Galois equivalence on a successive principal-unit quotient maps each class to the class of its conjugate.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem galoisGroupPrincipalUnitsSuccQuotMapEquivOfIsIntegralClosure_apply
    (K L : Type u) [Field K] [ValuativeRel K] [Field L] [ValuativeRel L]
    [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    (n : Nat) (σ : Gal(L/K)) (u : principalUnits L n) :
    galoisGroupPrincipalUnitsSuccQuotMapEquivOfIsIntegralClosure K L n σ
        (QuotientGroup.mk u) =
      QuotientGroup.mk
        (galoisGroupPrincipalUnitsMapEquivOfIsIntegralClosure K L n σ u)

def

galoisGroupPrincipalUnitsSuccQuotMapEquivHomOfIsIntegralClosure

L546 ↗

LocalFieldTheory.galoisGroupPrincipalUnitsSuccQuotMapEquivHomOfIsIntegralClosure

Documentation

Actual integral-closure real Galois action on successive principal-unit quotients as a group homomorphism.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · full declaration

def galoisGroupPrincipalUnitsSuccQuotMapEquivHomOfIsIntegralClosure
    (K L : Type u) [Field K] [ValuativeRel K] [Field L] [ValuativeRel L]
    [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    (n : Nat) :
    Gal(L / K) →* (PrincipalUnitsSuccQuot L n ≃* PrincipalUnitsSuccQuot L n) where
  toFun := galoisGroupPrincipalUnitsSuccQuotMapEquivOfIsIntegralClosure K L n
  map_one' := by
    ext x
    refine QuotientGroup.induction_on x ?_
    intro u
    rfl
  map_mul' := by
    intro σ τ
    ext x
    refine QuotientGroup.induction_on x ?_
    intro u
    rfl

def

galoisGroupPrincipalUnitsSuccQuotMulDistribMulActionOfIsIntegralClosure

L570 ↗

LocalFieldTheory.galoisGroupPrincipalUnitsSuccQuotMulDistribMulActionOfIsIntegralClosure

Documentation

Actual integral-closure real Galois action on successive principal-unit quotients, packaged as the multiplicative action required by low-degree Herbrand quotients.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · full declaration

def galoisGroupPrincipalUnitsSuccQuotMulDistribMulActionOfIsIntegralClosure
    (K L : Type u) [Field K] [ValuativeRel K] [Field L] [ValuativeRel L]
    [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    (n : Nat) :
    MulDistribMulAction (Gal(L / K)) (PrincipalUnitsSuccQuot L n) where
  smul σ x := galoisGroupPrincipalUnitsSuccQuotMapEquivOfIsIntegralClosure K L n σ x
  one_smul := by
    intro x
    change galoisGroupPrincipalUnitsSuccQuotMapEquivOfIsIntegralClosure K L n 1 x = x
    have h := congrArg (fun e : PrincipalUnitsSuccQuot L n ≃*
        PrincipalUnitsSuccQuot L n => e x)
      (map_one (galoisGroupPrincipalUnitsSuccQuotMapEquivHomOfIsIntegralClosure K L n))
    exact h
  mul_smul := by
    intro σ τ x
    change galoisGroupPrincipalUnitsSuccQuotMapEquivOfIsIntegralClosure K L n (σ * τ) x =
      galoisGroupPrincipalUnitsSuccQuotMapEquivOfIsIntegralClosure K L n σ
        (galoisGroupPrincipalUnitsSuccQuotMapEquivOfIsIntegralClosure K L n τ x)
    have h := congrArg (fun e : PrincipalUnitsSuccQuot L n ≃*
        PrincipalUnitsSuccQuot L n => e x)
      (map_mul (galoisGroupPrincipalUnitsSuccQuotMapEquivHomOfIsIntegralClosure K L n) σ τ)
    exact h
  smul_mul := by
    intro σ x y
    exact map_mul (galoisGroupPrincipalUnitsSuccQuotMapEquivOfIsIntegralClosure K L n σ) x y
  smul_one := by
    intro σ
    exact map_one (galoisGroupPrincipalUnitsSuccQuotMapEquivOfIsIntegralClosure K L n σ)

theorem

galoisGroupPrincipalUnitsSuccQuotMulDistribMulActionOfIsIntegralClosure_smul

L603 ↗

LocalFieldTheory.galoisGroupPrincipalUnitsSuccQuotMulDistribMulActionOfIsIntegralClosure_smul

Documentation

The packaged integral-closure action is the quotient map equivalence action pointwise.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · full declaration

theorem galoisGroupPrincipalUnitsSuccQuotMulDistribMulActionOfIsIntegralClosure_smul
    (K L : Type u) [Field K] [ValuativeRel K] [Field L] [ValuativeRel L]
    [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    (n : Nat) (σ : Gal(L/K)) (x : PrincipalUnitsSuccQuot L n) :
    letI := galoisGroupPrincipalUnitsSuccQuotMulDistribMulActionOfIsIntegralClosure K L n
    σ • x = galoisGroupPrincipalUnitsSuccQuotMapEquivOfIsIntegralClosure K L n σ x :=
  rfl

def

galoisGroupPrincipalUnitsSuccQuotAddDistribMulActionOfIsIntegralClosure

L616 ↗

LocalFieldTheory.galoisGroupPrincipalUnitsSuccQuotAddDistribMulActionOfIsIntegralClosure

Documentation

Actual integral-closure real Galois action on the additive form of successive principal-unit quotients.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · full declaration

def galoisGroupPrincipalUnitsSuccQuotAddDistribMulActionOfIsIntegralClosure
    (K L : Type u) [Field K] [ValuativeRel K] [Field L] [ValuativeRel L]
    [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    (n : Nat) :
    DistribMulAction (Gal(L / K)) (Additive (PrincipalUnitsSuccQuot L n)) where
  smul σ x :=
    Additive.ofMul
      (galoisGroupPrincipalUnitsSuccQuotMapEquivOfIsIntegralClosure K L n σ
        (Additive.toMul x))
  one_smul := by
    intro x
    change Additive.ofMul
        (galoisGroupPrincipalUnitsSuccQuotMapEquivOfIsIntegralClosure K L n 1
          (Additive.toMul x)) = Additive.ofMul (Additive.toMul x)
    exact congrArg Additive.ofMul
      (congrArg (fun e : PrincipalUnitsSuccQuot L n ≃*
          PrincipalUnitsSuccQuot L n => e (Additive.toMul x))
        (map_one (galoisGroupPrincipalUnitsSuccQuotMapEquivHomOfIsIntegralClosure K L n)))
  mul_smul := by
    intro σ τ x
    change Additive.ofMul
        (galoisGroupPrincipalUnitsSuccQuotMapEquivOfIsIntegralClosure K L n (σ * τ)
          (Additive.toMul x)) =
      Additive.ofMul
        (galoisGroupPrincipalUnitsSuccQuotMapEquivOfIsIntegralClosure K L n σ
          (galoisGroupPrincipalUnitsSuccQuotMapEquivOfIsIntegralClosure K L n τ
            (Additive.toMul x)))
    exact congrArg Additive.ofMul
      (congrArg (fun e : PrincipalUnitsSuccQuot L n ≃*
          PrincipalUnitsSuccQuot L n => e (Additive.toMul x))
        (map_mul (galoisGroupPrincipalUnitsSuccQuotMapEquivHomOfIsIntegralClosure K L n) σ τ))
  smul_zero := by
    intro σ
    change Additive.ofMul
        (galoisGroupPrincipalUnitsSuccQuotMapEquivOfIsIntegralClosure K L n σ 1) =
      Additive.ofMul (1 : PrincipalUnitsSuccQuot L n)
    exact congrArg Additive.ofMul
      (map_one (galoisGroupPrincipalUnitsSuccQuotMapEquivOfIsIntegralClosure K L n σ))
  smul_add := by
    intro σ x y
    change Additive.ofMul
        (galoisGroupPrincipalUnitsSuccQuotMapEquivOfIsIntegralClosure K L n σ
          (Additive.toMul (x + y))) =
      Additive.ofMul
        (galoisGroupPrincipalUnitsSuccQuotMapEquivOfIsIntegralClosure K L n σ
            (Additive.toMul x) *
          galoisGroupPrincipalUnitsSuccQuotMapEquivOfIsIntegralClosure K L n σ
            (Additive.toMul y))
    rw [show Additive.toMul (x + y) = Additive.toMul x * Additive.toMul y from rfl]
    rw [map_mul]

theorem

galoisGroupPrincipalUnitsSuccQuotAddDistribMulActionOfIsIntegralClosure_smul

L671 ↗

LocalFieldTheory.galoisGroupPrincipalUnitsSuccQuotAddDistribMulActionOfIsIntegralClosure_smul

Documentation

The additive Galois action on a successive principal-unit quotient is induced by conjugation of representatives.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · full declaration

theorem galoisGroupPrincipalUnitsSuccQuotAddDistribMulActionOfIsIntegralClosure_smul
    (K L : Type u) [Field K] [ValuativeRel K] [Field L] [ValuativeRel L]
    [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    (n : Nat) (σ : Gal(L/K)) (x : Additive (PrincipalUnitsSuccQuot L n)) :
    letI := galoisGroupPrincipalUnitsSuccQuotAddDistribMulActionOfIsIntegralClosure K L n
    σ • x = Additive.ofMul
      (galoisGroupPrincipalUnitsSuccQuotMapEquivOfIsIntegralClosure K L n σ
        (Additive.toMul x)) :=
  rfl

theorem

principalUnitsSuccQuotOfMaximalIdealPowSuccQuot_galoisGroup_of_isIntegralClosure

L685 ↗

LocalFieldTheory.principalUnitsSuccQuotOfMaximalIdealPowSuccQuot_galoisGroup_of_isIntegralClosure

Documentation

The comparison from a maximal-ideal quotient to a principal-unit quotient intertwines the Galois actions.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem principalUnitsSuccQuotOfMaximalIdealPowSuccQuot_galoisGroup_of_isIntegralClosure
    (K L : Type u) [Field K] [ValuativeRel K] [Field L] [ValuativeRel L]
    [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    (n : Nat) (hn : 1 ≤ n) (σ : Gal(L/K))
    (x : MaximalIdealPowSuccQuot L n) :
    galoisGroupPrincipalUnitsSuccQuotMapEquivOfIsIntegralClosure K L n σ
        (principalUnitsSuccQuotOfMaximalIdealPowSuccQuot L n hn x) =
      principalUnitsSuccQuotOfMaximalIdealPowSuccQuot L n hn
        (galoisGroupMaximalIdealPowSuccQuotMapEquivOfIsIntegralClosure K L n σ x)

theorem

principalUnitsSuccQuotOfMaximalIdealPowSuccQuotAdd_galoisGroup_of_isIntegralClosure

L701 ↗

LocalFieldTheory.principalUnitsSuccQuotOfMaximalIdealPowSuccQuotAdd_galoisGroup_of_isIntegralClosure

Documentation

The additive comparison between maximal-ideal and principal-unit quotients is Galois equivariant.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem principalUnitsSuccQuotOfMaximalIdealPowSuccQuotAdd_galoisGroup_of_isIntegralClosure
    (K L : Type u) [Field K] [ValuativeRel K] [Field L] [ValuativeRel L]
    [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    (n : Nat) (hn : 1 ≤ n) (σ : Gal(L/K))
    (x : MaximalIdealPowSuccQuot L n) :
    Additive.ofMul
        (galoisGroupPrincipalUnitsSuccQuotMapEquivOfIsIntegralClosure K L n σ
          (principalUnitsSuccQuotOfMaximalIdealPowSuccQuot L n hn x)) =
      principalUnitsSuccQuotOfMaximalIdealPowSuccQuotAdd L n hn
        (galoisGroupMaximalIdealPowSuccQuotMapEquivOfIsIntegralClosure K L n σ x)

theorem

maximalIdealPowSuccQuotAddEquivPrincipalUnitsSuccQuot_galoisGroup_of_isIntegralClosure

L718 ↗

LocalFieldTheory.maximalIdealPowSuccQuotAddEquivPrincipalUnitsSuccQuot_galoisGroup_of_isIntegralClosure

Documentation

Real Galois equivariance of the additive associated-graded comparison, with both sides using the packaged additive actions.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · full declaration

theorem maximalIdealPowSuccQuotAddEquivPrincipalUnitsSuccQuot_galoisGroup_of_isIntegralClosure
    (K L : Type u) [Field K] [ValuativeRel K] [Field L] [ValuativeRel L]
    [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    (n : Nat) (hn : 1 ≤ n) (σ : Gal(L/K))
    (x : MaximalIdealPowSuccQuot L n) :
    letI := galoisGroupMaximalIdealPowSuccQuotDistribMulActionOfIsIntegralClosure K L n
    letI := galoisGroupPrincipalUnitsSuccQuotAddDistribMulActionOfIsIntegralClosure K L n
    σ • (maximalIdealPowSuccQuotAddEquivPrincipalUnitsSuccQuot L n hn x) =
      maximalIdealPowSuccQuotAddEquivPrincipalUnitsSuccQuot L n hn (σ • x) := by
  change principalUnitsSuccQuotAddEquivOfIntegerRingEquiv L n
        (galoisGroupIntegerRingEquivOfIsIntegralClosure K L σ)
        (maximalIdealPowSuccQuotAddEquivPrincipalUnitsSuccQuot L n hn x) =
      maximalIdealPowSuccQuotAddEquivPrincipalUnitsSuccQuot L n hn
        (galoisGroupMaximalIdealPowSuccQuotMapEquivOfIsIntegralClosure K L n σ x)
  exact maximalIdealPowSuccQuotAddEquivPrincipalUnitsSuccQuot_integerRingEquiv L n hn
    (galoisGroupIntegerRingEquivOfIsIntegralClosure K L σ) x

theorem

maximalIdealPowSuccQuotMulEquivPrincipalUnitsSuccQuot_galoisGroup_of_isIntegralClosure

L739 ↗

LocalFieldTheory.maximalIdealPowSuccQuotMulEquivPrincipalUnitsSuccQuot_galoisGroup_of_isIntegralClosure

Documentation

Real Galois equivariance of the multiplicative associated-graded comparison, with both sides using the multiplicative packaged actions.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · full declaration

theorem maximalIdealPowSuccQuotMulEquivPrincipalUnitsSuccQuot_galoisGroup_of_isIntegralClosure
    (K L : Type u) [Field K] [ValuativeRel K] [Field L] [ValuativeRel L]
    [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    (n : Nat) (hn : 1 ≤ n) (σ : Gal(L/K))
    (x : Multiplicative (MaximalIdealPowSuccQuot L n)) :
    letI :=
      galoisGroupMaximalIdealPowSuccQuotMultiplicativeMulDistribMulActionOfIsIntegralClosure
        K L n
    letI := galoisGroupPrincipalUnitsSuccQuotMulDistribMulActionOfIsIntegralClosure K L n
    σ • (maximalIdealPowSuccQuotMulEquivPrincipalUnitsSuccQuot L n hn x) =
      maximalIdealPowSuccQuotMulEquivPrincipalUnitsSuccQuot L n hn (σ • x) := by
  change principalUnitsSuccQuotMapEquivOfIntegerRingEquiv L n
        (galoisGroupIntegerRingEquivOfIsIntegralClosure K L σ)
        (maximalIdealPowSuccQuotMulEquivPrincipalUnitsSuccQuot L n hn x) =
      maximalIdealPowSuccQuotMulEquivPrincipalUnitsSuccQuot L n hn
        (maximalIdealPowSuccQuotMultiplicativeMapEquivOfIntegerRingEquiv L n
          (galoisGroupIntegerRingEquivOfIsIntegralClosure K L σ) x)
  exact maximalIdealPowSuccQuotMulEquivPrincipalUnitsSuccQuot_integerRingEquiv L n hn
    (galoisGroupIntegerRingEquivOfIsIntegralClosure K L σ) x

theorem

galoisGroup_prod_one_add_sub_one_sub_sum_mem_maximalIdeal_pow_succ_of_isIntegralClosure

L763 ↗

LocalFieldTheory.galoisGroup_prod_one_add_sub_one_sub_sum_mem_maximalIdeal_pow_succ_of_isIntegralClosure

Documentation

Actual integral-closure first-order expansion of the real Galois product attached to a principal-unit representative.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · full declaration

theorem galoisGroup_prod_one_add_sub_one_sub_sum_mem_maximalIdeal_pow_succ_of_isIntegralClosure
    (K L : Type u) [Field K] [ValuativeRel K] [Field L] [ValuativeRel L]
    [Algebra K L] [FiniteDimensional K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    (n : Nat) (hn : 1 ≤ n) (a : (𝓂[L] ^ n : Ideal 𝒪[L])) :
    (Finset.univ.prod fun σ : Gal(L / K) =>
        1 + galoisGroupIntegerRingEquivOfIsIntegralClosure K L σ (a : 𝒪[L])) - 1 -
      (Finset.univ.sum fun σ : Gal(L / K) =>
        galoisGroupIntegerRingEquivOfIsIntegralClosure K L σ (a : 𝒪[L])) ∈
        (𝓂[L] ^ (n + 1) : Ideal 𝒪[L]) := by
  classical
  refine finset_prod_one_add_sub_one_sub_sum_mem_maximalIdeal_pow_succ L
    (Finset.univ : Finset (Gal(L / K))) n hn
    (fun σ => galoisGroupIntegerRingEquivOfIsIntegralClosure K L σ (a : 𝒪[L])) ?_
  intro σ _
  exact (integerRingEquiv_mem_maximalIdeal_pow L
    (galoisGroupIntegerRingEquivOfIsIntegralClosure K L σ) n (a : 𝒪[L])).2 a.2

Module documentation

Galois actions on valuation rings

Declarations