Documentation

Mathlib.RingTheory.Valuation.ValuationSubring

Valuation subrings of a field #

Projects #

The order structure on ValuationSubring K.

structure ValuationSubring (K : Type u) [Field K] extends Subring :

A valuation subring of a field K is a subring A such that for every x : K, either x ∈ A or x⁻¹ ∈ A.

  • carrier : Set K
  • mul_mem' : ∀ {a b : K}, a self.carrierb self.carriera * b self.carrier
  • one_mem' : 1 self.carrier
  • add_mem' : ∀ {a b : K}, a self.carrierb self.carriera + b self.carrier
  • zero_mem' : 0 self.carrier
  • neg_mem' : ∀ {x : K}, x self.carrier-x self.carrier
  • mem_or_inv_mem' : ∀ (x : K), x self.carrier x⁻¹ self.carrier
Instances For
    theorem ValuationSubring.mem_or_inv_mem' {K : Type u} [Field K] (self : ValuationSubring K) (x : K) :
    x self.carrier x⁻¹ self.carrier
    Equations
    • ValuationSubring.instSetLike = { coe := fun (A : ValuationSubring K) => A.toSubring, coe_injective' := }
    @[simp]
    theorem ValuationSubring.mem_carrier {K : Type u} [Field K] (A : ValuationSubring K) (x : K) :
    x A.carrier x A
    @[simp]
    theorem ValuationSubring.mem_toSubring {K : Type u} [Field K] (A : ValuationSubring K) (x : K) :
    x A.toSubring x A
    theorem ValuationSubring.ext_iff {K : Type u} [Field K] {A : ValuationSubring K} {B : ValuationSubring K} :
    A = B ∀ (x : K), x A x B
    theorem ValuationSubring.ext {K : Type u} [Field K] (A : ValuationSubring K) (B : ValuationSubring K) (h : ∀ (x : K), x A x B) :
    A = B
    theorem ValuationSubring.add_mem {K : Type u} [Field K] (A : ValuationSubring K) (x : K) (y : K) :
    x Ay Ax + y A
    theorem ValuationSubring.mul_mem {K : Type u} [Field K] (A : ValuationSubring K) (x : K) (y : K) :
    x Ay Ax * y A
    theorem ValuationSubring.neg_mem {K : Type u} [Field K] (A : ValuationSubring K) (x : K) :
    x A-x A
    theorem ValuationSubring.mem_or_inv_mem {K : Type u} [Field K] (A : ValuationSubring K) (x : K) :
    x A x⁻¹ A
    theorem ValuationSubring.toSubring_injective {K : Type u} [Field K] :
    Function.Injective ValuationSubring.toSubring
    Equations
    • A.instCommRingSubtypeMem = inferInstance
    Equations
    • =
    Equations
    • ValuationSubring.instTop = { top := let __src := ; { toSubring := __src, mem_or_inv_mem' := } }
    theorem ValuationSubring.mem_top {K : Type u} [Field K] (x : K) :
    Equations
    Equations
    • ValuationSubring.instInhabited = { default := }
    Equations
    • A.instAlgebraSubtypeMem = inferInstance
    Equations
    • =
    @[simp]
    theorem ValuationSubring.algebraMap_apply {K : Type u} [Field K] (A : ValuationSubring K) (a : A) :
    (algebraMap (↥A) K) a = a

    The value group of the valuation associated to A. Note: it is actually a group with zero.

    Equations
    Instances For
      Equations
      • A.instLinearOrderedCommGroupWithZeroValueGroup = id inferInstance
      def ValuationSubring.valuation {K : Type u} [Field K] (A : ValuationSubring K) :
      Valuation K A.ValueGroup

      Any valuation subring of K induces a natural valuation on K.

      Equations
      Instances For
        instance ValuationSubring.inhabitedValueGroup {K : Type u} [Field K] (A : ValuationSubring K) :
        Inhabited A.ValueGroup
        Equations
        • A.inhabitedValueGroup = { default := A.valuation 0 }
        theorem ValuationSubring.valuation_le_one {K : Type u} [Field K] (A : ValuationSubring K) (a : A) :
        A.valuation a 1
        theorem ValuationSubring.mem_of_valuation_le_one {K : Type u} [Field K] (A : ValuationSubring K) (x : K) (h : A.valuation x 1) :
        x A
        theorem ValuationSubring.valuation_le_one_iff {K : Type u} [Field K] (A : ValuationSubring K) (x : K) :
        A.valuation x 1 x A
        theorem ValuationSubring.valuation_eq_iff {K : Type u} [Field K] (A : ValuationSubring K) (x : K) (y : K) :
        A.valuation x = A.valuation y ∃ (a : (↥A)ˣ), a * y = x
        theorem ValuationSubring.valuation_le_iff {K : Type u} [Field K] (A : ValuationSubring K) (x : K) (y : K) :
        A.valuation x A.valuation y ∃ (a : A), a * y = x
        theorem ValuationSubring.valuation_unit {K : Type u} [Field K] (A : ValuationSubring K) (a : (↥A)ˣ) :
        A.valuation a = 1
        theorem ValuationSubring.valuation_eq_one_iff {K : Type u} [Field K] (A : ValuationSubring K) (a : A) :
        IsUnit a A.valuation a = 1
        theorem ValuationSubring.valuation_lt_one_or_eq_one {K : Type u} [Field K] (A : ValuationSubring K) (a : A) :
        A.valuation a < 1 A.valuation a = 1
        theorem ValuationSubring.valuation_lt_one_iff {K : Type u} [Field K] (A : ValuationSubring K) (a : A) :
        a LocalRing.maximalIdeal A A.valuation a < 1
        def ValuationSubring.ofSubring {K : Type u} [Field K] (R : Subring K) (hR : ∀ (x : K), x R x⁻¹ R) :

        A subring R of K such that for all x : K either x ∈ R or x⁻¹ ∈ R is a valuation subring of K.

        Equations
        Instances For
          @[simp]
          theorem ValuationSubring.mem_ofSubring {K : Type u} [Field K] (R : Subring K) (hR : ∀ (x : K), x R x⁻¹ R) (x : K) :
          def ValuationSubring.ofLE {K : Type u} [Field K] (R : ValuationSubring K) (S : Subring K) (h : R.toSubring S) :

          An overring of a valuation ring is a valuation ring.

          Equations
          • R.ofLE S h = { toSubring := S, mem_or_inv_mem' := }
          Instances For
            Equations
            def ValuationSubring.inclusion {K : Type u} [Field K] (R : ValuationSubring K) (S : ValuationSubring K) (h : R S) :
            R →+* S

            The ring homomorphism induced by the partial order.

            Equations
            Instances For
              def ValuationSubring.subtype {K : Type u} [Field K] (R : ValuationSubring K) :
              R →+* K

              The canonical ring homomorphism from a valuation ring to its field of fractions.

              Equations
              • R.subtype = R.subtype
              Instances For
                def ValuationSubring.mapOfLE {K : Type u} [Field K] (R : ValuationSubring K) (S : ValuationSubring K) (h : R S) :
                R.ValueGroup →*₀ S.ValueGroup

                The canonical map on value groups induced by a coarsening of valuation rings.

                Equations
                • R.mapOfLE S h = { toFun := Quotient.map' id , map_zero' := , map_one' := , map_mul' := }
                Instances For
                  theorem ValuationSubring.monotone_mapOfLE {K : Type u} [Field K] (R : ValuationSubring K) (S : ValuationSubring K) (h : R S) :
                  Monotone (R.mapOfLE S h)
                  @[simp]
                  theorem ValuationSubring.mapOfLE_comp_valuation {K : Type u} [Field K] (R : ValuationSubring K) (S : ValuationSubring K) (h : R S) :
                  (R.mapOfLE S h) R.valuation = S.valuation
                  @[simp]
                  theorem ValuationSubring.mapOfLE_valuation_apply {K : Type u} [Field K] (R : ValuationSubring K) (S : ValuationSubring K) (h : R S) (x : K) :
                  (R.mapOfLE S h) (R.valuation x) = S.valuation x
                  def ValuationSubring.idealOfLE {K : Type u} [Field K] (R : ValuationSubring K) (S : ValuationSubring K) (h : R S) :
                  Ideal R

                  The ideal corresponding to a coarsening of a valuation ring.

                  Equations
                  Instances For
                    instance ValuationSubring.prime_idealOfLE {K : Type u} [Field K] (R : ValuationSubring K) (S : ValuationSubring K) (h : R S) :
                    (R.idealOfLE S h).IsPrime
                    Equations
                    • =
                    def ValuationSubring.ofPrime {K : Type u} [Field K] (A : ValuationSubring K) (P : Ideal A) [P.IsPrime] :

                    The coarsening of a valuation ring associated to a prime ideal.

                    Equations
                    Instances For
                      instance ValuationSubring.ofPrimeAlgebra {K : Type u} [Field K] (A : ValuationSubring K) (P : Ideal A) [P.IsPrime] :
                      Algebra A (A.ofPrime P)
                      Equations
                      instance ValuationSubring.ofPrime_scalar_tower {K : Type u} [Field K] (A : ValuationSubring K) (P : Ideal A) [P.IsPrime] :
                      IsScalarTower (↥A) (↥(A.ofPrime P)) K
                      Equations
                      • =
                      instance ValuationSubring.ofPrime_localization {K : Type u} [Field K] (A : ValuationSubring K) (P : Ideal A) [P.IsPrime] :
                      IsLocalization.AtPrime (↥(A.ofPrime P)) P
                      Equations
                      • =
                      theorem ValuationSubring.le_ofPrime {K : Type u} [Field K] (A : ValuationSubring K) (P : Ideal A) [P.IsPrime] :
                      A A.ofPrime P
                      theorem ValuationSubring.ofPrime_valuation_eq_one_iff_mem_primeCompl {K : Type u} [Field K] (A : ValuationSubring K) (P : Ideal A) [P.IsPrime] (x : A) :
                      (A.ofPrime P).valuation x = 1 x P.primeCompl
                      @[simp]
                      theorem ValuationSubring.idealOfLE_ofPrime {K : Type u} [Field K] (A : ValuationSubring K) (P : Ideal A) [P.IsPrime] :
                      A.idealOfLE (A.ofPrime P) = P
                      @[simp]
                      theorem ValuationSubring.ofPrime_idealOfLE {K : Type u} [Field K] (R : ValuationSubring K) (S : ValuationSubring K) (h : R S) :
                      R.ofPrime (R.idealOfLE S h) = S
                      theorem ValuationSubring.ofPrime_le_of_le {K : Type u} [Field K] (A : ValuationSubring K) (P : Ideal A) (Q : Ideal A) [P.IsPrime] [Q.IsPrime] (h : P Q) :
                      A.ofPrime Q A.ofPrime P
                      theorem ValuationSubring.idealOfLE_le_of_le {K : Type u} [Field K] (A : ValuationSubring K) (R : ValuationSubring K) (S : ValuationSubring K) (hR : A R) (hS : A S) (h : R S) :
                      A.idealOfLE S hS A.idealOfLE R hR
                      @[simp]
                      theorem ValuationSubring.primeSpectrumEquiv_symm_apply_asIdeal {K : Type u} [Field K] (A : ValuationSubring K) (S : { S : ValuationSubring K // A S }) :
                      (A.primeSpectrumEquiv.symm S).asIdeal = A.idealOfLE S
                      @[simp]
                      theorem ValuationSubring.primeSpectrumEquiv_apply_coe {K : Type u} [Field K] (A : ValuationSubring K) (P : PrimeSpectrum A) :
                      (A.primeSpectrumEquiv P) = A.ofPrime P.asIdeal

                      The equivalence between coarsenings of a valuation ring and its prime ideals.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        @[simp]
                        theorem ValuationSubring.primeSpectrumOrderEquiv_apply_coe_carrier {K : Type u} [Field K] (A : ValuationSubring K) (P : PrimeSpectrum A) :
                        (A.primeSpectrumOrderEquiv P) = {x : K | aA, ∃ (a_1 : K), (∃ (x : a_1 A), a_1, P.asIdeal.primeCompl) x = a * a_1⁻¹}
                        @[simp]
                        theorem ValuationSubring.primeSpectrumOrderEquiv_symm_apply_asIdeal_carrier {K : Type u} [Field K] (A : ValuationSubring K) (S : { S : ValuationSubring K // A S }) :
                        ((RelIso.symm A.primeSpectrumOrderEquiv) S).asIdeal = (A.inclusion S ) ⁻¹' (LocalRing.maximalIdeal S)

                        An ordered variant of primeSpectrumEquiv.

                        Equations
                        • A.primeSpectrumOrderEquiv = { toEquiv := A.primeSpectrumEquiv, map_rel_iff' := }
                        Instances For
                          Equations
                          • A.linearOrderOverring = LinearOrder.mk inferInstance decidableEqOfDecidableLE decidableLTOfDecidableLE

                          The valuation subring associated to a valuation.

                          Equations
                          • v.valuationSubring = { toSubring := v.integer, mem_or_inv_mem' := }
                          Instances For
                            @[simp]
                            theorem Valuation.mem_valuationSubring_iff {K : Type u} [Field K] {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] (v : Valuation K Γ) (x : K) :
                            x v.valuationSubring v x 1
                            theorem Valuation.isEquiv_iff_valuationSubring {K : Type u} [Field K] {Γ₁ : Type u_2} {Γ₂ : Type u_3} [LinearOrderedCommGroupWithZero Γ₁] [LinearOrderedCommGroupWithZero Γ₂] (v₁ : Valuation K Γ₁) (v₂ : Valuation K Γ₂) :
                            v₁.IsEquiv v₂ v₁.valuationSubring = v₂.valuationSubring
                            theorem Valuation.isEquiv_valuation_valuationSubring {K : Type u} [Field K] {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] (v : Valuation K Γ) :
                            v.IsEquiv v.valuationSubring.valuation
                            @[simp]
                            theorem ValuationSubring.valuationSubring_valuation {K : Type u} [Field K] (A : ValuationSubring K) :
                            A.valuation.valuationSubring = A

                            The unit group of a valuation subring, as a subgroup of .

                            Equations
                            • A.unitGroup = ((↑A.valuation.toMonoidWithZeroHom).comp (Units.coeHom K)).ker
                            Instances For
                              @[simp]
                              theorem ValuationSubring.mem_unitGroup_iff {K : Type u} [Field K] (A : ValuationSubring K) (x : Kˣ) :
                              x A.unitGroup A.valuation x = 1
                              def ValuationSubring.unitGroupMulEquiv {K : Type u} [Field K] (A : ValuationSubring K) :
                              A.unitGroup ≃* (↥A)ˣ

                              For a valuation subring A, A.unitGroup agrees with the units of A.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                @[simp]
                                theorem ValuationSubring.coe_unitGroupMulEquiv_apply {K : Type u} [Field K] (A : ValuationSubring K) (a : A.unitGroup) :
                                (A.unitGroupMulEquiv a) = a
                                @[simp]
                                theorem ValuationSubring.coe_unitGroupMulEquiv_symm_apply {K : Type u} [Field K] (A : ValuationSubring K) (a : (↥A)ˣ) :
                                (A.unitGroupMulEquiv.symm a) = a
                                theorem ValuationSubring.unitGroup_le_unitGroup {K : Type u} [Field K] {A : ValuationSubring K} {B : ValuationSubring K} :
                                A.unitGroup B.unitGroup A B
                                theorem ValuationSubring.unitGroup_injective {K : Type u} [Field K] :
                                Function.Injective ValuationSubring.unitGroup
                                theorem ValuationSubring.eq_iff_unitGroup {K : Type u} [Field K] {A : ValuationSubring K} {B : ValuationSubring K} :
                                A = B A.unitGroup = B.unitGroup

                                The map on valuation subrings to their unit groups is an order embedding.

                                Equations
                                • ValuationSubring.unitGroupOrderEmbedding = { toFun := fun (A : ValuationSubring K) => A.unitGroup, inj' := , map_rel_iff' := }
                                Instances For
                                  theorem ValuationSubring.unitGroup_strictMono {K : Type u} [Field K] :
                                  StrictMono ValuationSubring.unitGroup

                                  The nonunits of a valuation subring of K, as a subsemigroup of K

                                  Equations
                                  • A.nonunits = { carrier := {x : K | A.valuation x < 1}, mul_mem' := }
                                  Instances For
                                    theorem ValuationSubring.mem_nonunits_iff {K : Type u} [Field K] (A : ValuationSubring K) {x : K} :
                                    x A.nonunits A.valuation x < 1
                                    theorem ValuationSubring.nonunits_le_nonunits {K : Type u} [Field K] {A : ValuationSubring K} {B : ValuationSubring K} :
                                    B.nonunits A.nonunits A B
                                    theorem ValuationSubring.nonunits_injective {K : Type u} [Field K] :
                                    Function.Injective ValuationSubring.nonunits
                                    theorem ValuationSubring.nonunits_inj {K : Type u} [Field K] {A : ValuationSubring K} {B : ValuationSubring K} :
                                    A.nonunits = B.nonunits A = B

                                    The map on valuation subrings to their nonunits is a dual order embedding.

                                    Equations
                                    • ValuationSubring.nonunitsOrderEmbedding = { toFun := fun (A : ValuationSubring K) => A.nonunits, inj' := , map_rel_iff' := }
                                    Instances For
                                      theorem ValuationSubring.coe_mem_nonunits_iff {K : Type u} [Field K] {A : ValuationSubring K} {a : A} :
                                      a A.nonunits a LocalRing.maximalIdeal A

                                      The elements of A.nonunits are those of the maximal ideal of A after coercion to K.

                                      See also mem_nonunits_iff_exists_mem_maximalIdeal, which gets rid of the coercion to K, at the expense of a more complicated right hand side.

                                      theorem ValuationSubring.nonunits_le {K : Type u} [Field K] {A : ValuationSubring K} :
                                      A.nonunits A.toSubsemigroup
                                      theorem ValuationSubring.nonunits_subset {K : Type u} [Field K] {A : ValuationSubring K} :
                                      A.nonunits A
                                      theorem ValuationSubring.mem_nonunits_iff_exists_mem_maximalIdeal {K : Type u} [Field K] {A : ValuationSubring K} {a : K} :
                                      a A.nonunits ∃ (ha : a A), a, ha LocalRing.maximalIdeal A

                                      The elements of A.nonunits are those of the maximal ideal of A.

                                      See also coe_mem_nonunits_iff, which has a simpler right hand side but requires the element to be in A already.

                                      theorem ValuationSubring.image_maximalIdeal {K : Type u} [Field K] {A : ValuationSubring K} :
                                      Subtype.val '' (LocalRing.maximalIdeal A) = A.nonunits

                                      A.nonunits agrees with the maximal ideal of A, after taking its image in K.

                                      The principal unit group of a valuation subring, as a subgroup of .

                                      Equations
                                      • A.principalUnitGroup = { carrier := {x : Kˣ | A.valuation (x - 1) < 1}, mul_mem' := , one_mem' := , inv_mem' := }
                                      Instances For
                                        theorem ValuationSubring.principal_units_le_units {K : Type u} [Field K] (A : ValuationSubring K) :
                                        A.principalUnitGroup A.unitGroup
                                        theorem ValuationSubring.mem_principalUnitGroup_iff {K : Type u} [Field K] (A : ValuationSubring K) (x : Kˣ) :
                                        x A.principalUnitGroup A.valuation (x - 1) < 1
                                        theorem ValuationSubring.principalUnitGroup_le_principalUnitGroup {K : Type u} [Field K] {A : ValuationSubring K} {B : ValuationSubring K} :
                                        B.principalUnitGroup A.principalUnitGroup A B
                                        theorem ValuationSubring.principalUnitGroup_injective {K : Type u} [Field K] :
                                        Function.Injective ValuationSubring.principalUnitGroup
                                        theorem ValuationSubring.eq_iff_principalUnitGroup {K : Type u} [Field K] {A : ValuationSubring K} {B : ValuationSubring K} :
                                        A = B A.principalUnitGroup = B.principalUnitGroup

                                        The map on valuation subrings to their principal unit groups is an order embedding.

                                        Equations
                                        • ValuationSubring.principalUnitGroupOrderEmbedding = { toFun := fun (A : ValuationSubring K) => A.principalUnitGroup, inj' := , map_rel_iff' := }
                                        Instances For
                                          theorem ValuationSubring.coe_mem_principalUnitGroup_iff {K : Type u} [Field K] (A : ValuationSubring K) {x : A.unitGroup} :
                                          x A.principalUnitGroup A.unitGroupMulEquiv x (Units.map (LocalRing.residue A)).ker
                                          def ValuationSubring.principalUnitGroupEquiv {K : Type u} [Field K] (A : ValuationSubring K) :
                                          A.principalUnitGroup ≃* (Units.map (LocalRing.residue A)).ker

                                          The principal unit group agrees with the kernel of the canonical map from the units of A to the units of the residue field of A.

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            theorem ValuationSubring.principalUnitGroupEquiv_apply {K : Type u} [Field K] (A : ValuationSubring K) (a : A.principalUnitGroup) :
                                            (A.principalUnitGroupEquiv a) = a
                                            theorem ValuationSubring.principalUnitGroup_symm_apply {K : Type u} [Field K] (A : ValuationSubring K) (a : (Units.map (LocalRing.residue A)).ker) :
                                            (A.principalUnitGroupEquiv.symm a) = a

                                            The canonical map from the unit group of A to the units of the residue field of A.

                                            Equations
                                            Instances For
                                              @[simp]
                                              theorem ValuationSubring.coe_unitGroupToResidueFieldUnits_apply {K : Type u} [Field K] (A : ValuationSubring K) (x : A.unitGroup) :
                                              (A.unitGroupToResidueFieldUnits x) = (Ideal.Quotient.mk (LocalRing.maximalIdeal A)) (A.unitGroupMulEquiv x)
                                              theorem ValuationSubring.ker_unitGroupToResidueFieldUnits {K : Type u} [Field K] (A : ValuationSubring K) :
                                              A.unitGroupToResidueFieldUnits.ker = Subgroup.comap A.unitGroup.subtype A.principalUnitGroup
                                              def ValuationSubring.unitsModPrincipalUnitsEquivResidueFieldUnits {K : Type u} [Field K] (A : ValuationSubring K) :
                                              A.unitGroup Subgroup.comap A.unitGroup.subtype A.principalUnitGroup ≃* (LocalRing.ResidueField A)ˣ

                                              The quotient of the unit group of A by the principal unit group of A agrees with the units of the residue field of A.

                                              Equations
                                              Instances For

                                                Porting note: Lean needs to be reminded of this instance

                                                Equations
                                                • A.instMulOneClassQuotientSubtypeUnitsMemSubgroupUnitGroupComapSubtypePrincipalUnitGroup = inferInstance
                                                Instances For
                                                  theorem ValuationSubring.unitsModPrincipalUnitsEquivResidueFieldUnits_comp_quotientGroup_mk {K : Type u} [Field K] (A : ValuationSubring K) :
                                                  A.unitsModPrincipalUnitsEquivResidueFieldUnits.toMonoidHom.comp (QuotientGroup.mk' (Subgroup.comap A.unitGroup.subtype A.principalUnitGroup)) = A.unitGroupToResidueFieldUnits
                                                  theorem ValuationSubring.unitsModPrincipalUnitsEquivResidueFieldUnits_comp_quotientGroup_mk_apply {K : Type u} [Field K] (A : ValuationSubring K) (x : A.unitGroup) :
                                                  A.unitsModPrincipalUnitsEquivResidueFieldUnits.toMonoidHom x = A.unitGroupToResidueFieldUnits x

                                                  Pointwise actions #

                                                  This transfers the action from Subring.pointwiseMulAction, noting that it only applies when the action is by a group. Notably this provides an instances when G is K ≃+* K.

                                                  These instances are in the Pointwise locale.

                                                  The lemmas in this section are copied from the file Mathlib.Algebra.Ring.Subring.Pointwise; try to keep these in sync.

                                                  The action on a valuation subring corresponding to applying the action to every element.

                                                  This is available as an instance in the Pointwise locale.

                                                  Equations
                                                  • ValuationSubring.pointwiseHasSMul = { smul := fun (g : G) (S : ValuationSubring K) => let __src := g S.toSubring; { toSubring := __src, mem_or_inv_mem' := } }
                                                  Instances For
                                                    @[simp]
                                                    theorem ValuationSubring.coe_pointwise_smul {K : Type u} [Field K] {G : Type u_1} [Group G] [MulSemiringAction G K] (g : G) (S : ValuationSubring K) :
                                                    (g S) = g S
                                                    @[simp]
                                                    theorem ValuationSubring.pointwise_smul_toSubring {K : Type u} [Field K] {G : Type u_1} [Group G] [MulSemiringAction G K] (g : G) (S : ValuationSubring K) :
                                                    (g S).toSubring = g S.toSubring

                                                    The action on a valuation subring corresponding to applying the action to every element.

                                                    This is available as an instance in the Pointwise locale.

                                                    This is a stronger version of ValuationSubring.pointwiseSMul.

                                                    Equations
                                                    Instances For
                                                      theorem ValuationSubring.smul_mem_pointwise_smul {K : Type u} [Field K] {G : Type u_1} [Group G] [MulSemiringAction G K] (g : G) (x : K) (S : ValuationSubring K) :
                                                      x Sg x g S
                                                      instance ValuationSubring.instCovariantClassHSMulLe {K : Type u} [Field K] {G : Type u_1} [Group G] [MulSemiringAction G K] :
                                                      CovariantClass G (ValuationSubring K) HSMul.hSMul LE.le
                                                      Equations
                                                      • =
                                                      theorem ValuationSubring.mem_smul_pointwise_iff_exists {K : Type u} [Field K] {G : Type u_1} [Group G] [MulSemiringAction G K] (g : G) (x : K) (S : ValuationSubring K) :
                                                      x g S sS, g s = x
                                                      @[simp]
                                                      theorem ValuationSubring.smul_mem_pointwise_smul_iff {K : Type u} [Field K] {G : Type u_1} [Group G] [MulSemiringAction G K] {g : G} {S : ValuationSubring K} {x : K} :
                                                      g x g S x S
                                                      theorem ValuationSubring.mem_pointwise_smul_iff_inv_smul_mem {K : Type u} [Field K] {G : Type u_1} [Group G] [MulSemiringAction G K] {g : G} {S : ValuationSubring K} {x : K} :
                                                      x g S g⁻¹ x S
                                                      theorem ValuationSubring.mem_inv_pointwise_smul_iff {K : Type u} [Field K] {G : Type u_1} [Group G] [MulSemiringAction G K] {g : G} {S : ValuationSubring K} {x : K} :
                                                      x g⁻¹ S g x S
                                                      @[simp]
                                                      def ValuationSubring.comap {K : Type u} [Field K] {L : Type u_1} [Field L] (A : ValuationSubring L) (f : K →+* L) :

                                                      The pullback of a valuation subring A along a ring homomorphism K →+* L.

                                                      Equations
                                                      • A.comap f = { toSubring := Subring.comap f A.toSubring, mem_or_inv_mem' := }
                                                      Instances For
                                                        @[simp]
                                                        theorem ValuationSubring.coe_comap {K : Type u} [Field K] {L : Type u_1} [Field L] (A : ValuationSubring L) (f : K →+* L) :
                                                        (A.comap f) = f ⁻¹' A
                                                        @[simp]
                                                        theorem ValuationSubring.mem_comap {K : Type u} [Field K] {L : Type u_1} [Field L] {A : ValuationSubring L} {f : K →+* L} {x : K} :
                                                        x A.comap f f x A
                                                        theorem ValuationSubring.comap_comap {K : Type u} [Field K] {L : Type u_1} {J : Type u_2} [Field L] [Field J] (A : ValuationSubring J) (g : L →+* J) (f : K →+* L) :
                                                        (A.comap g).comap f = A.comap (g.comp f)
                                                        theorem Valuation.mem_unitGroup_iff (K : Type u) [Field K] {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] (v : Valuation K Γ) (x : Kˣ) :
                                                        x v.valuationSubring.unitGroup v x = 1