ModuleValuationSubring_ResidueValuationSubring.lean
Nyll.AlgebraicCurves.Valuations.ValuationSubring_ResidueValuationSubring
6 declarations indexed from sourceView source ↗ Module documentation
Valuation Subring Residue Valuation Subring
Imports2
- Mathlib.RingTheory.Valuation.ValuationSubring
- Mathlib.RingTheory.LocalRing.ResidueField.Basic
Imported by4
Declarations
ValuationSubring.residueValuationSubring
DocumentationThe valuation subring of the residue field obtained as the image of the smaller valuation ring.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ValuationSubring
open IsLocalRing
variable {L : Type*} [Field L]
ValuationSubring.toResidueValuationSubring
DocumentationThe residue homomorphism from the smaller valuation ring onto its image in the residue field.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ValuationSubring
open IsLocalRing
variable {L : Type*} [Field L]
ValuationSubring.mem_residueValuationSubring_iff
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ValuationSubring
open IsLocalRing
variable {L : Type*} [Field L]
variable (A S : ValuationSubring L) (h : A ≤ S)
ValuationSubring.coe_toResidueValuationSubring
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ValuationSubring
open IsLocalRing
variable {L : Type*} [Field L]
variable (A S : ValuationSubring L) (h : A ≤ S)
ValuationSubring.toResidueValuationSubring_surjective
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ValuationSubring
open IsLocalRing
variable {L : Type*} [Field L]
variable (A S : ValuationSubring L) (h : A ≤ S)
ValuationSubring.ker_toResidueValuationSubring
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ValuationSubring
open IsLocalRing
variable {L : Type*} [Field L]
variable (A S : ValuationSubring L) (h : A ≤ S)