CoprimeProduct.lean

def quotientProdPowEquiv
    (J : ι → Ideal R) (hJ : Pairwise (IsCoprime on J)) (n : ℕ) :
    R ⧸ (∏ i, J i) ^ n ≃+* ∀ i, R ⧸ J i ^ n

theorem quotientProdPowEquiv_mk
    (J : ι → Ideal R) (hJ : Pairwise (IsCoprime on J)) (n : ℕ) (x : R) :
    quotientProdPowEquiv J hJ n (Ideal.Quotient.mk _ x) =
      fun _ => Ideal.Quotient.mk _ x := by
  rfl

theorem quotientProdPowEquiv_factorPow
    (J : ι → Ideal R) (hJ : Pairwise (IsCoprime on J))
    {m n : ℕ} (hmn : m ≤ n) (x : R ⧸ (∏ i, J i) ^ n) (i : ι) :
    Ideal.Quotient.factorPow (J i) hmn (quotientProdPowEquiv J hJ n x i) =
      quotientProdPowEquiv J hJ m
        (Ideal.Quotient.factorPow (∏ i, J i) hmn x) i

theorem quotientProdPowEquiv_symm_factorPow
    (J : ι → Ideal R) (hJ : Pairwise (IsCoprime on J))
    {m n : ℕ} (hmn : m ≤ n) (x : ∀ i, R ⧸ J i ^ n) :
    Ideal.Quotient.factorPow (∏ i, J i) hmn
        ((quotientProdPowEquiv J hJ n).symm x) =
      (quotientProdPowEquiv J hJ m).symm
        (fun i => Ideal.Quotient.factorPow (J i) hmn (x i)) := by
  apply (quotientProdPowEquiv J hJ m).injective
  funext i
  rw [RingEquiv.apply_symm_apply,
    ← quotientProdPowEquiv_factorPow J hJ hmn
      ((quotientProdPowEquiv J hJ n).symm x) i,
    RingEquiv.apply_symm_apply]

theorem factorPow_evalₐ
    (K : Ideal R) {m n : ℕ} (hmn : m ≤ n) (x : AdicCompletion K R) :
    Ideal.Quotient.factorPow K hmn (AdicCompletion.evalₐ K n x) =
      AdicCompletion.evalₐ K m x

def quotientProjectionRingHom
    (J : ι → Ideal R) (hJ : Pairwise (IsCoprime on J)) (i : ι) (n : ℕ) :
    AdicCompletion (∏ j, J j) R →+* R ⧸ J i ^ n

theorem quotientProjectionRingHom_compatible
    (J : ι → Ideal R) (hJ : Pairwise (IsCoprime on J)) (i : ι) :
    ∀ {m n : ℕ} (hmn : m ≤ n),
      (Ideal.Quotient.factorPow (J i) hmn).comp
          (quotientProjectionRingHom J hJ i n) =
        quotientProjectionRingHom J hJ i m

def adicCompletionToComponent
    (J : ι → Ideal R) (hJ : Pairwise (IsCoprime on J)) (i : ι) :
    AdicCompletion (∏ j, J j) R →+* AdicCompletion (J i) R

theorem evalₐ_adicCompletionToComponent
    (J : ι → Ideal R) (hJ : Pairwise (IsCoprime on J)) (i : ι)
    (n : ℕ) (x : AdicCompletion (∏ j, J j) R) :
    AdicCompletion.evalₐ (J i) n (adicCompletionToComponent J hJ i x) =
      quotientProdPowEquiv J hJ n
        (AdicCompletion.evalₐ (∏ j, J j) n x) i

def quotientAssemblyRingHom
    (J : ι → Ideal R) (hJ : Pairwise (IsCoprime on J)) (n : ℕ) :
    (∀ i, AdicCompletion (J i) R) →+* R ⧸ (∏ i, J i) ^ n

theorem quotientAssemblyRingHom_compatible
    (J : ι → Ideal R) (hJ : Pairwise (IsCoprime on J)) :
    ∀ {m n : ℕ} (hmn : m ≤ n),
      (Ideal.Quotient.factorPow (∏ i, J i) hmn).comp
          (quotientAssemblyRingHom J hJ n) =
        quotientAssemblyRingHom J hJ m

def adicCompletionFromPi
    (J : ι → Ideal R) (hJ : Pairwise (IsCoprime on J)) :
    (∀ i, AdicCompletion (J i) R) →+* AdicCompletion (∏ i, J i) R

theorem evalₐ_adicCompletionFromPi
    (J : ι → Ideal R) (hJ : Pairwise (IsCoprime on J))
    (n : ℕ) (x : ∀ i, AdicCompletion (J i) R) :
    AdicCompletion.evalₐ (∏ i, J i) n (adicCompletionFromPi J hJ x) =
      (quotientProdPowEquiv J hJ n).symm
        (fun i => AdicCompletion.evalₐ (J i) n (x i)) := by
  unfold adicCompletionFromPi
  rw [AdicCompletion.evalₐ_liftRingHom]
  rfl

def adicCompletionToPi
    (J : ι → Ideal R) (hJ : Pairwise (IsCoprime on J)) :
    AdicCompletion (∏ i, J i) R →+* ∀ i, AdicCompletion (J i) R

theorem adicCompletionToPi_comp_fromPi
    (J : ι → Ideal R) (hJ : Pairwise (IsCoprime on J)) :
    (adicCompletionToPi J hJ).comp (adicCompletionFromPi J hJ) =
      RingHom.id (∀ i, AdicCompletion (J i) R)

theorem adicCompletionFromPi_comp_toPi
    (J : ι → Ideal R) (hJ : Pairwise (IsCoprime on J)) :
    (adicCompletionFromPi J hJ).comp (adicCompletionToPi J hJ) =
      RingHom.id (AdicCompletion (∏ i, J i) R)

def adicCompletionProdEquivPi
    (J : ι → Ideal R) (hJ : Pairwise (IsCoprime on J)) :
    AdicCompletion (∏ i, J i) R ≃+* ∀ i, AdicCompletion (J i) R

theorem adicCompletionProdEquivPi_apply
    (J : ι → Ideal R) (hJ : Pairwise (IsCoprime on J))
    (x : AdicCompletion (∏ i, J i) R) (i : ι) :
    adicCompletionProdEquivPi J hJ x i =
      adicCompletionToComponent J hJ i x

theorem adicCompletionProdEquivPi_of
    (J : ι → Ideal R) (hJ : Pairwise (IsCoprime on J))
    (x : R) (i : ι) :
    adicCompletionProdEquivPi J hJ
        (AdicCompletion.of (∏ j, J j) R x) i =
      AdicCompletion.of (J i) R x

def adicCompletionIdealCongr
    {I J : Ideal R} (h : I = J) :
    AdicCompletion I R ≃+* AdicCompletion J R

theorem adicCompletionIdealCongr_of
    {I J : Ideal R} (h : I = J) (x : R) :
    adicCompletionIdealCongr h (AdicCompletion.of I R x) =
      AdicCompletion.of J R x

def integralExtensionPrimesOverFintype
    {A : Type*} [CommRing A] [IsDomain A]
    {B : Type*} [CommRing B] [IsDedekindDomain B]
    [Algebra A B] [Algebra.IsIntegral A B] [Module.Finite A B]
    (p : Ideal A) : Fintype (p.primesOver B)

def integralExtensionPrimePowerFamily
    {A : Type*} [CommRing A] [IsDomain A]
    {B : Type*} [CommRing B] [IsDedekindDomain B]
    [Algebra A B] [Algebra.IsIntegral A B]
    (p : Ideal A) (Q : p.primesOver B) : Ideal B

theorem integralExtensionPrimePowerFamily_apply
    {A : Type*} [CommRing A] [IsDomain A]
    {B : Type*} [CommRing B] [IsDedekindDomain B]
    [Algebra A B] [Algebra.IsIntegral A B]
    (p : Ideal A) (Q : p.primesOver B) :
    integralExtensionPrimePowerFamily p Q =
      Q.1 ^ Q.1.ramificationIdx A

theorem integralExtensionPrimePowerFamily_pairwise
    {A : Type*} [CommRing A] [IsDomain A]
    {B : Type*} [CommRing B] [IsDedekindDomain B]
    [Algebra A B] [Algebra.IsIntegral A B]
    (p : Ideal A) [p.IsMaximal] :
    Pairwise (IsCoprime on integralExtensionPrimePowerFamily (B := B) p)

theorem integralExtension_map_eq_prod_primePowerFamily
    {A : Type*} [CommRing A] [IsDomain A]
    {B : Type*} [CommRing B] [IsDedekindDomain B]
    [Algebra A B] [Algebra.IsIntegral A B] [Module.IsTorsionFree A B]
    [Module.Finite A B]
    (p : Ideal A) [p.IsMaximal] (hp : p ≠ ⊥) :
    letI : Fintype (p.primesOver B) :=
      integralExtensionPrimesOverFintype p
    p.map (algebraMap A B) =
      ∏ Q, integralExtensionPrimePowerFamily (B := B) p Q := by
  let : Fintype (p.primesOver B) :=
    integralExtensionPrimesOverFintype p
  rw [Ideal.map_algebraMap_eq_finsetProd_pow hp]
  simpa [integralExtensionPrimePowerFamily] using
    (Finset.prod_set_coe (s := p.primesOver B)
      (f := fun P => P ^ P.ramificationIdx A)).symm

def adicCompletionIntegralExtensionEquivPi
    {A : Type*} [CommRing A] [IsDomain A]
    {B : Type*} [CommRing B] [IsDedekindDomain B]
    [Algebra A B] [Algebra.IsIntegral A B] [Module.IsTorsionFree A B]
    [Module.Finite A B] (p : Ideal A) [p.IsMaximal] (hp : p ≠ ⊥) :
    AdicCompletion (p.map (algebraMap A B)) B ≃+*
      ∀ Q : p.primesOver B,
        AdicCompletion (Q.1 ^ Q.1.ramificationIdx A) B

theorem adicCompletionIntegralExtensionEquivPi_of
    {A : Type*} [CommRing A] [IsDomain A]
    {B : Type*} [CommRing B] [IsDedekindDomain B]
    [Algebra A B] [Algebra.IsIntegral A B] [Module.IsTorsionFree A B]
    [Module.Finite A B] (p : Ideal A) [p.IsMaximal] (hp : p ≠ ⊥)
    (x : B) (Q : p.primesOver B) :
    adicCompletionIntegralExtensionEquivPi p hp
        (AdicCompletion.of (p.map (algebraMap A B)) B x) Q =
      AdicCompletion.of (Q.1 ^ Q.1.ramificationIdx A) B x