Module

AutomorphismEquiv.lean

Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.PrincipalUnits.AutomorphismEquiv

4 declarations indexed from sourceView source ↗

Module documentation

Automorphisms of the concrete principal-unit groups

A field automorphism preserving the valuation ring restricts to every level of the principal-unit filtration, with its original action on field elements.

Imports2

Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.PrincipalUnits.AutomorphismTransport
Mathlib.Algebra.Group.Subgroup.Map

Imported by4

def

equivOfPreserves

L25 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.equivOfPreserves

Documentation

Restriction of a valuation-ring-preserving automorphism to U^n.

Source context 4 commands

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

namespace LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
universe u v
variable {K : Type u} [Field K]
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

def equivOfPreserves
    (e : K ≃+* K)
    (hmem : ∀ x : K, x ∈ F.valuation.valuationSubring ↔ e x ∈ F.valuation.valuationSubring)
    (n : ℕ) : higherPrincipalUnitGroup F n ≃* higherPrincipalUnitGroup F n

theorem

equivOfPreserves_apply_coe

L35 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.equivOfPreserves_apply_coe

Documentation

The restricted automorphism retains the original action on field elements.

Source context 4 commands

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

namespace LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
universe u v
variable {K : Type u} [Field K]
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

theorem equivOfPreserves_apply_coe
    (e : K ≃+* K)
    (hmem : ∀ x : K, x ∈ F.valuation.valuationSubring ↔ e x ∈ F.valuation.valuationSubring)
    (n : ℕ) (a : higherPrincipalUnitGroup F n) :
    (((equivOfPreserves F e hmem n a : F.valuationSubringˣ) : F.valuationSubring) : K) =
      e (((a : F.valuationSubringˣ) : F.valuationSubring) : K)

theorem

equivOfPreserves_refl

L48 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.equivOfPreserves_refl

Documentation

Restriction preserves the identity automorphism.

Source context 4 commands

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

namespace LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
universe u v
variable {K : Type u} [Field K]
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · full declaration

theorem equivOfPreserves_refl (n : ℕ) :
    equivOfPreserves F (RingEquiv.refl K) (fun _ => Iff.rfl) n =
      MulEquiv.refl (higherPrincipalUnitGroup F n) := by
  apply MulEquiv.ext
  intro a
  apply Subtype.ext
  apply Units.ext
  apply Subtype.ext
  exact equivOfPreserves_apply_coe F (RingEquiv.refl K) (fun _ => Iff.rfl) n a

theorem

equivOfPreserves_trans

L59 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.equivOfPreserves_trans

Documentation

Restriction preserves composition, with e applied before f.

Source context 4 commands

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

namespace LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
universe u v
variable {K : Type u} [Field K]
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · full declaration

theorem equivOfPreserves_trans
    (e f : K ≃+* K)
    (he : ∀ x : K, x ∈ F.valuation.valuationSubring ↔ e x ∈ F.valuation.valuationSubring)
    (hf : ∀ x : K, x ∈ F.valuation.valuationSubring ↔ f x ∈ F.valuation.valuationSubring)
    (n : ℕ) :
    equivOfPreserves F (e.trans f) (fun x => (he x).trans (hf (e x))) n =
      (equivOfPreserves F e he n).trans (equivOfPreserves F f hf n) := by
  apply MulEquiv.ext
  intro a
  apply Subtype.ext
  apply Units.ext
  apply Subtype.ext
  simp only [MulEquiv.trans_apply, equivOfPreserves_apply_coe, RingEquiv.trans_apply]

Module documentation

Automorphisms of the concrete principal-unit groups

Declarations

equivOfPreserves

equivOfPreserves_apply_coe

equivOfPreserves_refl

equivOfPreserves_trans