FoxDifferential/Completed/FreeProC/QuotientKernelBasis.lean

1import FoxDifferential.Completed.FreeProC.StageApproximation

3/-

4PUBLIC_PAGE_SNAPSHOT

5generated_at: 2026-05-27T09:47:29+09:00

6lean_source: lean4/FoxDifferential/Completed/FreeProC/QuotientKernelBasis.lean

7translation_root: data/translation

8purpose: identifies the local data snapshot used to build pages/

9placement: after imports, never before imports

10-/

11/-!

12# Quotient-kernel neighbourhood bases

14The completed density theorem uses quotient maps out of the completed Fox semidirect product.

15This file adds the standard topological-group conversion from identity-neighbourhood kernel

16bases to the left-coset kernel basis used by closure arguments.

17-/

19namespace FoxDifferential

21noncomputable section

23open scoped Topology

25universe u v

27section QuotientKernelIdentityBasis

29variable {Y : Type u} [Group Y] [TopologicalSpace Y]

30variable {J : Type v} {Q : J → Type*} [∀ j, Group (Q j)]

31variable (π : ∀ j : J, Y →* Q j)

33/-- Quotient kernels form a neighbourhood basis at the identity.

35For every open neighbourhood of `1`, some finite-stage kernel is contained in it. In a

36topological group this is the natural form obtained from finite quotient separation; it implies

37the left-coset basis used by `subset_closure_of_quotientKernel_approximation`. -/

38def HasIdentityQuotientKernelNeighbourhoodBasis : Prop :=

39 ∀ U : Set Y, IsOpen U → (1 : Y) ∈ U →

40 ∃ j : J, ∀ z : Y, z ∈ (π j).ker → z ∈ U

42/-- Identity-neighbourhood quotient kernels give the left quotient-kernel basis. -/

43theorem HasIdentityQuotientKernelNeighbourhoodBasis.to_left

44 [IsTopologicalGroup Y]

45 (hbasis : HasIdentityQuotientKernelNeighbourhoodBasis (Y := Y) π) :

46 HasLeftQuotientKernelNeighbourhoodBasis (Y := Y) π := by

47 intro y U hU hyU

48 let W : Set Y := {z : Y | y * z ∈ U}

49 have hWopen : IsOpen W := by

50 have hmul : Continuous fun z : Y => y * z :=

51 (continuous_const : Continuous fun _ : Y => y).mul continuous_id

52 exact hU.preimage hmul

53 have hWone : (1 : Y) ∈ W := by

54 simp only [Set.mem_setOf_eq, mul_one, hyU, W]

55 rcases hbasis W hWopen hWone with ⟨j, hj⟩

56 refine ⟨j, ?_⟩

57 intro z hz

58 exact hj z hz

60/-- Closure criterion using identity-neighbourhood quotient kernels directly. -/

61theorem subset_closure_of_identityQuotientKernel_approximation

62 [IsTopologicalGroup Y]

63 {S T : Set Y}

64 (hbasis : HasIdentityQuotientKernelNeighbourhoodBasis (Y := Y) π)

65 (happrox :

66 ∀ y : Y, y ∈ T → ∀ j : J,

67 ∃ s : Y, s ∈ S ∧ π j s = π j y) :

68 T ⊆ closure S :=

69 subset_closure_of_quotientKernel_approximation

70 (Y := Y) (S := S) (T := T) π

71 (HasIdentityQuotientKernelNeighbourhoodBasis.to_left (Y := Y) (π := π) hbasis)

72 happrox

74/-- Stage-exact closure criterion with identity-neighbourhood quotient kernels. -/

75theorem subset_closure_of_identityQuotientKernel_stage_exact

76 [IsTopologicalGroup Y]

77 {S T : Set Y}

78 (hbasis : HasIdentityQuotientKernelNeighbourhoodBasis (Y := Y) π)

79 (Sstage Tstage : ∀ j : J, Set (Q j))

80 (hTstage : ∀ y : Y, y ∈ T → ∀ j : J, π j y ∈ Tstage j)

81 (hstage_exact : ∀ j : J, Tstage j ⊆ Sstage j)

82 (hlift_stage : ∀ j : J, ∀ q : Q j, q ∈ Sstage j →

83 ∃ s : Y, s ∈ S ∧ π j s = q) :

84 T ⊆ closure S :=

85 subset_closure_of_quotientKernel_stage_exact

86 (Y := Y) (S := S) (T := T) π

87 (HasIdentityQuotientKernelNeighbourhoodBasis.to_left (Y := Y) (π := π) hbasis)

88 Sstage Tstage hTstage hstage_exact hlift_stage

90end QuotientKernelIdentityBasis

92end

94end FoxDifferential