of_pi — Mathlib

English

If the product is formally smooth, then each factor is formally smooth; equivalently, pi_iff holds.

Русский

Если произведение формально гладкое, то каждая составляющая формально гладкая; эквивалентно верности pi_iff.

LaTeX

$$$\text{FormallySmooth}(R, \prod_i A_i) \Rightarrow \forall i, \text{FormallySmooth}(R, A_i)$$$

Lean4

theorem of_pi [FormallySmooth R (Π i, A i)] (i) : FormallySmooth R (A i) := by
  classical
  fapply FormallySmooth.of_split (Pi.evalAlgHom R A i)
  · apply AlgHom.ofLinearMap ((Ideal.Quotient.mkₐ R _).toLinearMap.comp (LinearMap.single _ _ i))
    · change Ideal.Quotient.mk _ (Pi.single i 1) = 1
      rw [← (Ideal.Quotient.mk _).map_one, ← sub_eq_zero, ← map_sub, Ideal.Quotient.eq_zero_iff_mem]
      have : Pi.single i 1 - 1 ∈ RingHom.ker (Pi.evalAlgHom R A i).toRingHom := by simp [RingHom.mem_ker]
      convert neg_mem (Ideal.pow_mem_pow this 2) using 1
      simp [pow_two, sub_mul, mul_sub, ← Pi.single_mul]
    · intro x y
      change Ideal.Quotient.mk _ _ = Ideal.Quotient.mk _ _ * Ideal.Quotient.mk _ _
      simp only [AlgHom.toRingHom_eq_coe, LinearMap.coe_single, Pi.single_mul, map_mul]
  · ext x
    change (Pi.single i x) i = x
    simp

Похожие утверждения