def immersionRel {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (M : Type u_3) [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H' : Type u_5} [TopologicalSpace H'] (I' : ModelWithCorners ℝ E' H') (M' : Type u_6) [TopologicalSpace M'] [ChartedSpace H' M'] : RelMfld I M I' M'

The relation of immersions for maps between two manifolds.

Equations

• immersionRel I M I' M' = {σ : OneJetBundle I M I' M' | Function.Injective ⇑σ.snd}

@[simp]

theorem mem_immersionRel_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H' : Type u_5} [TopologicalSpace H'] (I' : ModelWithCorners ℝ E' H') {M' : Type u_6} [TopologicalSpace M'] [ChartedSpace H' M'] {σ : OneJetBundle I M I' M'} : σ ∈ immersionRel I M I' M' ↔ Function.Injective ⇑σ.snd

theorem mem_immersionRel_iff' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H' : Type u_5} [TopologicalSpace H'] (I' : ModelWithCorners ℝ E' H') {M' : Type u_6} [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I' (↑⊤) M'] {σ σ' : OneJetBundle I M I' M'} (hσ' : σ' ∈ (chartAt (ModelProd (ModelProd H H') (E →L[ℝ] E')) σ).source) : σ' ∈ immersionRel I M I' M' ↔ Function.Injective ⇑(↑(chartAt (ModelProd (ModelProd H H') (E →L[ℝ] E')) σ) σ').2

A characterisation of the immersion relation in terms of a local chart.

theorem chartAt_image_immersionRel_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H' : Type u_5} [TopologicalSpace H'] (I' : ModelWithCorners ℝ E' H') {M' : Type u_6} [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I' (↑⊤) M'] {σ : OneJetBundle I M I' M'} : ↑(chartAt (ModelProd (ModelProd H H') (E →L[ℝ] E')) σ) '' ((chartAt (ModelProd (ModelProd H H') (E →L[ℝ] E')) σ).source ∩ immersionRel I M I' M') = (chartAt (ModelProd (ModelProd H H') (E →L[ℝ] E')) σ).target ∩ {q : ModelProd (ModelProd H H') (E →L[ℝ] E') | Function.Injective ⇑q.2}

theorem immersionRel_open {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H' : Type u_5} [TopologicalSpace H'] (I' : ModelWithCorners ℝ E' H') {M' : Type u_6} [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I' (↑⊤) M'] [FiniteDimensional ℝ E] : IsOpen (immersionRel I M I' M')

@[simp]

theorem immersionRel_slice_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H' : Type u_5} [TopologicalSpace H'] (I' : ModelWithCorners ℝ E' H') {M' : Type u_6} [TopologicalSpace M'] [ChartedSpace H' M'] {m : M} {m' : M'} {p : DualPair (TangentSpace I m)} {φ : TangentSpace I m →L[ℝ] TangentSpace I' m'} (hφ : Function.Injective ⇑φ) : (immersionRel I M I' M').slice ⟨(m, m'), φ⟩ p = (↑(Submodule.map (↑φ) (↑p.π).ker))ᶜ

theorem immersionRel_ample {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H' : Type u_5} [TopologicalSpace H'] (I' : ModelWithCorners ℝ E' H') {M' : Type u_6} [TopologicalSpace M'] [ChartedSpace H' M'] [FiniteDimensional ℝ E] [FiniteDimensional ℝ E'] (h : Module.finrank ℝ E < Module.finrank ℝ E') : (immersionRel I M I' M').Ample

theorem immersionRel_open_ample {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H' : Type u_5} [TopologicalSpace H'] (I' : ModelWithCorners ℝ E' H') {M' : Type u_6} [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I' (↑⊤) M'] [FiniteDimensional ℝ E] [FiniteDimensional ℝ E'] (h : Module.finrank ℝ E < Module.finrank ℝ E') : IsOpen (immersionRel I M I' M') ∧ (immersionRel I M I' M').Ample

This is lemma lem:open_ample_immersion from the blueprint.

theorem immersionRel_satisfiesHPrincipleWith {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) [I.Boundaryless] (M : Type u_3) [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E'] {H' : Type u_5} [TopologicalSpace H'] (I' : ModelWithCorners ℝ E' H') [I'.Boundaryless] (M' : Type u_6) [MetricSpace M'] [ChartedSpace H' M'] [IsManifold I' (↑⊤) M'] {EP : Type u_7} [NormedAddCommGroup EP] [NormedSpace ℝ EP] [FiniteDimensional ℝ EP] {HP : Type u_8} [TopologicalSpace HP] (IP : ModelWithCorners ℝ EP HP) [IP.Boundaryless] (P : Type u_9) [TopologicalSpace P] [ChartedSpace HP P] [IsManifold IP (↑⊤) P] {C : Set (P × M)} {ε : M → ℝ} [T2Space P] [SigmaCompactSpace P] [T2Space M] [SigmaCompactSpace M] [SigmaCompactSpace M'] (h : Module.finrank ℝ E < Module.finrank ℝ E') (hC : IsClosed C) (hε_pos : ∀ (x : M), 0 < ε x) (hε_cont : Continuous ε) : RelMfld.SatisfiesHPrincipleWith IP (immersionRel I M I' M') C ε

parametric h-principle for immersions.

The inclusion and antipodal map on a sphere are immersions: these results are not used directly, but are good sanity checks.

theorem immersion_inclusion_sphere {n : ℕ} (E : Type u_1) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = n + 1)] : Immersion (modelWithCornersSelf ℝ (ℝ^n)) (modelWithCornersSelf ℝ E) (fun (x : ↑(Metric.sphere 0 1)) => ↑x) ↑⊤

The inclusion of 𝕊^n into ℝ^{n+1} is an immersion.

theorem immersion_antipodal_sphere {n : ℕ} (E : Type u_1) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = n + 1)] : Immersion (modelWithCornersSelf ℝ (ℝ^n)) (modelWithCornersSelf ℝ E) (fun (x : ↑(Metric.sphere 0 1)) => -↑x) ↑⊤

The antipodal map on 𝕊^n ⊆ ℝ^{n+1} is an immersion.

theorem smooth_bs (E : Type u_1) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 3)] : ContMDiff ((modelWithCornersSelf ℝ ℝ).prod (modelWithCornersSelf ℝ (ℝ^2))) (modelWithCornersSelf ℝ E) ↑⊤ fun (p : ℝ × ↑(Metric.sphere 0 1)) => (1 - p.1) • ↑p.2 + p.1 • -↑p.2

noncomputable def formalEversionAux (E : Type u_1) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 3)] (ω : Orientation ℝ E (Fin 3)) : FamilyOneJetSec (modelWithCornersSelf ℝ (ℝ^2)) (↑(Metric.sphere 0 1)) (modelWithCornersSelf ℝ E) E (modelWithCornersSelf ℝ ℝ) ℝ

Equations

• formalEversionAux E ω = familyJoin ⋯ (familyTwist (drop (oneJetExtSec ⟨Subtype.val, ⋯⟩)) (fun (p : ℝ × ↑(Metric.sphere 0 1)) => ω.rot (p.1, ↑p.2)) ⋯)

noncomputable def formalEversionAux2 (E : Type u_1) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 3)] (ω : Orientation ℝ E (Fin 3)) : HtpyFormalSol (immersionRel (modelWithCornersSelf ℝ (ℝ^2)) (↑(Metric.sphere 0 1)) (modelWithCornersSelf ℝ E) E)

A formal eversion of a two-sphere into its ambient Euclidean space.

Equations

• formalEversionAux2 E ω = { toFamilyOneJetSec := formalEversionAux E ω, is_sol' := ⋯ }

noncomputable def formalEversion (E : Type u_1) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 3)] (ω : Orientation ℝ E (Fin 3)) : HtpyFormalSol (immersionRel (modelWithCornersSelf ℝ (ℝ^2)) (↑(Metric.sphere 0 1)) (modelWithCornersSelf ℝ E) E)

Equations

• formalEversion E ω = FamilyFormalSol.reindex (formalEversionAux2 E ω) ⟨smoothStep, formalEversion._proof_1⟩

@[simp]

theorem formalEversion_bs (E : Type u_1) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 3)] (ω : Orientation ℝ E (Fin 3)) (t : ℝ) : ((formalEversion E ω) t).bs = fun (x : ↑(Metric.sphere 0 1)) => (1 - smoothStep t) • ↑x + smoothStep t • -↑x

theorem formalEversion_zero (E : Type u_1) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 3)] (ω : Orientation ℝ E (Fin 3)) (x : ↑(Metric.sphere 0 1)) : ((formalEversion E ω) 0).bs x = ↑x

theorem formalEversion_one (E : Type u_1) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 3)] (ω : Orientation ℝ E (Fin 3)) (x : ↑(Metric.sphere 0 1)) : ((formalEversion E ω) 1).bs x = -↑x

theorem formalEversionHolAtZero (E : Type u_1) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 3)] (ω : Orientation ℝ E (Fin 3)) {t : ℝ} (ht : t < 1 / 4) : ((formalEversion E ω) t).IsHolonomic

theorem formalEversionHolAtOne (E : Type u_1) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 3)] (ω : Orientation ℝ E (Fin 3)) {t : ℝ} (ht : 3 / 4 < t) : ((formalEversion E ω) t).IsHolonomic

theorem formalEversion_hol_near_zero_one (E : Type u_1) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 3)] (ω : Orientation ℝ E (Fin 3)) : ∀ᶠ (s : ℝ × ↑(Metric.sphere 0 1)) in nhdsSet ({0, 1} ×ˢ Set.univ), ((formalEversion E ω) s.1).IsHolonomicAt s.2

theorem ContDiff.inr {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (x : E) (n : ℕ∞) : ContDiff 𝕜 ↑n fun (p : F) => (x, p)

theorem ContDiff.uncurry_left' {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} {G : Type u_5} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] (n : ℕ∞) {f : E × F → G} (hf : ContDiff 𝕜 (↑n) f) (x : E) : ContDiff 𝕜 ↑n fun (p : F) => f (x, p)

theorem ContDiff.uncurry_left {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} {G : Type u_5} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E → F → G} (n : ℕ∞) (hf : ContDiff 𝕜 ↑n ↿f) (x : E) : ContDiff 𝕜 (↑n) (f x)

theorem ContMDiff.prod_left {𝕜 : Type u_6} [NontriviallyNormedField 𝕜] {E : Type u_7} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_8} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_10} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_11} [TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E' H') {M' : Type u_12} [MetricSpace M'] [ChartedSpace H' M'] {n : ℕ∞} (x : M) : ContMDiff I' (I.prod I') ↑n fun (p : M') => (x, p)

theorem ContMDiff.uncurry_left {𝕜 : Type u_6} [NontriviallyNormedField 𝕜] {E : Type u_7} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_8} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_10} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_11} [TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E' H') {M' : Type u_12} [MetricSpace M'] [ChartedSpace H' M'] {EP : Type u_13} [NormedAddCommGroup EP] [NormedSpace 𝕜 EP] {HP : Type u_14} [TopologicalSpace HP] (IP : ModelWithCorners 𝕜 EP HP) {P : Type u_15} [TopologicalSpace P] [ChartedSpace HP P] {n : ℕ∞} {f : M → M' → P} (hf : ContMDiff (I.prod I') IP ↑n ↿f) (x : M) : ContMDiff I' IP (↑n) (f x)

theorem sphere_eversion (E : Type u_1) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 3)] : ∃ (f : ℝ → ↑(Metric.sphere 0 1) → E), ContMDiff ((modelWithCornersSelf ℝ ℝ).prod (modelWithCornersSelf ℝ (ℝ^2))) (modelWithCornersSelf ℝ E) ↑⊤ ↿f ∧ (f 0 = fun (x : ↑(Metric.sphere 0 1)) => ↑x) ∧ (f 1 = fun (x : ↑(Metric.sphere 0 1)) => -↑x) ∧ ∀ (t : ℝ), Immersion (modelWithCornersSelf ℝ (ℝ^2)) (modelWithCornersSelf ℝ E) (f t) ↑⊤

instance instFactEqNatFinrankRealEuclideanSpaceFin_sphereEversion (n : ℕ) : Fact (Module.finrank ℝ (ℝ^n) = n)

def «termℝ^_» : Lean.ParserDescr

Equations

• «termℝ^_» = Lean.ParserDescr.node `«termℝ^_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "ℝ^") (Lean.ParserDescr.cat `term 1023))