mathlib3 documentation

ring_theory.valuation.valuation_subring

Valuation subrings of a field #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Projects #

The order structure on valuation_subring K.

source
structure valuation_subring (K : Type u_1) [field K] :
Type u_1

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

Instances for valuation_subring
source
@[protected, instance]
def valuation_subring.set_like {K : Type u_1} [field K] :
set_like (valuation_subring K) K
Equations
source
@[simp]
theorem valuation_subring.mem_carrier {K : Type u_1} [field K] (A : valuation_subring K) (x : K) :
x ∈ A.to_subring.carrier ↔ x ∈ A
source
@[simp]
theorem valuation_subring.mem_to_subring {K : Type u_1} [field K] (A : valuation_subring K) (x : K) :
x ∈ A.to_subring ↔ x ∈ A
source
@[ext]
theorem valuation_subring.ext {K : Type u_1} [field K] (A B : valuation_subring K) (h : ∀ (x : K), x ∈ A ↔ x ∈ B) :
A = B
source
theorem valuation_subring.zero_mem {K : Type u_1} [field K] (A : valuation_subring K) :
0 ∈ A
source
theorem valuation_subring.one_mem {K : Type u_1} [field K] (A : valuation_subring K) :
1 ∈ A
source
theorem valuation_subring.add_mem {K : Type u_1} [field K] (A : valuation_subring K) (x y : K) :
x ∈ A → y ∈ A → x + y ∈ A
source
theorem valuation_subring.mul_mem {K : Type u_1} [field K] (A : valuation_subring K) (x y : K) :
x ∈ A → y ∈ A → x * y ∈ A
source
theorem valuation_subring.neg_mem {K : Type u_1} [field K] (A : valuation_subring K) (x : K) :
x ∈ A → -x ∈ A
source
theorem valuation_subring.mem_or_inv_mem {K : Type u_1} [field K] (A : valuation_subring K) (x : K) :
x ∈ A ∨ x⁻¹ ∈ A
source
@[protected, instance]
def valuation_subring.subring_class {K : Type u_1} [field K] :
subring_class (valuation_subring K) K
source
theorem valuation_subring.to_subring_injective {K : Type u_1} [field K] :
function.injective valuation_subring.to_subring
source
@[protected, instance]
def valuation_subring.comm_ring {K : Type u_1} [field K] (A : valuation_subring K) :
comm_ring ↥A
Equations
source
@[protected, instance]
def valuation_subring.is_domain {K : Type u_1} [field K] (A : valuation_subring K) :
is_domain ↥A
source
@[protected, instance]
def valuation_subring.has_top {K : Type u_1} [field K] :
has_top (valuation_subring K)
Equations
source
theorem valuation_subring.mem_top {K : Type u_1} [field K] (x : K) :
x ∈ ⊤
source
theorem valuation_subring.le_top {K : Type u_1} [field K] (A : valuation_subring K) :
A ≤ ⊤
source
@[protected, instance]
def valuation_subring.order_top {K : Type u_1} [field K] :
order_top (valuation_subring K)
Equations
source
@[protected, instance]
def valuation_subring.inhabited {K : Type u_1} [field K] :
inhabited (valuation_subring K)
Equations
source
@[protected, instance]
def valuation_subring.valuation_ring {K : Type u_1} [field K] (A : valuation_subring K) :
valuation_ring ↥A
source
@[protected, instance]
def valuation_subring.algebra {K : Type u_1} [field K] (A : valuation_subring K) :
algebra ↥A K
Equations
source
@[simp]
theorem valuation_subring.algebra_map_apply {K : Type u_1} [field K] (A : valuation_subring K) (a : ↥A) :
⇑(algebra_map ↥A K) a = ↑a
source
@[protected, instance]
def valuation_subring.is_fraction_ring {K : Type u_1} [field K] (A : valuation_subring K) :
is_fraction_ring ↥A K
source
@[protected, instance]
noncomputable def valuation_subring.value_group.linear_ordered_comm_group_with_zero {K : Type u_1} [field K] (A : valuation_subring K) :
linear_ordered_comm_group_with_zero A.value_group
source
def valuation_subring.value_group {K : Type u_1} [field K] (A : valuation_subring K) :
Type u_1

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

Equations
Instances for valuation_subring.value_group
source
def valuation_subring.valuation {K : Type u_1} [field K] (A : valuation_subring K) :
valuation K A.value_group

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

Equations
source
@[protected, instance]
noncomputable def valuation_subring.inhabited_value_group {K : Type u_1} [field K] (A : valuation_subring K) :
inhabited A.value_group
Equations
source
theorem valuation_subring.valuation_le_one {K : Type u_1} [field K] (A : valuation_subring K) (a : ↥A) :
⇑(A.valuation) ↑a ≤ 1
source
theorem valuation_subring.mem_of_valuation_le_one {K : Type u_1} [field K] (A : valuation_subring K) (x : K) (h : ⇑(A.valuation) x ≤ 1) :
x ∈ A
source
theorem valuation_subring.valuation_le_one_iff {K : Type u_1} [field K] (A : valuation_subring K) (x : K) :
⇑(A.valuation) x ≤ 1 ↔ x ∈ A
source
theorem valuation_subring.valuation_eq_iff {K : Type u_1} [field K] (A : valuation_subring K) (x y : K) :
⇑(A.valuation) x = ⇑(A.valuation) y ↔ ∃ (a : (↥A)ˣ), ↑a * y = x
source
theorem valuation_subring.valuation_le_iff {K : Type u_1} [field K] (A : valuation_subring K) (x y : K) :
⇑(A.valuation) x ≤ ⇑(A.valuation) y ↔ ∃ (a : ↥A), ↑a * y = x
source
theorem valuation_subring.valuation_surjective {K : Type u_1} [field K] (A : valuation_subring K) :
function.surjective ⇑(A.valuation)
source
theorem valuation_subring.valuation_unit {K : Type u_1} [field K] (A : valuation_subring K) (a : (↥A)ˣ) :
⇑(A.valuation) ↑a = 1
source
theorem valuation_subring.valuation_eq_one_iff {K : Type u_1} [field K] (A : valuation_subring K) (a : ↥A) :
is_unit a ↔ ⇑(A.valuation) ↑a = 1
source
theorem valuation_subring.valuation_lt_one_or_eq_one {K : Type u_1} [field K] (A : valuation_subring K) (a : ↥A) :
⇑(A.valuation) ↑a < 1 ∨ ⇑(A.valuation) ↑a = 1
source
theorem valuation_subring.valuation_lt_one_iff {K : Type u_1} [field K] (A : valuation_subring K) (a : ↥A) :
a ∈ local_ring.maximal_ideal ↥A ↔ ⇑(A.valuation) ↑a < 1
source
def valuation_subring.of_subring {K : Type u_1} [field K] (R : subring K) (hR : ∀ (x : K), x ∈ R ∨ x⁻¹ ∈ R) :
valuation_subring K

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

Equations
source
@[simp]
theorem valuation_subring.mem_of_subring {K : Type u_1} [field K] (R : subring K) (hR : ∀ (x : K), x ∈ R ∨ x⁻¹ ∈ R) (x : K) :
x ∈ valuation_subring.of_subring R hR ↔ x ∈ R
source
def valuation_subring.of_le {K : Type u_1} [field K] (R : valuation_subring K) (S : subring K) (h : R.to_subring ≤ S) :
valuation_subring K

An overring of a valuation ring is a valuation ring.

Equations
source
@[protected, instance]
def valuation_subring.semilattice_sup {K : Type u_1} [field K] :
semilattice_sup (valuation_subring K)
Equations
source
def valuation_subring.inclusion {K : Type u_1} [field K] (R S : valuation_subring K) (h : R ≤ S) :
↥R →+* ↥S

The ring homomorphism induced by the partial order.

Equations
source
def valuation_subring.subtype {K : Type u_1} [field K] (R : valuation_subring K) :
↥R →+* K

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

Equations
source
def valuation_subring.map_of_le {K : Type u_1} [field K] (R S : valuation_subring K) (h : R ≤ S) :
R.value_group →*₀ S.value_group

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

Equations
source
theorem valuation_subring.monotone_map_of_le {K : Type u_1} [field K] (R S : valuation_subring K) (h : R ≤ S) :
monotone ⇑(R.map_of_le S h)
source
@[simp]
theorem valuation_subring.map_of_le_comp_valuation {K : Type u_1} [field K] (R S : valuation_subring K) (h : R ≤ S) :
⇑(R.map_of_le S h) ∘ ⇑(R.valuation) = ⇑(S.valuation)
source
@[simp]
theorem valuation_subring.map_of_le_valuation_apply {K : Type u_1} [field K] (R S : valuation_subring K) (h : R ≤ S) (x : K) :
⇑(R.map_of_le S h) (⇑(R.valuation) x) = ⇑(S.valuation) x
source
def valuation_subring.ideal_of_le {K : Type u_1} [field K] (R S : valuation_subring K) (h : R ≤ S) :
ideal ↥R

The ideal corresponding to a coarsening of a valuation ring.

Equations
Instances for valuation_subring.ideal_of_le
source
@[protected, instance]
def valuation_subring.prime_ideal_of_le {K : Type u_1} [field K] (R S : valuation_subring K) (h : R ≤ S) :
(R.ideal_of_le S h).is_prime
source
noncomputable def valuation_subring.of_prime {K : Type u_1} [field K] (A : valuation_subring K) (P : ideal ↥A) [P.is_prime] :
valuation_subring K

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

Equations
Instances for ↥valuation_subring.of_prime
source
@[protected, instance]
noncomputable def valuation_subring.of_prime_algebra {K : Type u_1} [field K] (A : valuation_subring K) (P : ideal ↥A) [P.is_prime] :
algebra ↥A ↥(A.of_prime P)
Equations
source
@[protected, instance]
def valuation_subring.of_prime_scalar_tower {K : Type u_1} [field K] (A : valuation_subring K) (P : ideal ↥A) [P.is_prime] :
is_scalar_tower ↥A ↥(A.of_prime P) K
source
@[protected, instance]
def valuation_subring.of_prime_localization {K : Type u_1} [field K] (A : valuation_subring K) (P : ideal ↥A) [P.is_prime] :
is_localization.at_prime ↥(A.of_prime P) P
source
theorem valuation_subring.le_of_prime {K : Type u_1} [field K] (A : valuation_subring K) (P : ideal ↥A) [P.is_prime] :
A ≤ A.of_prime P
source
theorem valuation_subring.of_prime_valuation_eq_one_iff_mem_prime_compl {K : Type u_1} [field K] (A : valuation_subring K) (P : ideal ↥A) [P.is_prime] (x : ↥A) :
⇑((A.of_prime P).valuation) ↑x = 1 ↔ x ∈ P.prime_compl
source
@[simp]
theorem valuation_subring.ideal_of_le_of_prime {K : Type u_1} [field K] (A : valuation_subring K) (P : ideal ↥A) [P.is_prime] :
A.ideal_of_le (A.of_prime P) _ = P
source
@[simp]
theorem valuation_subring.of_prime_ideal_of_le {K : Type u_1} [field K] (R S : valuation_subring K) (h : R ≤ S) :
R.of_prime (R.ideal_of_le S h) = S
source
theorem valuation_subring.of_prime_le_of_le {K : Type u_1} [field K] (A : valuation_subring K) (P Q : ideal ↥A) [P.is_prime] [Q.is_prime] (h : P ≤ Q) :
A.of_prime Q ≤ A.of_prime P
source
theorem valuation_subring.ideal_of_le_le_of_le {K : Type u_1} [field K] (A R S : valuation_subring K) (hR : A ≤ R) (hS : A ≤ S) (h : R ≤ S) :
A.ideal_of_le S hS ≤ A.ideal_of_le R hR
source
noncomputable def valuation_subring.prime_spectrum_equiv {K : Type u_1} [field K] (A : valuation_subring K) :
prime_spectrum ↥A ≃ ↥{S : valuation_subring K | A ≤ S}

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

Equations
source
@[simp]
theorem valuation_subring.prime_spectrum_equiv_apply_coe {K : Type u_1} [field K] (A : valuation_subring K) (P : prime_spectrum ↥A) :
↑(⇑(A.prime_spectrum_equiv) P) = A.of_prime P.as_ideal
source
@[simp]
theorem valuation_subring.prime_spectrum_equiv_symm_apply_as_ideal {K : Type u_1} [field K] (A : valuation_subring K) (S : ↥{S : valuation_subring K | A ≤ S}) :
(⇑(A.prime_spectrum_equiv.symm) S).as_ideal = A.ideal_of_le ↑S _
source
@[simp]
theorem valuation_subring.prime_spectrum_order_equiv_apply {K : Type u_1} [field K] (A : valuation_subring K) (ᾰ : prime_spectrum ↥A) :
⇑(A.prime_spectrum_order_equiv) ᾰ = A.prime_spectrum_equiv.to_fun ᾰ
source
@[simp]
theorem valuation_subring.prime_spectrum_order_equiv_symm_apply {K : Type u_1} [field K] (A : valuation_subring K) (ᾰ : ↥{S : valuation_subring K | A ≤ S}) :
⇑(rel_iso.symm A.prime_spectrum_order_equiv) ᾰ = A.prime_spectrum_equiv.inv_fun ᾰ
source
noncomputable def valuation_subring.prime_spectrum_order_equiv {K : Type u_1} [field K] (A : valuation_subring K) :
(prime_spectrum ↥A)ᵒᵈ ≃o ↥{S : valuation_subring K | A ≤ S}

An ordered variant of prime_spectrum_equiv.

Equations
source
@[protected, instance]
noncomputable def valuation_subring.linear_order_overring {K : Type u_1} [field K] (A : valuation_subring K) :
linear_order ↥{S : valuation_subring K | A ≤ S}
Equations
source
def valuation.valuation_subring {K : Type u_1} [field K] {Γ : Type u_2} [linear_ordered_comm_group_with_zero Γ] (v : valuation K Γ) :
valuation_subring K

The valuation subring associated to a valuation.

Equations
source
@[simp]
theorem valuation.mem_valuation_subring_iff {K : Type u_1} [field K] {Γ : Type u_2} [linear_ordered_comm_group_with_zero Γ] (v : valuation K Γ) (x : K) :
x ∈ v.valuation_subring ↔ ⇑v x ≤ 1
source
theorem valuation.is_equiv_iff_valuation_subring {K : Type u_1} [field K] {Γ₁ : Type u_3} {Γ₂ : Type u_4} [linear_ordered_comm_group_with_zero Γ₁] [linear_ordered_comm_group_with_zero Γ₂] (v₁ : valuation K Γ₁) (v₂ : valuation K Γ₂) :
v₁.is_equiv v₂ ↔ v₁.valuation_subring = v₂.valuation_subring
source
theorem valuation.is_equiv_valuation_valuation_subring {K : Type u_1} [field K] {Γ : Type u_2} [linear_ordered_comm_group_with_zero Γ] (v : valuation K Γ) :
v.is_equiv v.valuation_subring.valuation
source
@[simp]
theorem valuation_subring.valuation_subring_valuation {K : Type u_1} [field K] (A : valuation_subring K) :
A.valuation.valuation_subring = A
source
noncomputable def valuation_subring.unit_group {K : Type u_1} [field K] (A : valuation_subring K) :
subgroup Kˣ

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

Equations
source
@[simp]
theorem valuation_subring.mem_unit_group_iff {K : Type u_1} [field K] (A : valuation_subring K) (x : Kˣ) :
x ∈ A.unit_group ↔ ⇑(A.valuation) ↑x = 1
source
noncomputable def valuation_subring.unit_group_mul_equiv {K : Type u_1} [field K] (A : valuation_subring K) :
↥(A.unit_group) ≃* (↥A)ˣ

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

Equations
source
@[simp]
theorem valuation_subring.coe_unit_group_mul_equiv_apply {K : Type u_1} [field K] (A : valuation_subring K) (a : ↥(A.unit_group)) :
↑(⇑(A.unit_group_mul_equiv) a) = ↑a
source
@[simp]
theorem valuation_subring.coe_unit_group_mul_equiv_symm_apply {K : Type u_1} [field K] (A : valuation_subring K) (a : (↥A)ˣ) :
↑(⇑(A.unit_group_mul_equiv.symm) a) = ↑a
source
theorem valuation_subring.unit_group_le_unit_group {K : Type u_1} [field K] {A B : valuation_subring K} :
A.unit_group ≤ B.unit_group ↔ A ≤ B
source
theorem valuation_subring.unit_group_injective {K : Type u_1} [field K] :
function.injective valuation_subring.unit_group
source
theorem valuation_subring.eq_iff_unit_group {K : Type u_1} [field K] {A B : valuation_subring K} :
A = B ↔ A.unit_group = B.unit_group
source
noncomputable def valuation_subring.unit_group_order_embedding {K : Type u_1} [field K] :
valuation_subring K ↪o subgroup Kˣ

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

Equations
source
theorem valuation_subring.unit_group_strict_mono {K : Type u_1} [field K] :
strict_mono valuation_subring.unit_group
source
def valuation_subring.nonunits {K : Type u_1} [field K] (A : valuation_subring K) :
subsemigroup K

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

Equations
source
theorem valuation_subring.mem_nonunits_iff {K : Type u_1} [field K] (A : valuation_subring K) {x : K} :
x ∈ A.nonunits ↔ ⇑(A.valuation) x < 1
source
theorem valuation_subring.nonunits_le_nonunits {K : Type u_1} [field K] {A B : valuation_subring K} :
B.nonunits ≤ A.nonunits ↔ A ≤ B
source
theorem valuation_subring.nonunits_injective {K : Type u_1} [field K] :
function.injective valuation_subring.nonunits
source
theorem valuation_subring.nonunits_inj {K : Type u_1} [field K] {A B : valuation_subring K} :
A.nonunits = B.nonunits ↔ A = B
source
def valuation_subring.nonunits_order_embedding {K : Type u_1} [field K] :
valuation_subring K ↪o (subsemigroup K)ᵒᵈ

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

Equations
source
theorem valuation_subring.coe_mem_nonunits_iff {K : Type u_1} [field K] {A : valuation_subring K} {a : ↥A} :
↑a ∈ A.nonunits ↔ a ∈ local_ring.maximal_ideal ↥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_maximal_ideal, which gets rid of the coercion to K, at the expense of a more complicated right hand side.

source
theorem valuation_subring.nonunits_le {K : Type u_1} [field K] {A : valuation_subring K} :
A.nonunits ≤ A.to_subring.to_submonoid.to_subsemigroup
source
theorem valuation_subring.nonunits_subset {K : Type u_1} [field K] {A : valuation_subring K} :
↑(A.nonunits) ⊆ ↑A
source
theorem valuation_subring.mem_nonunits_iff_exists_mem_maximal_ideal {K : Type u_1} [field K] {A : valuation_subring K} {a : K} :
a ∈ A.nonunits ↔ ∃ (ha : a ∈ A), ⟨a, ha⟩ ∈ local_ring.maximal_ideal ↥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.

source
theorem valuation_subring.image_maximal_ideal {K : Type u_1} [field K] {A : valuation_subring K} :
coe '' ↑(local_ring.maximal_ideal ↥A) = ↑(A.nonunits)

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

source
def valuation_subring.principal_unit_group {K : Type u_1} [field K] (A : valuation_subring K) :
subgroup Kˣ

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

Equations
source
theorem valuation_subring.principal_units_le_units {K : Type u_1} [field K] (A : valuation_subring K) :
A.principal_unit_group ≤ A.unit_group
source
theorem valuation_subring.mem_principal_unit_group_iff {K : Type u_1} [field K] (A : valuation_subring K) (x : Kˣ) :
x ∈ A.principal_unit_group ↔ ⇑(A.valuation) (↑x - 1) < 1
source
theorem valuation_subring.principal_unit_group_le_principal_unit_group {K : Type u_1} [field K] {A B : valuation_subring K} :
B.principal_unit_group ≤ A.principal_unit_group ↔ A ≤ B
source
theorem valuation_subring.principal_unit_group_injective {K : Type u_1} [field K] :
function.injective valuation_subring.principal_unit_group
source
theorem valuation_subring.eq_iff_principal_unit_group {K : Type u_1} [field K] {A B : valuation_subring K} :
A = B ↔ A.principal_unit_group = B.principal_unit_group
source
def valuation_subring.principal_unit_group_order_embedding {K : Type u_1} [field K] :
valuation_subring K ↪o (subgroup Kˣ)ᵒᵈ

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

Equations
source
theorem valuation_subring.coe_mem_principal_unit_group_iff {K : Type u_1} [field K] (A : valuation_subring K) {x : ↥(A.unit_group)} :
↑x ∈ A.principal_unit_group ↔ ⇑(A.unit_group_mul_equiv) x ∈ (units.map (local_ring.residue ↥A).to_monoid_hom).ker
source
noncomputable def valuation_subring.principal_unit_group_equiv {K : Type u_1} [field K] (A : valuation_subring K) :
↥(A.principal_unit_group) ≃* ↥((units.map (local_ring.residue ↥A).to_monoid_hom).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
source
@[simp]
theorem valuation_subring.principal_unit_group_equiv_apply {K : Type u_1} [field K] (A : valuation_subring K) (a : ↥(A.principal_unit_group)) :
↑(⇑(A.principal_unit_group_equiv) a) = ↑a
source
@[simp]
theorem valuation_subring.principal_unit_group_symm_apply {K : Type u_1} [field K] (A : valuation_subring K) (a : ↥((units.map (local_ring.residue ↥A).to_monoid_hom).ker)) :
↑(⇑(A.principal_unit_group_equiv.symm) a) = ↑a
source
noncomputable def valuation_subring.unit_group_to_residue_field_units {K : Type u_1} [field K] (A : valuation_subring K) :
↥(A.unit_group) →* (local_ring.residue_field ↥A)ˣ

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

Equations
source
@[simp]
theorem valuation_subring.coe_unit_group_to_residue_field_units_apply {K : Type u_1} [field K] (A : valuation_subring K) (x : ↥(A.unit_group)) :
↑(⇑(A.unit_group_to_residue_field_units) x) = ⇑(ideal.quotient.mk (local_ring.maximal_ideal ↥A)) ↑(⇑(A.unit_group_mul_equiv) x)
source
theorem valuation_subring.ker_unit_group_to_residue_field_units {K : Type u_1} [field K] (A : valuation_subring K) :
A.unit_group_to_residue_field_units.ker = subgroup.comap A.unit_group.subtype A.principal_unit_group
source
theorem valuation_subring.surjective_unit_group_to_residue_field_units {K : Type u_1} [field K] (A : valuation_subring K) :
function.surjective ⇑(A.unit_group_to_residue_field_units)
source
noncomputable def valuation_subring.units_mod_principal_units_equiv_residue_field_units {K : Type u_1} [field K] (A : valuation_subring K) :
↥(A.unit_group) ⧸ subgroup.comap A.unit_group.subtype A.principal_unit_group ≃* (local_ring.residue_field ↥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
source
@[simp]
theorem valuation_subring.units_mod_principal_units_equiv_residue_field_units_comp_quotient_group_mk {K : Type u_1} [field K] (A : valuation_subring K) :
A.units_mod_principal_units_equiv_residue_field_units.to_monoid_hom.comp (quotient_group.mk' (subgroup.comap A.unit_group.subtype A.principal_unit_group)) = A.unit_group_to_residue_field_units
source
@[simp]
theorem valuation_subring.units_mod_principal_units_equiv_residue_field_units_comp_quotient_group_mk_apply {K : Type u_1} [field K] (A : valuation_subring K) (x : ↥(A.unit_group)) :
⇑(A.units_mod_principal_units_equiv_residue_field_units.to_monoid_hom) (quotient_group.mk x) = ⇑(A.unit_group_to_residue_field_units) x

Pointwise actions #

This transfers the action from subring.pointwise_mul_action, 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 ring_theory/subring/pointwise.lean; try to keep these in sync.

source
def valuation_subring.pointwise_has_smul {K : Type u_1} [field K] {G : Type u_2} [group G] [mul_semiring_action G K] :
has_smul G (valuation_subring K)

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
source
@[simp]
theorem valuation_subring.coe_pointwise_smul {K : Type u_1} [field K] {G : Type u_2} [group G] [mul_semiring_action G K] (g : G) (S : valuation_subring K) :
↑(g • S) = g • ↑S
source
@[simp]
theorem valuation_subring.pointwise_smul_to_subring {K : Type u_1} [field K] {G : Type u_2} [group G] [mul_semiring_action G K] (g : G) (S : valuation_subring K) :
(g • S).to_subring = g • S.to_subring
source
def valuation_subring.pointwise_mul_action {K : Type u_1} [field K] {G : Type u_2} [group G] [mul_semiring_action G K] :
mul_action G (valuation_subring K)

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 valuation_subring.pointwise_has_smul.

Equations
source
theorem valuation_subring.smul_mem_pointwise_smul {K : Type u_1} [field K] {G : Type u_2} [group G] [mul_semiring_action G K] (g : G) (x : K) (S : valuation_subring K) :
x ∈ S → g • x ∈ g • S
source
theorem valuation_subring.mem_smul_pointwise_iff_exists {K : Type u_1} [field K] {G : Type u_2} [group G] [mul_semiring_action G K] (g : G) (x : K) (S : valuation_subring K) :
x ∈ g • S ↔ ∃ (s : K), s ∈ S ∧ g • s = x
source
@[protected, instance]
def valuation_subring.pointwise_central_scalar {K : Type u_1} [field K] {G : Type u_2} [group G] [mul_semiring_action G K] [mul_semiring_action Gᵐᵒᵖ K] [is_central_scalar G K] :
is_central_scalar G (valuation_subring K)
source
@[simp]
theorem valuation_subring.smul_mem_pointwise_smul_iff {K : Type u_1} [field K] {G : Type u_2} [group G] [mul_semiring_action G K] {g : G} {S : valuation_subring K} {x : K} :
g • x ∈ g • S ↔ x ∈ S
source
theorem valuation_subring.mem_pointwise_smul_iff_inv_smul_mem {K : Type u_1} [field K] {G : Type u_2} [group G] [mul_semiring_action G K] {g : G} {S : valuation_subring K} {x : K} :
x ∈ g • S ↔ g⁻¹ • x ∈ S
source
theorem valuation_subring.mem_inv_pointwise_smul_iff {K : Type u_1} [field K] {G : Type u_2} [group G] [mul_semiring_action G K] {g : G} {S : valuation_subring K} {x : K} :
x ∈ g⁻¹ • S ↔ g • x ∈ S
source
@[simp]
theorem valuation_subring.pointwise_smul_le_pointwise_smul_iff {K : Type u_1} [field K] {G : Type u_2} [group G] [mul_semiring_action G K] {g : G} {S T : valuation_subring K} :
g • S ≤ g • T ↔ S ≤ T
source
theorem valuation_subring.pointwise_smul_subset_iff {K : Type u_1} [field K] {G : Type u_2} [group G] [mul_semiring_action G K] {g : G} {S T : valuation_subring K} :
g • S ≤ T ↔ S ≤ g⁻¹ • T
source
theorem valuation_subring.subset_pointwise_smul_iff {K : Type u_1} [field K] {G : Type u_2} [group G] [mul_semiring_action G K] {g : G} {S T : valuation_subring K} :
S ≤ g • T ↔ g⁻¹ • S ≤ T
source
def valuation_subring.comap {K : Type u_1} [field K] {L : Type u_2} [field L] (A : valuation_subring L) (f : K →+* L) :
valuation_subring K

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

Equations
source
@[simp]
theorem valuation_subring.coe_comap {K : Type u_1} [field K] {L : Type u_2} [field L] (A : valuation_subring L) (f : K →+* L) :
↑(A.comap f) = ⇑f ⁻¹' ↑A
source
@[simp]
theorem valuation_subring.mem_comap {K : Type u_1} [field K] {L : Type u_2} [field L] {A : valuation_subring L} {f : K →+* L} {x : K} :
x ∈ A.comap f ↔ ⇑f x ∈ A
source
theorem valuation_subring.comap_comap {K : Type u_1} [field K] {L : Type u_2} {J : Type u_3} [field L] [field J] (A : valuation_subring J) (g : L →+* J) (f : K →+* L) :
(A.comap g).comap f = A.comap (g.comp f)
source
@[simp]
theorem valuation.mem_unit_group_iff (K : Type u_1) [field K] {Γ : Type u_2} [linear_ordered_comm_group_with_zero Γ] (v : valuation K Γ) (x : Kˣ) :
x ∈ v.valuation_subring.unit_group ↔ ⇑v ↑x = 1