Lean4
theorem pi_iff [Finite I] : FormallySmooth R (Π i, A i) ↔ ∀ i, FormallySmooth R (A i) := by
classical
cases nonempty_fintype I
constructor
· exact fun _ ↦ of_pi A
· intro H
constructor
intro B _ _ J hJ g
have hJ' (x) (hx : x ∈ RingHom.ker (Ideal.Quotient.mk J)) : IsNilpotent x :=
by
refine ⟨2, show x ^ 2 ∈ (⊥ : Ideal B) from ?_⟩
rw [← hJ]
exact Ideal.pow_mem_pow (by simpa using hx) 2
obtain ⟨e, he, he'⟩ :=
((CompleteOrthogonalIdempotents.single A).map g.toRingHom).lift_of_isNilpotent_ker (Ideal.Quotient.mk J) hJ'
fun _ ↦ Ideal.Quotient.mk_surjective _
replace he' : ∀ i, Ideal.Quotient.mk J (e i) = g (Pi.single i 1) := congr_fun he'
let iso : B ≃ₐ[R] ∀ i, B ⧸ Ideal.span {1 - e i} :=
{ __ := Pi.algHom _ _ fun i ↦ Ideal.Quotient.mkₐ R _
__ := Equiv.ofBijective _ he.bijective_pi }
let J' := fun i ↦ J.map (Ideal.Quotient.mk (Ideal.span {1 - e i}))
let ι : ∀ i, (B ⧸ J →ₐ[R] (B ⧸ _) ⧸ J' i) := fun i ↦
Ideal.quotientMapₐ _ (IsScalarTower.toAlgHom R B _) Ideal.le_comap_map
have hι : ∀ i x, ι i x = 0 → (e i) * x = 0 := by
intro i x hix
have : x ∈ (Ideal.span {1 - e i}).map (Ideal.Quotient.mk J) := by rw [← Ideal.ker_quotientMap_mk]; exact hix
rw [Ideal.map_span, Set.image_singleton, Ideal.mem_span_singleton] at this
obtain ⟨c, rfl⟩ := this
rw [← mul_assoc, ← map_mul, mul_sub, mul_one, (he.idem i).eq, sub_self, map_zero, zero_mul]
have :
∀ i : I,
∃ a : A i →ₐ[R] B ⧸ Ideal.span {1 - e i}, ∀ x, Ideal.Quotient.mk (J' i) (a x) = ι i (g (Pi.single i x)) :=
by
intro i
let g' : A i →ₐ[R] (B ⧸ _) ⧸ (J' i) :=
by
apply AlgHom.ofLinearMap (((ι i).comp g).toLinearMap ∘ₗ LinearMap.single _ _ i)
· suffices Ideal.Quotient.mk (Ideal.span {1 - e i}) (e i) = 1 by simp [ι, ← he', this]
rw [← (Ideal.Quotient.mk _).map_one, eq_comm, Ideal.Quotient.mk_eq_mk_iff_sub_mem, Ideal.mem_span_singleton]
· intro x y; simp [Pi.single_mul]
obtain ⟨a, ha⟩ := FormallySmooth.comp_surjective (I := J' i) (by rw [← Ideal.map_pow, hJ, Ideal.map_bot]) g'
exact ⟨a, AlgHom.congr_fun ha⟩
choose a ha using this
use iso.symm.toAlgHom.comp (Pi.algHom _ _ fun i ↦ (a i).comp (Pi.evalAlgHom R A i))
ext x; rw [← AlgHom.toLinearMap_apply, ← AlgHom.toLinearMap_apply]; congr 1
ext i x
simp only [AlgEquiv.toAlgHom_eq_coe, AlgHom.comp_toLinearMap, AlgEquiv.toAlgHom_toLinearMap, LinearMap.coe_comp,
LinearMap.coe_single, Function.comp_apply, AlgHom.toLinearMap_apply, AlgEquiv.toLinearMap_apply,
Ideal.Quotient.mkₐ_eq_mk]
obtain ⟨y, hy⟩ := Ideal.Quotient.mk_surjective (a i x)
have hy' : Ideal.Quotient.mk (Ideal.span {1 - e i}) (y * e i) = a i x :=
by
have : Ideal.Quotient.mk (Ideal.span {1 - e i}) (e i) = 1 := by
rw [← (Ideal.Quotient.mk _).map_one, eq_comm, Ideal.Quotient.mk_eq_mk_iff_sub_mem, Ideal.mem_span_singleton]
rw [map_mul, this, hy, mul_one]
trans Ideal.Quotient.mk J (y * e i)
· congr 1; apply iso.injective; ext j
suffices a j (Pi.single i x j) = Ideal.Quotient.mk _ (y * e i) by simpa using this
by_cases hij : i = j
· subst hij
rw [Pi.single_eq_same, hy']
· have : Ideal.Quotient.mk (Ideal.span {1 - e j}) (e i) = 0 :=
by
rw [Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_span_singleton]
refine ⟨e i, by simp [he.ortho (Ne.symm hij), sub_mul]⟩
rw [Pi.single_eq_of_ne (Ne.symm hij), map_zero, map_mul, this, mul_zero]
· have : ι i (Ideal.Quotient.mk J (y * e i)) = ι i (g (Pi.single i x)) :=
by
rw [← ha, ← hy']
simp only [Ideal.quotient_map_mkₐ, IsScalarTower.coe_toAlgHom', Ideal.Quotient.algebraMap_eq,
Ideal.Quotient.mkₐ_eq_mk, ι]
rw [← sub_eq_zero, ← map_sub] at this
replace this := hι _ _ this
rwa [mul_sub, ← map_mul, mul_comm, mul_assoc, (he.idem i).eq, he', ← map_mul, ← Pi.single_mul, one_mul,
sub_eq_zero] at this
