Theorems · Theorem · commutative algebra

Valuation.HasExtension.maximalIdeal_comap_algebraMap_eq_maximalIdeal

∀ {K : outParam (Type u_5)} {L : outParam (Type u_6)} {Γ₀ : outParam (Type u_7)} {Γ₁ : outParam (Type u_8)}
  [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [inst_3 : LinearOrderedCommGroupWithZero Γ₀]
  [inst_4 : LinearOrderedCommGroupWithZero Γ₁] (vK : Valuation K Γ₀) (vL : Valuation L Γ₁)
  [inst_5 : vK.HasExtension vL],
  Ideal.comap (algebraMap ↥vK.valuationSubring ↥vL.valuationSubring) (IsLocalRing.maximalIdeal ↥vL.valuationSubring) =
    IsLocalRing.maximalIdeal ↥vK.valuationSubring

Defined in

Mathlib.RingTheory.Valuation.Extension

Cited by

0 results in Mathlib

Foundations

Depth 58 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldFieldAlgebraLinearOrderedCommGroupWithZeroLinearOrderedCommGroupWithZeroValuation.HasExtension