faithfully flat

Stream: Is there code for X?

[Yongle Hu]

Hi! Is there a formalization of faithfully flat in Mathlib now? Or is anyone currently formalizing faithfully flat? If not, we would be happy to formalize faithfully flat. We plan to formalize all the definitions and theorems in Stacks Project, Section 00H9 that are not yet in Mathlib.

[Kim Morrison]

Everything we have so far is in Mathlib/RingTheory/Flat/

[Joël Riou]

I would like to point out there is some work in progress https://github.com/leanprover-community/mathlib4/pull/15014 about faithfully flat morphisms of rings and https://github.com/leanprover-community/mathlib4/pull/14203 towards faithfully flat descent of modules.

[Yongle Hu]

@Judith Ludwig Are you actively working on the rest of Stacks Project, Section 00H9? If not, can you give us the permission to use the results in your PR #15014?

[Jujian Zhang]

I have picked up #15014 and proved 00HO and most of 00HP