NYLL
Module

ValuationTransport.lean

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.ValuationTransport
7 declarations indexed from sourceView source ↗

Module documentation

Valuation transport along field equivalences

This file records the source facts needed to transport complete-DVF data from a finite subextension to its image inside a common ambient field. The transport is by comapping the valuation along a field equivalence; no valuation-comparison hypothesis is added.

Imports1
Imported by8

Declarations

theorem

valueGroup_comap_ringEquiv

L32 ↗
ValuationTheory.DiscreteValuationField.Valuation.valueGroup_comap_ringEquiv
Documentation

Pulling a valuation back along a field equivalence does not change its value group.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
namespace Valuation
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable {Γ : Type v} [LinearOrderedCommGroupWithZero Γ]
Lean source · statement
theorem valueGroup_comap_ringEquiv
    (v : _root_.Valuation K Γ) (e : L ≃+* K) :
    MonoidWithZeroHom.valueGroup
        (.ofClass (v.comap (e : L →+* K))) =
      MonoidWithZeroHom.valueGroup (.ofClass v)
instance

isRankOneDiscrete_comap_ringEquiv

L85 ↗
ValuationTheory.DiscreteValuationField.Valuation.isRankOneDiscrete_comap_ringEquiv
Documentation

Rank-one discreteness is preserved by pulling a valuation back along a field equivalence.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
namespace Valuation
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable {Γ : Type v} [LinearOrderedCommGroupWithZero Γ]
Lean source · full declaration
instance isRankOneDiscrete_comap_ringEquiv
    (v : _root_.Valuation K Γ) [v.IsRankOneDiscrete] (e : L ≃+* K) :
    (v.comap (e : L →+* K)).IsRankOneDiscrete where
  exists_generator_lt_one' := by
    rcases _root_.Valuation.IsRankOneDiscrete.exists_generator_lt_one v with
      ⟨γ, hγ, hlt⟩
    refine ⟨γ, ?_, hlt⟩
    change Subgroup.zpowers γ =
      MonoidWithZeroHom.valueGroup (.ofClass (v.comap (e : L →+* K)))
    rw [valueGroup_comap_ringEquiv (v := v) e]
    exact hγ
def

valuationSubringRingEquivOfComap

L99 ↗
ValuationTheory.DiscreteValuationField.Valuation.valuationSubringRingEquivOfComap
Documentation

The valuation ring of a comapped valuation is the source valuation ring, transported through the field equivalence.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
namespace Valuation
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable {Γ : Type v} [LinearOrderedCommGroupWithZero Γ]
Lean source · full declaration
def valuationSubringRingEquivOfComap
    (v : _root_.Valuation K Γ) (e : L ≃+* K) :
    (v.comap (e : L →+* K)).valuationSubring ≃+* v.valuationSubring where
  toFun x := ⟨e (x : L), x.2⟩
  invFun y := ⟨e.symm (y : K), by
    change v (e (e.symm (y : K))) ≤ 1
    rw [e.apply_symm_apply]
    exact y.2⟩
  left_inv x := by
    ext
    simp
  right_inv y := by
    ext
    simp
  map_mul' x y := by
    ext
    simp
  map_add' x y := by
    ext
    simp
theorem

valuationSubringRingEquivOfComap_apply

L121 ↗
ValuationTheory.DiscreteValuationField.Valuation.valuationSubringRingEquivOfComap_apply
Documentation

The valuation-subring equivalence induced by a comap acts through the ambient ring map.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
namespace Valuation
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable {Γ : Type v} [LinearOrderedCommGroupWithZero Γ]
Lean source · statement
theorem valuationSubringRingEquivOfComap_apply
    (v : _root_.Valuation K Γ) (e : L ≃+* K)
    (x : (v.comap (e : L →+* K)).valuationSubring) :
    ((valuationSubringRingEquivOfComap v e x : v.valuationSubring) : K) =
      e (x : L)
theorem

valuationSubringRingEquivOfComap_mem_maximalIdeal_iff

L130 ↗
ValuationTheory.DiscreteValuationField.Valuation.valuationSubringRingEquivOfComap_mem_maximalIdeal_iff
Documentation

The valuation-ring equivalence attached to a comap carries maximal-ideal membership exactly.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
namespace Valuation
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable {Γ : Type v} [LinearOrderedCommGroupWithZero Γ]
Lean source · statement
theorem valuationSubringRingEquivOfComap_mem_maximalIdeal_iff
    (v : _root_.Valuation K Γ) (e : L ≃+* K)
    (x : (v.comap (e : L →+* K)).valuationSubring) :
    valuationSubringRingEquivOfComap v e x ∈
        IsLocalRing.maximalIdeal v.valuationSubring ↔
      x ∈ IsLocalRing.maximalIdeal
        (v.comap (e : L →+* K)).valuationSubring
theorem

maximalIdeal_map_valuationSubringRingEquivOfComap

L143 ↗
ValuationTheory.DiscreteValuationField.Valuation.maximalIdeal_map_valuationSubringRingEquivOfComap
Documentation

Map form of maximal-ideal preservation for the valuation-ring equivalence attached to a comap.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
namespace Valuation
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable {Γ : Type v} [LinearOrderedCommGroupWithZero Γ]
Lean source · statement
theorem maximalIdeal_map_valuationSubringRingEquivOfComap
    (v : _root_.Valuation K Γ) (e : L ≃+* K) :
    (IsLocalRing.maximalIdeal
        (v.comap (e : L →+* K)).valuationSubring).map
        (valuationSubringRingEquivOfComap v e :
          (v.comap (e : L →+* K)).valuationSubring →+*
            v.valuationSubring) =
      IsLocalRing.maximalIdeal v.valuationSubring
theorem

maximalIdeal_comap_valuationSubringRingEquivOfComap

L168 ↗
ValuationTheory.DiscreteValuationField.Valuation.maximalIdeal_comap_valuationSubringRingEquivOfComap
Documentation

Comap form of maximal-ideal preservation for the valuation-ring equivalence attached to a comap.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
namespace Valuation
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable {Γ : Type v} [LinearOrderedCommGroupWithZero Γ]
Lean source · statement
theorem maximalIdeal_comap_valuationSubringRingEquivOfComap
    (v : _root_.Valuation K Γ) (e : L ≃+* K) :
    (IsLocalRing.maximalIdeal v.valuationSubring).comap
        (valuationSubringRingEquivOfComap v e :
          (v.comap (e : L →+* K)).valuationSubring →+*
            v.valuationSubring) =
      IsLocalRing.maximalIdeal
        (v.comap (e : L →+* K)).valuationSubring

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.