def chineseMap {ι : Type u_1} {R : Type u_2} [CommRing R] (I : ι → Ideal R) : R ⧸ ⨅ (i : ι), I i →+* (i : ι) → R ⧸ I i

The homomorphism from R ⧸ ⨅ i, I i to Π i, R ⧸ I i featured in the Chinese Remainder Theorem.

Equations

• chineseMap I = sorryAx (R ⧸ ⨅ (i : ι), I i →+* (i : ι) → R ⧸ I i)

theorem chineseMap_mk {ι : Type u_1} {R : Type u_2} [CommRing R] (I : ι → Ideal R) (x : R) : (chineseMap I) ⟦x⟧ = fun (i : ι) => (Ideal.Quotient.mk (I i)) x

theorem chineseMap_mk' {ι : Type u_1} {R : Type u_2} [CommRing R] (I : ι → Ideal R) (x : R) (i : ι) : (chineseMap I) ((Ideal.Quotient.mk (⨅ (i : ι), I i)) x) i = (Ideal.Quotient.mk (I i)) x

theorem chineseMap_inj {ι : Type u_1} {R : Type u_2} [CommRing R] (I : ι → Ideal R) : Function.Injective ⇑(chineseMap I)

theorem isCoprime_Inf {ι : Type u_1} {R : Type u_2} [CommRing R] {I : Ideal R} {J : ι → Ideal R} {s : Finset ι} (hf : ∀ j ∈ s, IsCoprime I (J j)) : IsCoprime I (⨅ j ∈ s, J j)

theorem chineseMap_surj {ι : Type u_1} {R : Type u_2} [CommRing R] [Fintype ι] {I : ι → Ideal R} (hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)) : Function.Surjective ⇑(chineseMap I)

noncomputable def chineseIso {ι : Type u_1} {R : Type u_2} [CommRing R] [Fintype ι] (f : ι → Ideal R) (hf : ∀ (i j : ι), i ≠ j → IsCoprime (f i) (f j)) : R ⧸ ⨅ (i : ι), f i ≃+* ((i : ι) → R ⧸ f i)

Equations

• chineseIso f hf = { toEquiv := Equiv.ofBijective ⇑(chineseMap f) ⋯, map_mul' := ⋯, map_add' := ⋯ }

def circleEquation : MvPolynomial (Fin 2) ℝ

Equations

• circleEquation = MvPolynomial.X 0 ^ 2 + MvPolynomial.X 1 ^ 2 - 1