NYLL
Module

ResidueField.lean

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.ResidueField
28 declarations indexed from sourceView source ↗

Module documentation

Residue-field API for local maps

This file adds reusable local-ring residue-field lemmas that are used by the Henselian and unramified parts of the DVF library. It keeps mathlib's IsLocalRing.ResidueField.map and IsLocalRing.residue as the primary objects.

Imports1
  • Mathlib.RingTheory.LocalRing.ResidueField.Basic
Imported by7

Declarations

theorem

residue_eq_residue_iff_sub_mem_maximalIdeal

L34 ↗
ValuationTheory.DiscreteValuationField.ResidueField.residue_eq_residue_iff_sub_mem_maximalIdeal
Documentation

Equality in the residue field is equality modulo the maximal ideal.

Source context 8 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
namespace ResidueField
variable {R : Type u} {S : Type v} {T : Type w}
section LocalRing
variable [CommRing R] [IsLocalRing R]
Lean source · statement
theorem residue_eq_residue_iff_sub_mem_maximalIdeal (x y : R) :
    IsLocalRing.residue R x = IsLocalRing.residue R y ↔
      x - y ∈ IsLocalRing.maximalIdeal R
theorem

residue_sub_eq_zero_iff

L41 ↗
ValuationTheory.DiscreteValuationField.ResidueField.residue_sub_eq_zero_iff
Documentation

The residue of a difference is zero exactly when the two residues are equal.

Source context 8 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
namespace ResidueField
variable {R : Type u} {S : Type v} {T : Type w}
section LocalRing
variable [CommRing R] [IsLocalRing R]
Lean source · statement
theorem residue_sub_eq_zero_iff (x y : R) :
    IsLocalRing.residue R (x - y) = 0 ↔
      IsLocalRing.residue R x = IsLocalRing.residue R y
theorem

lift_eq_of_comp_residue_eq

L56 ↗
ValuationTheory.DiscreteValuationField.ResidueField.lift_eq_of_comp_residue_eq
Documentation

The map from the residue field induced by a local homomorphism to a field is uniquely characterized by its composite with the residue map.

Source context 9 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
namespace ResidueField
variable {R : Type u} {S : Type v} {T : Type w}
section FieldLift
variable [CommRing R] [IsLocalRing R] [Field S]
variable (f : R →+* S) [IsLocalHom f]
Lean source · statement
theorem lift_eq_of_comp_residue_eq
    (g : IsLocalRing.ResidueField R →+* S)
    (hg : g.comp (IsLocalRing.residue R) = f) :
    g = IsLocalRing.ResidueField.lift f
theorem

comap_maximalIdeal_eq

L74 ↗
ValuationTheory.DiscreteValuationField.ResidueField.comap_maximalIdeal_eq
Documentation

A local homomorphism pulls back the target maximal ideal to the source maximal ideal.

Source context 9 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
namespace ResidueField
variable {R : Type u} {S : Type v} {T : Type w}
section LocalHom
variable [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S]
variable (f : R →+* S) [IsLocalHom f]
Lean source · statement
theorem comap_maximalIdeal_eq :
    (IsLocalRing.maximalIdeal S).comap f = IsLocalRing.maximalIdeal R
theorem

map_injective

L79 ↗
ValuationTheory.DiscreteValuationField.ResidueField.map_injective
Documentation

A local homomorphism induces an injective map on residue fields.

Source context 9 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
namespace ResidueField
variable {R : Type u} {S : Type v} {T : Type w}
section LocalHom
variable [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S]
variable (f : R →+* S) [IsLocalHom f]
Lean source · statement
theorem map_injective :
    Function.Injective (IsLocalRing.ResidueField.map f)
theorem

map_eq_zero_iff

L96 ↗
ValuationTheory.DiscreteValuationField.ResidueField.map_eq_zero_iff
Documentation

A residue-field map induced by a local homomorphism has trivial kernel.

Source context 9 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
namespace ResidueField
variable {R : Type u} {S : Type v} {T : Type w}
section LocalHom
variable [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S]
variable (f : R →+* S) [IsLocalHom f]
Lean source · statement
theorem map_eq_zero_iff (x : IsLocalRing.ResidueField R) :
    IsLocalRing.ResidueField.map f x = 0 ↔ x = 0
theorem

map_eq_map_iff

L106 ↗
ValuationTheory.DiscreteValuationField.ResidueField.map_eq_map_iff
Documentation

Equality can be checked after applying the residue-field map induced by a local homomorphism.

Source context 9 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
namespace ResidueField
variable {R : Type u} {S : Type v} {T : Type w}
section LocalHom
variable [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S]
variable (f : R →+* S) [IsLocalHom f]
Lean source · statement
theorem map_eq_map_iff (x y : IsLocalRing.ResidueField R) :
    IsLocalRing.ResidueField.map f x = IsLocalRing.ResidueField.map f y ↔
      x = y
def

ringEquivOfSurjective

L117 ↗
ValuationTheory.DiscreteValuationField.ResidueField.ringEquivOfSurjective
Documentation

The residue-field isomorphism induced by a surjective residue-field map coming from a local homomorphism.

Source context 9 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
namespace ResidueField
variable {R : Type u} {S : Type v} {T : Type w}
section LocalHom
variable [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S]
variable (f : R →+* S) [IsLocalHom f]
Lean source · statement
def ringEquivOfSurjective
    (hsurj : Function.Surjective (IsLocalRing.ResidueField.map f)) :
    IsLocalRing.ResidueField R ≃+* IsLocalRing.ResidueField S
theorem

ringEquivOfSurjective_apply

L125 ↗
ValuationTheory.DiscreteValuationField.ResidueField.ringEquivOfSurjective_apply
Documentation

The residue-ring equivalence induced by a surjective map evaluates by that map.

Source context 9 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
namespace ResidueField
variable {R : Type u} {S : Type v} {T : Type w}
section LocalHom
variable [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S]
variable (f : R →+* S) [IsLocalHom f]
Lean source · statement
theorem ringEquivOfSurjective_apply
    (hsurj : Function.Surjective (IsLocalRing.ResidueField.map f))
    (x : IsLocalRing.ResidueField R) :
    ringEquivOfSurjective f hsurj x =
      IsLocalRing.ResidueField.map f x
theorem

residue_map_eq_zero_iff

L133 ↗
ValuationTheory.DiscreteValuationField.ResidueField.residue_map_eq_zero_iff
Documentation

A local homomorphism preserves and reflects zero residues.

Source context 9 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
namespace ResidueField
variable {R : Type u} {S : Type v} {T : Type w}
section LocalHom
variable [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S]
variable (f : R →+* S) [IsLocalHom f]
Lean source · statement
theorem residue_map_eq_zero_iff (x : R) :
    IsLocalRing.residue S (f x) = 0 ↔ IsLocalRing.residue R x = 0
theorem

residue_map_eq_iff

L139 ↗
ValuationTheory.DiscreteValuationField.ResidueField.residue_map_eq_iff
Documentation

A local homomorphism preserves and reflects equality of residues.

Source context 9 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
namespace ResidueField
variable {R : Type u} {S : Type v} {T : Type w}
section LocalHom
variable [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S]
variable (f : R →+* S) [IsLocalHom f]
Lean source · statement
theorem residue_map_eq_iff (x y : R) :
    IsLocalRing.residue S (f x) = IsLocalRing.residue S (f y) ↔
      IsLocalRing.residue R x = IsLocalRing.residue R y
theorem

map_residue_eq_residue_iff_sub_mem_maximalIdeal

L147 ↗
ValuationTheory.DiscreteValuationField.ResidueField.map_residue_eq_residue_iff_sub_mem_maximalIdeal
Documentation

A mapped residue class equals a target residue class exactly when their chosen representatives are congruent modulo the target maximal ideal.

Source context 9 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
namespace ResidueField
variable {R : Type u} {S : Type v} {T : Type w}
section LocalHom
variable [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S]
variable (f : R →+* S) [IsLocalHom f]
Lean source · statement
theorem map_residue_eq_residue_iff_sub_mem_maximalIdeal (x : R) (y : S) :
    IsLocalRing.ResidueField.map f (IsLocalRing.residue R x) =
        IsLocalRing.residue S y ↔
      f x - y ∈ IsLocalRing.maximalIdeal S
theorem

residue_eq_map_residue_iff_sub_mem_maximalIdeal

L156 ↗
ValuationTheory.DiscreteValuationField.ResidueField.residue_eq_map_residue_iff_sub_mem_maximalIdeal
Documentation

Target residue equality with a mapped residue class, in the opposite orientation, is also equality modulo the target maximal ideal.

Source context 9 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
namespace ResidueField
variable {R : Type u} {S : Type v} {T : Type w}
section LocalHom
variable [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S]
variable (f : R →+* S) [IsLocalHom f]
Lean source · statement
theorem residue_eq_map_residue_iff_sub_mem_maximalIdeal (y : S) (x : R) :
    IsLocalRing.residue S y =
        IsLocalRing.ResidueField.map f (IsLocalRing.residue R x) ↔
      y - f x ∈ IsLocalRing.maximalIdeal S
theorem

algebraMap_eq_map_algebraMap

L172 ↗
ValuationTheory.DiscreteValuationField.ResidueField.algebraMap_eq_map_algebraMap
Documentation

For a local algebra map, mathlib's residue-field algebra map agrees with the residue-field map induced by the structure homomorphism.

Source context 9 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
namespace ResidueField
variable {R : Type u} {S : Type v} {T : Type w}
section Algebra
variable [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S]
variable [Algebra R S] [IsLocalHom (algebraMap R S)]
Lean source · statement
theorem algebraMap_eq_map_algebraMap :
    algebraMap (IsLocalRing.ResidueField R)
        (IsLocalRing.ResidueField S) =
      IsLocalRing.ResidueField.map (algebraMap R S)
theorem

map_algebraMap_injective

L182 ↗
ValuationTheory.DiscreteValuationField.ResidueField.map_algebraMap_injective
Documentation

The residue-field map induced by a local algebra map is injective.

Source context 9 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
namespace ResidueField
variable {R : Type u} {S : Type v} {T : Type w}
section Algebra
variable [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S]
variable [Algebra R S] [IsLocalHom (algebraMap R S)]
Lean source · statement
theorem map_algebraMap_injective :
    Function.Injective
      (IsLocalRing.ResidueField.map (algebraMap R S))
theorem

map_algebraMap_eq_zero_iff

L189 ↗
ValuationTheory.DiscreteValuationField.ResidueField.map_algebraMap_eq_zero_iff
Documentation

The residue-field map induced by a local algebra map has trivial kernel.

Source context 9 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
namespace ResidueField
variable {R : Type u} {S : Type v} {T : Type w}
section Algebra
variable [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S]
variable [Algebra R S] [IsLocalHom (algebraMap R S)]
Lean source · statement
theorem map_algebraMap_eq_zero_iff (x : IsLocalRing.ResidueField R) :
    IsLocalRing.ResidueField.map (algebraMap R S) x = 0 ↔ x = 0
theorem

residue_algebraMap_eq_zero_iff

L194 ↗
ValuationTheory.DiscreteValuationField.ResidueField.residue_algebraMap_eq_zero_iff
Documentation

A local algebra map preserves and reflects zero residues.

Source context 9 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
namespace ResidueField
variable {R : Type u} {S : Type v} {T : Type w}
section Algebra
variable [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S]
variable [Algebra R S] [IsLocalHom (algebraMap R S)]
Lean source · statement
theorem residue_algebraMap_eq_zero_iff (x : R) :
    IsLocalRing.residue S (algebraMap R S x) = 0 ↔
      IsLocalRing.residue R x = 0
theorem

residue_algebraMap_eq_iff

L200 ↗
ValuationTheory.DiscreteValuationField.ResidueField.residue_algebraMap_eq_iff
Documentation

A local algebra map preserves and reflects equality of residues.

Source context 9 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
namespace ResidueField
variable {R : Type u} {S : Type v} {T : Type w}
section Algebra
variable [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S]
variable [Algebra R S] [IsLocalHom (algebraMap R S)]
Lean source · statement
theorem residue_algebraMap_eq_iff (x y : R) :
    IsLocalRing.residue S (algebraMap R S x) =
        IsLocalRing.residue S (algebraMap R S y) ↔
      IsLocalRing.residue R x = IsLocalRing.residue R y
theorem

algebraMap_residue_eq_residue_iff_sub_mem_maximalIdeal

L209 ↗
ValuationTheory.DiscreteValuationField.ResidueField.algebraMap_residue_eq_residue_iff_sub_mem_maximalIdeal
Documentation

The residue-field algebra map sends the residue of x to the residue of y exactly when algebraMap R S x and y are congruent modulo the target maximal ideal.

Source context 9 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
namespace ResidueField
variable {R : Type u} {S : Type v} {T : Type w}
section Algebra
variable [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S]
variable [Algebra R S] [IsLocalHom (algebraMap R S)]
Lean source · statement
theorem algebraMap_residue_eq_residue_iff_sub_mem_maximalIdeal
    (x : R) (y : S) :
    algebraMap (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField S)
        (IsLocalRing.residue R x) = IsLocalRing.residue S y ↔
      algebraMap R S x - y ∈ IsLocalRing.maximalIdeal S
def

algEquivOfAlgEquiv

L228 ↗
ValuationTheory.DiscreteValuationField.ResidueField.algEquivOfAlgEquiv
Documentation

A local algebra equivalence induces an algebra equivalence on residue fields over the base residue field.

Source context 11 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
namespace ResidueField
variable {R : Type u} {S : Type v} {T : Type w}
section AlgEquiv
variable [CommRing T] [IsLocalRing T]
variable [CommRing R] [IsLocalRing R] [Algebra T R]
variable [CommRing S] [IsLocalRing S] [Algebra T S]
variable [IsLocalHom (algebraMap T R)] [IsLocalHom (algebraMap T S)]
Lean source · statement
def algEquivOfAlgEquiv
    (e : R ≃ₐ[T] S) :
    IsLocalRing.ResidueField R ≃ₐ[IsLocalRing.ResidueField T]
      IsLocalRing.ResidueField S
theorem

algEquivOfAlgEquiv_apply

L247 ↗
ValuationTheory.DiscreteValuationField.ResidueField.algEquivOfAlgEquiv_apply
Documentation

The residue-field equivalence induced by an algebra equivalence acts through residue representatives.

Source context 11 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
namespace ResidueField
variable {R : Type u} {S : Type v} {T : Type w}
section AlgEquiv
variable [CommRing T] [IsLocalRing T]
variable [CommRing R] [IsLocalRing R] [Algebra T R]
variable [CommRing S] [IsLocalRing S] [Algebra T S]
variable [IsLocalHom (algebraMap T R)] [IsLocalHom (algebraMap T S)]
Lean source · statement
theorem algEquivOfAlgEquiv_apply
    (e : R ≃ₐ[T] S)
    (x : IsLocalRing.ResidueField R) :
    algEquivOfAlgEquiv e x =
      IsLocalRing.ResidueField.map e.toRingEquiv x
theorem

algEquivOfAlgEquiv_apply_eq_mapEquiv

L255 ↗
ValuationTheory.DiscreteValuationField.ResidueField.algEquivOfAlgEquiv_apply_eq_mapEquiv
Documentation

The induced residue algebra equivalence agrees with the canonical quotient-map equivalence.

Source context 11 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
namespace ResidueField
variable {R : Type u} {S : Type v} {T : Type w}
section AlgEquiv
variable [CommRing T] [IsLocalRing T]
variable [CommRing R] [IsLocalRing R] [Algebra T R]
variable [CommRing S] [IsLocalRing S] [Algebra T S]
variable [IsLocalHom (algebraMap T R)] [IsLocalHom (algebraMap T S)]
Lean source · statement
theorem algEquivOfAlgEquiv_apply_eq_mapEquiv
    (e : R ≃ₐ[T] S)
    (x : IsLocalRing.ResidueField R) :
    algEquivOfAlgEquiv e x =
      IsLocalRing.ResidueField.mapEquiv e.toRingEquiv x
theorem

algEquivOfAlgEquiv_symm_apply_eq_mapEquiv

L263 ↗
ValuationTheory.DiscreteValuationField.ResidueField.algEquivOfAlgEquiv_symm_apply_eq_mapEquiv
Documentation

The inverse induced residue equivalence agrees with the inverse quotient-map equivalence.

Source context 11 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
namespace ResidueField
variable {R : Type u} {S : Type v} {T : Type w}
section AlgEquiv
variable [CommRing T] [IsLocalRing T]
variable [CommRing R] [IsLocalRing R] [Algebra T R]
variable [CommRing S] [IsLocalRing S] [Algebra T S]
variable [IsLocalHom (algebraMap T R)] [IsLocalHom (algebraMap T S)]
Lean source · statement
theorem algEquivOfAlgEquiv_symm_apply_eq_mapEquiv
    (e : R ≃ₐ[T] S)
    (x : IsLocalRing.ResidueField S) :
    (algEquivOfAlgEquiv e).symm x =
      IsLocalRing.ResidueField.mapEquiv e.symm.toRingEquiv x
theorem

algEquivOfAlgEquiv_apply_residue

L273 ↗
ValuationTheory.DiscreteValuationField.ResidueField.algEquivOfAlgEquiv_apply_residue
Documentation

The induced residue equivalence sends the residue of an integral element to its transported residue.

Source context 11 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
namespace ResidueField
variable {R : Type u} {S : Type v} {T : Type w}
section AlgEquiv
variable [CommRing T] [IsLocalRing T]
variable [CommRing R] [IsLocalRing R] [Algebra T R]
variable [CommRing S] [IsLocalRing S] [Algebra T S]
variable [IsLocalHom (algebraMap T R)] [IsLocalHom (algebraMap T S)]
Lean source · statement
theorem algEquivOfAlgEquiv_apply_residue
    (e : R ≃ₐ[T] S) (x : R) :
    algEquivOfAlgEquiv e (IsLocalRing.residue R x) =
      IsLocalRing.residue S (e x)
theorem

algEquivOfAlgEquiv_symm_apply_residue

L286 ↗
ValuationTheory.DiscreteValuationField.ResidueField.algEquivOfAlgEquiv_symm_apply_residue
Documentation

The inverse induced residue equivalence sends residues back along the inverse algebra equivalence.

Source context 11 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
namespace ResidueField
variable {R : Type u} {S : Type v} {T : Type w}
section AlgEquiv
variable [CommRing T] [IsLocalRing T]
variable [CommRing R] [IsLocalRing R] [Algebra T R]
variable [CommRing S] [IsLocalRing S] [Algebra T S]
variable [IsLocalHom (algebraMap T R)] [IsLocalHom (algebraMap T S)]
Lean source · statement
theorem algEquivOfAlgEquiv_symm_apply_residue
    (e : R ≃ₐ[T] S) (x : S) :
    (algEquivOfAlgEquiv e).symm (IsLocalRing.residue S x) =
      IsLocalRing.residue R (e.symm x)
theorem

algEquivOfAlgEquiv_symm

L299 ↗
ValuationTheory.DiscreteValuationField.ResidueField.algEquivOfAlgEquiv_symm
Documentation

Passing to residue fields commutes with inversion of algebra equivalences.

Source context 11 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
namespace ResidueField
variable {R : Type u} {S : Type v} {T : Type w}
section AlgEquiv
variable [CommRing T] [IsLocalRing T]
variable [CommRing R] [IsLocalRing R] [Algebra T R]
variable [CommRing S] [IsLocalRing S] [Algebra T S]
variable [IsLocalHom (algebraMap T R)] [IsLocalHom (algebraMap T S)]
Lean source · statement
theorem algEquivOfAlgEquiv_symm
    (e : R ≃ₐ[T] S) :
    (algEquivOfAlgEquiv e).symm = algEquivOfAlgEquiv e.symm
theorem

algEquivOfAlgEquiv_refl

L307 ↗
ValuationTheory.DiscreteValuationField.ResidueField.algEquivOfAlgEquiv_refl
Documentation

The identity algebra equivalence induces the identity on residue fields.

Source context 11 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
namespace ResidueField
variable {R : Type u} {S : Type v} {T : Type w}
section AlgEquiv
variable [CommRing T] [IsLocalRing T]
variable [CommRing R] [IsLocalRing R] [Algebra T R]
variable [CommRing S] [IsLocalRing S] [Algebra T S]
variable [IsLocalHom (algebraMap T R)] [IsLocalHom (algebraMap T S)]
Lean source · statement
theorem algEquivOfAlgEquiv_refl :
    algEquivOfAlgEquiv (AlgEquiv.refl : R ≃ₐ[T] R) =
      (AlgEquiv.refl :
        IsLocalRing.ResidueField R ≃ₐ[IsLocalRing.ResidueField T]
          IsLocalRing.ResidueField R)
theorem

algEquivOfAlgEquiv_trans

L317 ↗
ValuationTheory.DiscreteValuationField.ResidueField.algEquivOfAlgEquiv_trans
Documentation

Residue-field equivalences respect composition of algebra equivalences.

Source context 11 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
namespace ResidueField
variable {R : Type u} {S : Type v} {T : Type w}
section AlgEquiv
variable [CommRing T] [IsLocalRing T]
variable [CommRing R] [IsLocalRing R] [Algebra T R]
variable [CommRing S] [IsLocalRing S] [Algebra T S]
variable [IsLocalHom (algebraMap T R)] [IsLocalHom (algebraMap T S)]
Lean source · statement
theorem algEquivOfAlgEquiv_trans
    {U : Type*} [CommRing U] [IsLocalRing U] [Algebra T U]
    [IsLocalHom (algebraMap T U)]
    (eRS : R ≃ₐ[T] S) (eSU : S ≃ₐ[T] U) :
    (algEquivOfAlgEquiv eRS).trans (algEquivOfAlgEquiv eSU) =
      algEquivOfAlgEquiv (eRS.trans eSU)

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