OAI/NumberTheory/PiExponent/Approximation/ClosedPullbackUnit.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponentSeshadri.ClosedPullbackUnit.opensEquivalence line 10
  2. lemma OAI.PiExponentSeshadri.ClosedPullbackUnit.preimage_surjective line 13
  3. def OAI.PiExponentSeshadri.ClosedPullbackUnit.additivePreimage line 20
  4. lemma OAI.PiExponentSeshadri.ClosedPullbackUnit.additivePreimage_app line 26
  5. lemma OAI.PiExponentSeshadri.ClosedPullbackUnit.additivePreimage_smul line 34
  6. def OAI.PiExponentSeshadri.ClosedPullbackUnit.modulePreimage line 63
  7. def OAI.PiExponentSeshadri.ClosedPullbackUnit.pushforwardFullyFaithful line 73
  8. theorem OAI.PiExponentSeshadri.ClosedPullbackUnit.counit_isIso line 85
  9. theorem OAI.PiExponentSeshadri.ClosedPullbackUnit.unit_isIso_of_pushforward line 93
  10. lemma OAI.PiExponentSeshadri.ClosedPullbackUnit.subscheme_surjective_of_support_top line 102
  11. theorem OAI.PiExponentSeshadri.ClosedPullbackUnit.subscheme_counit_isIso line 107
  12. theorem OAI.PiExponentSeshadri.ClosedPullbackUnit.subscheme_unit_isIso_of_pushforward line 111