OAI/Geometry/SurfaceImmersion/Whitney/QuadraticCrosscapFactorization.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Every nondegenerate quadratic crosscap is a standard umbrella followed by a target map whose derivative at the origin is invertible.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.standardCrosscap line 16

    Source documentation

    Standard umbrella, with the regular coordinate placed last.

    def standardCrosscap (x : Base) : Base × ℝ := (![x 0*x 1,(x 1)^2],x 0)
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.standardCrosscap_smooth line 18
  3. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.crosscapTargetShear line 27

    Source documentation

    A quadratic target shear with identity differential at the origin.

    def crosscapTargetShear (β : Base × ℝ) (z : Base × ℝ) : Base × ℝ :=
…
  4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.crosscapTargetShear_smooth line 30
  5. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.crosscapTargetShear_fderiv line 34
  6. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.quadratic_crosscap_factorization line 44