Zulip Chat Archive
Stream: new members
Topic: FractionRing
亚历山大大帝 (Apr 12 2025 at 18:53):
Why can't inferInstance in “haveI : Algebra R (MvPolynomial X R) := inferInstance. haveI : IsDomain (MvPolynomial X R) := inferInstance” succeed?
Ilmārs Cīrulis (Apr 12 2025 at 18:59):
(deleted)
Ruben Van de Velde (Apr 12 2025 at 19:02):
Again, read #mwe and #backticks so we can help you
Junyan Xu (Apr 12 2025 at 22:40):
CommSemiring and Algebra are data and you need to use letI
Why are you declaring instances that can already be found by inferInstance?
亚历山大大帝 (Apr 13 2025 at 04:04):
IsLocalization.of_le can it be used in this environment? What other types need to be instantiated?
Lean4WebDownload (2).lean
import Mathlib
open IsFractionRing
-- 声明变量
variable {u v : Type} {R : Type u} {X : Type v} [CommRing R] [IsDomain R]
variable {S : Type v} [CommSemiring S] [Algebra R S]
variable (M : Submonoid R) [IsLocalization M S] (N : Submonoid R)
theorem FractionRing.isField :
IsField (FractionRing (MvPolynomial X R)) := by
-- 使用 letI 显式声明必要实例,确保类型类解析器能找到它们
letI : CommSemiring (MvPolynomial X R) := inferInstance
letI : Algebra R (MvPolynomial X R) := inferInstance
letI : IsDomain (MvPolynomial X R) := inferInstance
-- 构造 IsFractionRing 实例
letI isFractionRingInstance : IsFractionRing (MvPolynomial X R) (FractionRing (MvPolynomial X R)) := by
apply IsLocalization.of_le (MvPolynomial X R) (nonZeroDivisors (MvPolynomial X R)) (nonZeroDivisors (MvPolynomial X R))
<;> simp [nonZeroDivisors]
<;> exact fun r hr => by
simp [nonZeroDivisors, hr]
<;> exact inferInstance
-- 应用定理证明分式环是域
exact IsFractionRing.toField (MvPolynomial X R)
<;> infer_instance
example {R : Type u} [CommRing R] [IsDomain R] (I : Type v) :
FractionRing (MvPolynomial I R) ≃ₐ[R] FractionRing (MvPolynomial I (FractionRing R)) := by
-- 构造代数同构
refine' AlgEquiv.symm _
-- 应用分式域的代数同构定理
exact IsLocalization.algEquiv (nonZeroDivisors (MvPolynomial I R)) (le_refl _) (FractionRing (MvPolynomial I R)) (FractionRing (MvPolynomial I (FractionRing R)))
<;> infer_instance
Last updated: May 02 2025 at 03:31 UTC