OAI/RepresentationTheory/RestrictedTilting/LocalFreeness.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Weak regularity and local freeness of associated sections.

  1. lemma OAI.FiberFunctorProof.weaklyRegular_pair_iff line 20
  2. theorem OAI.FiberFunctorProof.flat_baseChange_free line 48
  3. lemma OAI.FiberFunctorProof.gluedLattice_regular line 68
  4. lemma OAI.FiberFunctorProof.regular_pair_equiv line 86
  5. theorem OAI.FiberFunctorProof.associatedSections_regular line 112
  6. theorem OAI.FiberFunctorProof.associatedStalk_free line 128