OAI/Geometry/EinsteinFour/RationalBettiTransport.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Transport of the actual rational singular-homology dimensions through homeomorphisms. No metric identification or topological model computation is presumed by these statements.

  1. def OAI.PositiveEinsteinFour.Topology.rationalHomologyCongr line 21

    Source documentation

    The singular-homology functor turns a homeomorphism into a rational linear equivalence in every degree.

    def rationalHomologyCongr (h : X ≃ₜ Y) (n : ℕ) :
    rationalHomology X n ≃ₗ[ℚ] rationalHomology Y n :=
…

    Mentions: OAI.PositiveEinsteinFour.Topology.rationalHomology

  2. theorem OAI.PositiveEinsteinFour.Topology.rationalBetti_homeomorph line 27
  3. theorem OAI.PositiveEinsteinFour.Topology.eulerFour_homeomorph line 31