of_bijective — Mathlib

English

Bijective ring homomorphisms are FaithfullyFlat.

Русский

Bijective отображения колец являются FaithfullyFlat.

LaTeX

$$$\\text{of_bijective}\\;hf \\Rightarrow f.{\\text{FaithfullyFlat}}$$$

Lean4

theorem of_bijective (hf : Function.Bijective f) : f.FaithfullyFlat :=
  by
  rw [iff_flat_and_comap_surjective]
  refine ⟨.of_bijective hf, fun p ↦ ?_⟩
  use ((RingEquiv.ofBijective f hf).symm : _ →+* _).specComap p
  have : ((RingEquiv.ofBijective f hf).symm : _ →+* _).comp f = id R :=
    by
    ext
    exact (RingEquiv.ofBijective f hf).injective (by simp)
  rw [← PrimeSpectrum.specComap_comp_apply, this, PrimeSpectrum.specComap_id]

Похожие утверждения