-- Mathlib/RingTheory/Flat/FaithfullyFlat/Algebra.lean
/-- If `A →+* B` is flat and surjective on prime spectra, `B` is a faithfully flat `A`-algebra. -/
lemma Module.FaithfullyFlat.of_specComap_surjective [Flat A B]
    (h : Function.Surjective ((algebraMap A B).specComap)) :
    Module.FaithfullyFlat A B

Proof state:
case intro
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Flat A B
h : Function.Surjective (algebraMap A B).specComap
m : Ideal A
hm : m.IsMaximal
m' : PrimeSpectrum B
hm' : (algebraMap A B).specComap m' = { asIdeal := m, isPrime := ⋯ }
⊢ m • ⊤ ≠ ⊤

Tactic:
have : m = Ideal.comap (algebraMap A B) m'.asIdeal := by
  rw [← PrimeSpectrum.specComap_asIdeal (algebraMap A B) m', hm']

Result:
case intro
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Flat A B
h : Function.Surjective (algebraMap A B).specComap
m : Ideal A
hm : m.IsMaximal
m' : PrimeSpectrum B
hm' : (algebraMap A B).specComap m' = { asIdeal := m, isPrime := ⋯ }
this : m = Ideal.comap (algebraMap A B) m'.asIdeal
⊢ m • ⊤ ≠ ⊤

Proof state:
case intro
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Flat A B
h : Function.Surjective (algebraMap A B).specComap
m : Ideal A
hm : m.IsMaximal
m' : PrimeSpectrum B
hm' : (algebraMap A B).specComap m' = { asIdeal := m, isPrime := ⋯ }
this : m = Ideal.comap (algebraMap A B) m'.asIdeal
⊢ Submodule.restrictScalars A (Ideal.map (algebraMap A B) (Ideal.comap (algebraMap A B) m'.asIdeal)) ≠ ⊤

Tactic:
exact (Submodule.restrictScalars_eq_top_iff _ _ _).ne.mpr
  fun top ↦ m'.isPrime.ne_top <| top_le_iff.mp <| top ▸ Ideal.map_comap_le

Result:
no goals

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Flat A B
h : Function.Surjective (algebraMap A B).specComap
⊢ FaithfullyFlat A B

Tactic:
refine ⟨fun m hm ↦ ?_⟩

Result:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Flat A B
h : Function.Surjective (algebraMap A B).specComap
m : Ideal A
hm : m.IsMaximal
⊢ m • ⊤ ≠ ⊤

Proof state:
case intro
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Flat A B
h : Function.Surjective (algebraMap A B).specComap
m : Ideal A
hm : m.IsMaximal
m' : PrimeSpectrum B
hm' : (algebraMap A B).specComap m' = { asIdeal := m, isPrime := ⋯ }
this : m = Ideal.comap (algebraMap A B) m'.asIdeal
⊢ m • ⊤ ≠ ⊤

Tactic:
rw [Ideal.smul_top_eq_map, this]

Result:
case intro
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Flat A B
h : Function.Surjective (algebraMap A B).specComap
m : Ideal A
hm : m.IsMaximal
m' : PrimeSpectrum B
hm' : (algebraMap A B).specComap m' = { asIdeal := m, isPrime := ⋯ }
this : m = Ideal.comap (algebraMap A B) m'.asIdeal
⊢ Submodule.restrictScalars A (Ideal.map (algebraMap A B) (Ideal.comap (algebraMap A B) m'.asIdeal)) ≠ ⊤

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Flat A B
h : Function.Surjective (algebraMap A B).specComap
m : Ideal A
hm : m.IsMaximal
⊢ m • ⊤ ≠ ⊤

Tactic:
obtain ⟨m', hm'⟩ := h ⟨m, hm.isPrime⟩

Result:
case intro
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Flat A B
h : Function.Surjective (algebraMap A B).specComap
m : Ideal A
hm : m.IsMaximal
m' : PrimeSpectrum B
hm' : (algebraMap A B).specComap m' = { asIdeal := m, isPrime := ⋯ }
⊢ m • ⊤ ≠ ⊤

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Flat A B
h : Function.Surjective (algebraMap A B).specComap
m : Ideal A
hm : m.IsMaximal
m' : PrimeSpectrum B
hm' : (algebraMap A B).specComap m' = { asIdeal := m, isPrime := ⋯ }
⊢ m = Ideal.comap (algebraMap A B) m'.asIdeal

Tactic:
rw [← PrimeSpectrum.specComap_asIdeal (algebraMap A B) m', hm']

Result:
no goals