IdempotentFactorProduct.lean

def quotientPiRingEquiv {D : Type*} [CommRing D] {e : I → D}
    (he : CompleteOrthogonalIdempotents e) :
    D ≃+* ∀ i, D ⧸ Ideal.span {1 - e i}

theorem quotientPiRingEquiv_toRingHom {D : Type*} [CommRing D] {e : I → D}
    (he : CompleteOrthogonalIdempotents e) :
    he.quotientPiRingEquiv.toRingHom =
      RingHom.pi fun i ↦ Ideal.Quotient.mk (Ideal.span {1 - e i}) :=
  rfl

theorem quotientPiRingEquiv_apply {D : Type*} [CommRing D] {e : I → D}
    (he : CompleteOrthogonalIdempotents e) (x : D) (i : I) :
    he.quotientPiRingEquiv x i =
      Ideal.Quotient.mk (Ideal.span {1 - e i}) x

def quotientPiAlgEquiv {B D : Type*} [CommRing B] [CommRing D]
    [Algebra B D] {e : I → D} (he : CompleteOrthogonalIdempotents e) :
    D ≃ₐ[B] ∀ i, D ⧸ Ideal.span {1 - e i}

theorem quotientPiAlgEquiv_toAlgHom {B D : Type*} [CommRing B] [CommRing D]
    [Algebra B D] {e : I → D} (he : CompleteOrthogonalIdempotents e) :
    (he.quotientPiAlgEquiv (B := B)).toAlgHom =
      AlgHom.pi fun i ↦ Ideal.Quotient.mkₐ B (Ideal.span {1 - e i}) :=
  rfl

theorem quotientPiAlgEquiv_apply {B D : Type*} [CommRing B] [CommRing D]
    [Algebra B D] {e : I → D} (he : CompleteOrthogonalIdempotents e)
    (x : D) (i : I) :
    (he.quotientPiAlgEquiv (B := B)) x i =
      Ideal.Quotient.mk (Ideal.span {1 - e i}) x