OAI/Geometry/EinsteinFour/ConnectionPullback.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Metric compatibility under the coordinate change formula for a connection. The matrices here are four-dimensional chart matrices.

  1. theorem OAI.PositiveEinsteinFour.Geometry.pullback_metric_compatibility line 16
  2. def OAI.PositiveEinsteinFour.Geometry.pulledConnection line 27
  3. theorem OAI.PositiveEinsteinFour.Geometry.pulledConnection_equation line 29
  4. theorem OAI.PositiveEinsteinFour.Geometry.pulledConnection_metric_compatibility line 34
  5. def OAI.PositiveEinsteinFour.Geometry.weightedConnection line 41
  6. theorem OAI.PositiveEinsteinFour.Geometry.weightedConnection_torsion line 44
  7. theorem OAI.PositiveEinsteinFour.Geometry.pulledConnection_torsion line 60
  8. theorem OAI.PositiveEinsteinFour.Geometry.matrixPartial_congruence line 71
  9. theorem OAI.PositiveEinsteinFour.Geometry.curvature_intertwining_of_connection line 88

    Source documentation

    The mixed Jacobian derivative cancels from the curvature transformation. The two last premises are exactly the differentiated connection laws.

    theorem curvature_intertwining_of_connection
    (J C₁ C₂ U₁ U₂ P₁ P₂ D₁₂ D₂₁ V₁₂ V₂₁ E : Mat4)
    (h₁ : J * C₁ = P₁ + U₁ * J) (h₂ : J * C₂ = P₂ + U₂ * J)
    (h₁₂ : P₁ * C₂ + J * D₁₂ = E + V₁₂ * J + U₂ * P₁)
    (h₂₁ : P₂ * C₁ + J * D₂₁ = E + V₂₁ * J + U₁ * P₂) :
    J * (D₁₂ - D₂₁ + C₁ * C₂ - C₂ * C₁) =
      (V₁₂ - V₂₁ + U₁ * U₂ - U₂ * U₁) * J := by
…

    Mentions: OAI.PositiveEinsteinFour.Geometry.Mat4