R : Type u_3
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a : R
ι : Type u_1
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
inst✝ : DecidableEq ι
T : Finset ι
hT : T ⊆ S
i : ι
hi : i ∈ S
hiT : ¬i ∈ T
⊢ (fun i => torsionBySet R M ↑(p i)) i ⊓ torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ T), p i) = ⊥
R : Type u_3
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a : R
ι : Type u_1
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
inst✝ : DecidableEq ι
T : Finset ι
hT : T ⊆ S
i : ι
hi : i ∈ S
hiT : ¬i ∈ T
⊢ Disjoint ((fun i => torsionBySet R M ↑(p i)) i) (Finset.sup T fun i => torsionBySet R M ↑(p i))
rw [disjoint_iff, Finset.sup_eq_iSup,
  iSup_torsionBySet_ideal_eq_torsionBySet_iInf fun i hi j hj ij => hp (hT hi) (hT hj) ij]
R : Type u_3
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a : R
ι : Type u_1
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
inst✝ : DecidableEq ι
T : Finset ι
hT : T ⊆ S
i : ι
hi : i ∈ S
hiT : ¬i ∈ T
this :
  torsionBySet R M ↑(↑OrderDual.ofDual (↑OrderDual.toDual (p i) ⊓ ↑OrderDual.toDual (⨅ (i : ι) (_ : i ∈ T), p i))) =
    torsionBySet R M ↑(↑OrderDual.ofDual (↑OrderDual.toDual (p i))) ⊓
      torsionBySet R M ↑(↑OrderDual.ofDual (↑OrderDual.toDual (⨅ (i : ι) (_ : i ∈ T), p i)))
⊢ (fun i => torsionBySet R M ↑(p i)) i ⊓ torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ T), p i) = ⊥
R : Type u_3
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a : R
ι : Type u_1
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
inst✝ : DecidableEq ι
T : Finset ι
hT : T ⊆ S
i : ι
hi : i ∈ S
hiT : ¬i ∈ T
⊢ (fun i => torsionBySet R M ↑(p i)) i ⊓ torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ T), p i) = ⊥
have := GaloisConnection.u_inf
  (b₁ := OrderDual.toDual (p i)) (b₂ := OrderDual.toDual (⨅ i ∈ T, p i)) (torsion_gc R M)
R : Type u_3
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a : R
ι : Type u_1
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
inst✝ : DecidableEq ι
T : Finset ι
hT : T ⊆ S
i : ι
hi : i ∈ S
hiT : ¬i ∈ T
this :
  torsionBySet R M ↑(p i ⊔ ⨅ (i : ι) (_ : i ∈ T), p i) =
    torsionBySet R M ↑(p i) ⊓ torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ T), p i)
⊢ torsionBySet R M ↑(p i) ⊓ torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ T), p i) = ⊥
R : Type u_3
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a : R
ι : Type u_1
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
inst✝ : DecidableEq ι
T : Finset ι
hT : T ⊆ S
i : ι
hi : i ∈ S
hiT : ¬i ∈ T
this :
  torsionBySet R M ↑(↑OrderDual.ofDual (↑OrderDual.toDual (p i) ⊓ ↑OrderDual.toDual (⨅ (i : ι) (_ : i ∈ T), p i))) =
    torsionBySet R M ↑(↑OrderDual.ofDual (↑OrderDual.toDual (p i))) ⊓
      torsionBySet R M ↑(↑OrderDual.ofDual (↑OrderDual.toDual (⨅ (i : ι) (_ : i ∈ T), p i)))
⊢ (fun i => torsionBySet R M ↑(p i)) i ⊓ torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ T), p i) = ⊥
dsimp at this ⊢
R : Type u_3
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a : R
ι : Type u_1
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
inst✝ : DecidableEq ι
T : Finset ι
hT : T ⊆ S
i : ι
hi : i ∈ S
hiT : ¬i ∈ T
this :
  torsionBySet R M ↑(p i ⊔ ⨅ (i : ι) (_ : i ∈ T), p i) =
    torsionBySet R M ↑(p i) ⊓ torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ T), p i)
⊢ ∀ (i_1 : ι), i_1 ∈ T → p i ⊔ p i_1 = ⊤
R : Type u_3
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a : R
ι : Type u_1
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
inst✝ : DecidableEq ι
T : Finset ι
hT : T ⊆ S
i : ι
hi : i ∈ S
hiT : ¬i ∈ T
this :
  torsionBySet R M ↑(p i ⊔ ⨅ (i : ι) (_ : i ∈ T), p i) =
    torsionBySet R M ↑(p i) ⊓ torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ T), p i)
⊢ torsionBySet R M ↑(p i) ⊓ torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ T), p i) = ⊥
rw [← this, Ideal.sup_iInf_eq_top, top_coe, torsionBySet_univ]
R : Type u_3
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a : R
ι : Type u_1
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
inst✝ : DecidableEq ι
T : Finset ι
hT : T ⊆ S
i : ι
hi : i ∈ S
hiT : ¬i ∈ T
this :
  torsionBySet R M ↑(p i ⊔ ⨅ (i : ι) (_ : i ∈ T), p i) =
    torsionBySet R M ↑(p i) ⊓ torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ T), p i)
j : ι
hj : j ∈ T
⊢ p i ⊔ p j = ⊤
R : Type u_3
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a : R
ι : Type u_1
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
inst✝ : DecidableEq ι
T : Finset ι
hT : T ⊆ S
i : ι
hi : i ∈ S
hiT : ¬i ∈ T
this :
  torsionBySet R M ↑(p i ⊔ ⨅ (i : ι) (_ : i ∈ T), p i) =
    torsionBySet R M ↑(p i) ⊓ torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ T), p i)
⊢ ∀ (i_1 : ι), i_1 ∈ T → p i ⊔ p i_1 = ⊤
intro j hj
R : Type u_3
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a : R
ι : Type u_1
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
inst✝ : DecidableEq ι
T : Finset ι
hT : T ⊆ S
i : ι
hi : i ∈ S
hiT : ¬i ∈ T
this :
  torsionBySet R M ↑(p i ⊔ ⨅ (i : ι) (_ : i ∈ T), p i) =
    torsionBySet R M ↑(p i) ⊓ torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ T), p i)
j : ι
hj : j ∈ T
⊢ i ≠ j
R : Type u_3
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a : R
ι : Type u_1
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
inst✝ : DecidableEq ι
T : Finset ι
hT : T ⊆ S
i : ι
hi : i ∈ S
hiT : ¬i ∈ T
this :
  torsionBySet R M ↑(p i ⊔ ⨅ (i : ι) (_ : i ∈ T), p i) =
    torsionBySet R M ↑(p i) ⊓ torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ T), p i)
j : ι
hj : j ∈ T
⊢ p i ⊔ p j = ⊤
apply hp hi (hT hj)
R : Type u_3
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a : R
ι : Type u_1
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
inst✝ : DecidableEq ι
T : Finset ι
hT : T ⊆ S
i : ι
hi : i ∈ S
hiT : ¬i ∈ T
this :
  torsionBySet R M ↑(p i ⊔ ⨅ (i : ι) (_ : i ∈ T), p i) =
    torsionBySet R M ↑(p i) ⊓ torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ T), p i)
hj : i ∈ T
⊢ False
R : Type u_3
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a : R
ι : Type u_1
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
inst✝ : DecidableEq ι
T : Finset ι
hT : T ⊆ S
i : ι
hi : i ∈ S
hiT : ¬i ∈ T
this :
  torsionBySet R M ↑(p i ⊔ ⨅ (i : ι) (_ : i ∈ T), p i) =
    torsionBySet R M ↑(p i) ⊓ torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ T), p i)
j : ι
hj : j ∈ T
⊢ i ≠ j
rintro rfl
no goals
R : Type u_3
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set R
a : R
ι : Type u_1
p : ι → Ideal R
S : Finset ι
hp : Set.Pairwise ↑S fun i j => p i ⊔ p j = ⊤
inst✝ : DecidableEq ι
T : Finset ι
hT : T ⊆ S
i : ι
hi : i ∈ S
hiT : ¬i ∈ T
this :
  torsionBySet R M ↑(p i ⊔ ⨅ (i : ι) (_ : i ∈ T), p i) =
    torsionBySet R M ↑(p i) ⊓ torsionBySet R M ↑(⨅ (i : ι) (_ : i ∈ T), p i)
hj : i ∈ T
⊢ False
exact hiT hj