class Module.UniformlyBoundedRank {ι : Type u_1} (R : Type u_2) (M : ι → Type u_3) [CommRing R] [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] : Prop

• cond : ∃ (n : ℕ), ∀ (i : ι), Module.rank (R ⧸ annihilator R (M i)) (M i) < ↑n

noncomputable def Module.UniformlyBoundedRank.bound {ι : Type u_1} (R : Type u_2) (M : ι → Type u_3) [CommRing R] [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] [UniformlyBoundedRank R M] : ℕ

theorem Module.UniformlyBoundedRank.rank_lt_bound {ι : Type u_1} (R : Type u_2) (M : ι → Type u_3) [CommRing R] [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] [UniformlyBoundedRank R M] (i : ι) : Module.rank (R ⧸ annihilator R (M i)) (M i) < ↑(bound R M)

theorem Module.UniformlyBoundedRank.finrank_lt_bound {ι : Type u_1} (R : Type u_2) (M : ι → Type u_3) [CommRing R] [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] [UniformlyBoundedRank R M] (i : ι) : finrank (R ⧸ annihilator R (M i)) (M i) < bound R M

instance instFiniteQuotientIdealAnnihilator_fLT {ι : Type u_1} (R : Type u_2) (M : ι → Type u_3) [CommRing R] [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] [Module.UniformlyBoundedRank R M] [∀ (i : ι), Module.Free (R ⧸ Module.annihilator R (M i)) (M i)] (i : ι) : Module.Finite (R ⧸ Module.annihilator R (M i)) (M i)

instance instFinite_fLT {ι : Type u_1} (R : Type u_2) (M : ι → Type u_3) [CommRing R] [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] [Module.UniformlyBoundedRank R M] [∀ (i : ι), Module.Free (R ⧸ Module.annihilator R (M i)) (M i)] (i : ι) : Module.Finite R (M i)

theorem Module.UniformlyBoundedRank.exists_finsupp_surjective {ι : Type u_1} (R : Type u_2) (M : ι → Type u_3) [CommRing R] [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] [UniformlyBoundedRank R M] [∀ (i : ι), Free (R ⧸ annihilator R (M i)) (M i)] (i : ι) : ∃ (f : (Fin (bound R M) →₀ R) →ₗ[R] M i), Function.Surjective ⇑f

theorem Module.UniformlyBoundedRank.finite_quotient_smul {ι : Type u_1} (R : Type u_2) (M : ι → Type u_3) [CommRing R] [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] [UniformlyBoundedRank R M] [∀ (i : ι), Free (R ⧸ annihilator R (M i)) (M i)] (i : ι) (I : Ideal R) [Finite (R ⧸ I)] : Finite (M i ⧸ I • ⊤)

theorem Module.UniformlyBoundedRank.card_quotient_le {ι : Type u_1} (R : Type u_2) (M : ι → Type u_3) [CommRing R] [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] [UniformlyBoundedRank R M] [∀ (i : ι), Free (R ⧸ annihilator R (M i)) (M i)] (i : ι) (I : Ideal R) [Finite (R ⧸ I)] : Nat.card (M i ⧸ I • ⊤) ≤ Nat.card (R ⧸ I) ^ bound R M

theorem Module.UniformlyBoundedRank.exists_rank {ι : Type u_1} (R : Type u_2) (M : ι → Type u_3) [CommRing R] [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] (F : Ultrafilter ι) [UniformlyBoundedRank R M] [∀ (i : ι), Free (R ⧸ annihilator R (M i)) (M i)] : ∃ (n : ℕ), ∀ᶠ (i : ι) in ↑F, Nonempty (M i ≃ₗ[R] Fin n → R ⧸ annihilator R (M i))

noncomputable def Module.UniformlyBoundedRank.rank {ι : Type u_1} (R : Type u_2) (M : ι → Type u_3) [CommRing R] [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] (F : Ultrafilter ι) [UniformlyBoundedRank R M] [∀ (i : ι), Free (R ⧸ annihilator R (M i)) (M i)] : ℕ

theorem Module.UniformlyBoundedRank.rank_spec {ι : Type u_1} (R : Type u_2) (M : ι → Type u_3) [CommRing R] [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] (F : Ultrafilter ι) [UniformlyBoundedRank R M] [∀ (i : ι), Free (R ⧸ annihilator R (M i)) (M i)] : ∀ᶠ (i : ι) in ↑F, Nonempty (M i ≃ₗ[R] Fin (rank R M F) → R ⧸ annihilator R (M i))

noncomputable def Module.UniformlyBoundedRank.linearMap {ι : Type u_1} (R : Type u_2) (M : ι → Type u_3) [CommRing R] [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] (F : Ultrafilter ι) [UniformlyBoundedRank R M] [∀ (i : ι), Free (R ⧸ annihilator R (M i)) (M i)] (i : ι) : (Fin (rank R M F) → R) →ₗ[R] M i

theorem Module.UniformlyBoundedRank.linearMap_surjective {ι : Type u_1} (R : Type u_2) (M : ι → Type u_3) [CommRing R] [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] (F : Ultrafilter ι) [UniformlyBoundedRank R M] [∀ (i : ι), Free (R ⧸ annihilator R (M i)) (M i)] : ∀ᶠ (i : ι) in ↑F, Function.Surjective ⇑(linearMap R M F i)

theorem Module.UniformlyBoundedRank.linearMap_eq_zero {ι : Type u_1} (R : Type u_2) (M : ι → Type u_3) [CommRing R] [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] (F : Ultrafilter ι) [UniformlyBoundedRank R M] [∀ (i : ι), Free (R ⧸ annihilator R (M i)) (M i)] : ∀ᶠ (i : ι) in ↑F, ∀ (x : Fin (rank R M F) → R), (linearMap R M F i) x = 0 ↔ ∀ (j : Fin (rank R M F)), x j ∈ annihilator R (M i)

@[reducible, inline]

abbrev PatchingModule.Component (R : Type u_1) [CommRing R] {ι : Type u_2} (M : ι → Type u_3) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] (F : Ultrafilter ι) (α : Ideal R) : Type (max u_2 u_3)

def PatchingModule.liftComponent (R : Type u_1) [CommRing R] {ι : Type u_2} (M : ι → Type u_3) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] (F : Ultrafilter ι) (M₀ : Type u_4) [AddCommGroup M₀] [Module R M₀] (α : Ideal R) (f : (i : ι) → M₀ →ₗ[R] M i) : M₀ ⧸ α • ⊤ →ₗ[R] Component R M F α

def OpenIdeals (R : Type u_1) [TopologicalSpace R] [CommRing R] : Type u_1

instance instSemilatticeInfOpenIdeals (R : Type u_1) [TopologicalSpace R] [CommRing R] : SemilatticeInf (OpenIdeals R)

instance instOrderTopOpenIdeals (R : Type u_1) [TopologicalSpace R] [CommRing R] : OrderTop (OpenIdeals R)

@[reducible, inline]

abbrev PatchingModule.componentMap (R : Type u_1) [CommRing R] {ι : Type u_2} (M : ι → Type u_3) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] (F : Ultrafilter ι) {α β : Ideal R} (h : α ≤ β) : Component R M F α →ₗ[R] Component R M F β

def PatchingModule.submodule (R : Type u_1) [TopologicalSpace R] [CommRing R] {ι : Type u_2} (M : ι → Type u_3) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] (F : Ultrafilter ι) : Submodule (ι → R) ((α : OpenIdeals R) → Component R M F ↑α)

theorem PatchingModule.isClosed_submodule (R : Type u_1) [TopologicalSpace R] [CommRing R] {ι : Type u_2} (M : ι → Type u_3) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] (F : Ultrafilter ι) : IsClosed ↑(submodule R M F)

def PatchingModule (R : Type u_1) [TopologicalSpace R] [CommRing R] {ι : Type u_2} (M : ι → Type u_3) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] (F : Ultrafilter ι) : Type (max (max u_1 u_2) u_3)

instance instAddCommGroupPatchingModule (R : Type u_1) [TopologicalSpace R] [CommRing R] {ι : Type u_2} (M : ι → Type u_3) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] (F : Ultrafilter ι) : AddCommGroup (PatchingModule R M F)

instance instModuleForallPatchingModule (R : Type u_1) [TopologicalSpace R] [CommRing R] {ι : Type u_2} (M : ι → Type u_3) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] (F : Ultrafilter ι) : Module (ι → R) (PatchingModule R M F)

instance instModulePatchingModule (R : Type u_1) [TopologicalSpace R] [CommRing R] {ι : Type u_2} (M : ι → Type u_3) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] (F : Ultrafilter ι) : Module R (PatchingModule R M F)

@[simp]

theorem PatchingModule.smul_apply (R : Type u_1) [TopologicalSpace R] [CommRing R] {ι : Type u_2} (M : ι → Type u_3) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] (F : Ultrafilter ι) (r : R) (x : PatchingModule R M F) (α : OpenIdeals R) : ↑(r • x) α = r • ↑x α

instance instIsScalarTowerForallPatchingModule (R : Type u_1) [TopologicalSpace R] [CommRing R] {ι : Type u_2} (M : ι → Type u_3) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] (F : Ultrafilter ι) : IsScalarTower R (ι → R) (PatchingModule R M F)

instance instTopologicalSpacePatchingModule (R : Type u_1) [TopologicalSpace R] [CommRing R] {ι : Type u_2} (M : ι → Type u_3) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] (F : Ultrafilter ι) : TopologicalSpace (PatchingModule R M F)

instance instIsTopologicalAddGroupPatchingModule (R : Type u_1) [TopologicalSpace R] [CommRing R] {ι : Type u_2} (M : ι → Type u_3) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] (F : Ultrafilter ι) : IsTopologicalAddGroup (PatchingModule R M F)

instance instContinuousSMulComponentValIdealIsOpenCoe (R : Type u_1) [TopologicalSpace R] [CommRing R] [IsTopologicalRing R] {ι : Type u_2} (M : ι → Type u_3) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] (F : Ultrafilter ι) (α : OpenIdeals R) : ContinuousSMul R (PatchingModule.Component R M F ↑α)

instance instContinuousSMulPatchingModule (R : Type u_1) [TopologicalSpace R] [CommRing R] [IsTopologicalRing R] {ι : Type u_2} (M : ι → Type u_3) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] (F : Ultrafilter ι) : ContinuousSMul R (PatchingModule R M F)

instance instTotallyDisconnectedSpacePatchingModule (R : Type u_1) [TopologicalSpace R] [CommRing R] {ι : Type u_2} (M : ι → Type u_3) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] (F : Ultrafilter ι) : TotallyDisconnectedSpace (PatchingModule R M F)

instance instT2SpacePatchingModule (R : Type u_1) [TopologicalSpace R] [CommRing R] {ι : Type u_2} (M : ι → Type u_3) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] (F : Ultrafilter ι) : T2Space (PatchingModule R M F)

def PatchingModule.π (R : Type u_1) [TopologicalSpace R] [CommRing R] {ι : Type u_2} (M : ι → Type u_3) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] (F : Ultrafilter ι) (α : OpenIdeals R) : PatchingModule R M F →ₗ[ι → R] Component R M F ↑α

def PatchingModule.ofPi (R : Type u_1) [TopologicalSpace R] [CommRing R] {ι : Type u_2} (M : ι → Type u_3) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] (F : Ultrafilter ι) : (OpenIdeals R → (i : ι) → M i) →ₗ[OpenIdeals R → ι → R] (α : OpenIdeals R) → Component R M F ↑α

@[simp]

theorem PatchingModule.ofPi_apply (R : Type u_1) [TopologicalSpace R] [CommRing R] {ι : Type u_2} (M : ι → Type u_3) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] (F : Ultrafilter ι) (x : OpenIdeals R → (i : ι) → M i) (α : OpenIdeals R) : (ofPi R M F) x α = (UltraProduct.πₗ (fun (x : ι) => R) (fun (i : ι) => M i ⧸ ↑α • ⊤) ↑F) fun (i : ι) => Submodule.Quotient.mk (x α i)

theorem PatchingModule.ofPi_surjective {R : Type u_1} [TopologicalSpace R] [CommRing R] {ι : Type u_2} {M : ι → Type u_3} [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] {F : Ultrafilter ι} : Function.Surjective ⇑(ofPi R M F)

def PatchingModule.incl (R : Type u_1) [TopologicalSpace R] [CommRing R] {ι : Type u_2} (M : ι → Type u_3) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] (F : Ultrafilter ι) : ((i : ι) → M i) →ₗ[ι → R] PatchingModule R M F

@[simp]

theorem PatchingModule.incl_apply (R : Type u_1) [TopologicalSpace R] [CommRing R] {ι : Type u_2} (M : ι → Type u_3) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] (F : Ultrafilter ι) (x : (i : ι) → M i) (α : OpenIdeals R) : ↑((incl R M F) x) α = (UltraProduct.πₗ (fun (x : ι) => R) (fun (i : ι) => M i ⧸ ↑α • ⊤) ↑F) fun (i : ι) => Submodule.Quotient.mk (x i)

instance instFiniteComponentValIdealIsOpenCoeOfUniformlyBoundedRankOfFreeQuotientAnnihilator (R : Type u_1) [TopologicalSpace R] [CommRing R] [IsTopologicalRing R] [CompactSpace R] {ι : Type u_2} (M : ι → Type u_3) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] (F : Ultrafilter ι) {α : OpenIdeals R} [Module.UniformlyBoundedRank R M] [∀ (i : ι), Module.Free (R ⧸ Module.annihilator R (M i)) (M i)] : Finite (PatchingModule.Component R M F ↑α)

@[reducible, inline]

abbrev PatchingModule.componentMapModule (R : Type u_1) [CommRing R] {ι : Type u_2} {M : ι → Type u_3} [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] (F : Ultrafilter ι) {N : ι → Type u_5} [(i : ι) → AddCommGroup (N i)] [(i : ι) → Module R (N i)] (f : (i : ι) → M i →ₗ[R] N i) (α : Ideal R) : Component R M F α →ₗ[ι → R] Component R N F α

theorem PatchingModule.componentMapModule_surjective (R : Type u_1) [CommRing R] {ι : Type u_2} {M : ι → Type u_3} [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] (F : Ultrafilter ι) {N : ι → Type u_5} [(i : ι) → AddCommGroup (N i)] [(i : ι) → Module R (N i)] (f : (i : ι) → M i →ₗ[R] N i) (hf : ∀ (i : ι), Function.Surjective ⇑(f i)) (α : Ideal R) : Function.Surjective ⇑(componentMapModule R F f α)

def PatchingModule.map (R : Type u_1) [TopologicalSpace R] [CommRing R] {ι : Type u_2} {M : ι → Type u_3} [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] (F : Ultrafilter ι) {N : ι → Type u_5} [(i : ι) → AddCommGroup (N i)] [(i : ι) → Module R (N i)] (f : (i : ι) → M i →ₗ[R] N i) : PatchingModule R M F →ₗ[ι → R] PatchingModule R N F

@[simp]

theorem PatchingModule.map_apply (R : Type u_1) [TopologicalSpace R] [CommRing R] {ι : Type u_2} {M : ι → Type u_3} [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] (F : Ultrafilter ι) {N : ι → Type u_5} [(i : ι) → AddCommGroup (N i)] [(i : ι) → Module R (N i)] (f : (i : ι) → M i →ₗ[R] N i) (x : PatchingModule R M F) (α : OpenIdeals R) : ↑((map R F f) x) α = (componentMapModule R F f ↑α) (↑x α)

theorem PatchingModule.map_comp_apply (R : Type u_1) [TopologicalSpace R] [CommRing R] {ι : Type u_2} {M : ι → Type u_3} [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] (F : Ultrafilter ι) {N : ι → Type u_5} [(i : ι) → AddCommGroup (N i)] [(i : ι) → Module R (N i)] {N' : ι → Type u_6} [(i : ι) → AddCommGroup (N' i)] [(i : ι) → Module R (N' i)] (f : (i : ι) → M i →ₗ[R] N i) (g : (i : ι) → N i →ₗ[R] N' i) (x : PatchingModule R M F) : (map R F fun (i : ι) => g i ∘ₗ f i) x = (map R F g) ((map R F f) x)

theorem PatchingModule.map_comp (R : Type u_1) [TopologicalSpace R] [CommRing R] {ι : Type u_2} {M : ι → Type u_3} [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] (F : Ultrafilter ι) {N : ι → Type u_5} [(i : ι) → AddCommGroup (N i)] [(i : ι) → Module R (N i)] {N' : ι → Type u_6} [(i : ι) → AddCommGroup (N' i)] [(i : ι) → Module R (N' i)] (f : (i : ι) → M i →ₗ[R] N i) (g : (i : ι) → N i →ₗ[R] N' i) : (map R F fun (i : ι) => g i ∘ₗ f i) = map R F g ∘ₗ map R F f

@[simp]

theorem PatchingModule.map_id (R : Type u_1) [TopologicalSpace R] [CommRing R] {ι : Type u_2} {M : ι → Type u_3} [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] (F : Ultrafilter ι) : (map R F fun (i : ι) => LinearMap.id) = LinearMap.id

def PatchingModule.mapEquiv (R : Type u_1) [TopologicalSpace R] [CommRing R] {ι : Type u_2} {M : ι → Type u_3} [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] (F : Ultrafilter ι) {N : ι → Type u_5} [(i : ι) → AddCommGroup (N i)] [(i : ι) → Module R (N i)] (f : (i : ι) → M i ≃ₗ[R] N i) : PatchingModule R M F ≃ₗ[ι → R] PatchingModule R N F

@[simp]

theorem PatchingModule.mapEquiv_apply (R : Type u_1) [TopologicalSpace R] [CommRing R] {ι : Type u_2} {M : ι → Type u_3} [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] (F : Ultrafilter ι) {N : ι → Type u_5} [(i : ι) → AddCommGroup (N i)] [(i : ι) → Module R (N i)] (f : (i : ι) → M i ≃ₗ[R] N i) (c : ↥(submodule R M F)) : (mapEquiv R F f) c = ⟨(LinearMap.piMap fun (α : OpenIdeals R) => componentMapModule R F (fun (i : ι) => ↑(f i)) ↑α) ↑c, ⋯⟩

@[simp]

theorem PatchingModule.mapEquiv_symm_apply (R : Type u_1) [TopologicalSpace R] [CommRing R] {ι : Type u_2} {M : ι → Type u_3} [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] (F : Ultrafilter ι) {N : ι → Type u_5} [(i : ι) → AddCommGroup (N i)] [(i : ι) → Module R (N i)] (f : (i : ι) → M i ≃ₗ[R] N i) (a : PatchingModule R N F) : (mapEquiv R F f).symm a = (map R F fun (i : ι) => ↑(f i).symm) a

theorem PatchingModule.map_surjective (R : Type u_1) [TopologicalSpace R] [CommRing R] [IsTopologicalRing R] [CompactSpace R] {ι : Type u_2} {M : ι → Type u_3} [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] (F : Ultrafilter ι) {N : ι → Type u_5} [(i : ι) → AddCommGroup (N i)] [(i : ι) → Module R (N i)] (f : (i : ι) → M i →ₗ[R] N i) [IsLocalRing R] [IsLocalRing.IsAdicTopology R] [Module.UniformlyBoundedRank R M] [∀ (i : ι), Module.Free (R ⧸ Module.annihilator R (M i)) (M i)] (hf : ∀ (i : ι), Function.Surjective ⇑(f i)) : Function.Surjective ⇑(map R F f)

def PatchingModule.toConst (R : Type u_1) [TopologicalSpace R] [CommRing R] {ι : Type u_2} (F : Ultrafilter ι) (M : Type u_5) [AddCommGroup M] [Module R M] : M →ₗ[R] PatchingModule R (fun (x : ι) => M) F

theorem PatchingModule.toConst_surjective (R : Type u_1) [TopologicalSpace R] [CommRing R] [IsTopologicalRing R] [CompactSpace R] {ι : Type u_2} (F : Ultrafilter ι) (M : Type u_5) [AddCommGroup M] [Module R M] [Module.Finite R M] : Function.Surjective ⇑(toConst R F M)

noncomputable def PatchingModule.constEquiv (R : Type u_1) [TopologicalSpace R] [CommRing R] [IsTopologicalRing R] [CompactSpace R] {ι : Type u_2} (F : Ultrafilter ι) [IsLocalRing R] [T2Space R] [IsNoetherianRing R] (M : Type u_5) [AddCommGroup M] [Module R M] [Module.Finite R M] : M ≃ₗ[R] PatchingModule R (fun (x : ι) => M) F

class IsPatchingSystem (R : Type u_1) [TopologicalSpace R] [CommRing R] {ι : Type u_2} (M : ι → Type u_3) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] (F : Filter ι) : Prop

• cond (α : Ideal R) : IsOpen ↑α → ∀ᶠ (i : ι) in F, Module.annihilator R (M i) ≤ α

noncomputable def IsPatchingSystem.linearMap (R : Type u_1) [CommRing R] {ι : Type u_2} (M : ι → Type u_3) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] (F : Ultrafilter ι) [∀ (i : ι), Module.Free (R ⧸ Module.annihilator R (M i)) (M i)] [Module.UniformlyBoundedRank R M] (α : Ideal R) (i : ι) : (Fin (Module.UniformlyBoundedRank.rank R M F) → R ⧸ α) →ₗ[R] M i ⧸ α • ⊤

theorem IsPatchingSystem.linearMap_compLeft (R : Type u_1) [CommRing R] {ι : Type u_2} (M : ι → Type u_3) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] (F : Ultrafilter ι) [∀ (i : ι), Module.Free (R ⧸ Module.annihilator R (M i)) (M i)] [Module.UniformlyBoundedRank R M] (α : Ideal R) (i : ι) (x : Fin (Module.UniformlyBoundedRank.rank R M F) → R) : (linearMap R M F α i) (((Algebra.linearMap R (R ⧸ α)).compLeft (Fin (Module.UniformlyBoundedRank.rank R M F))) x) = Submodule.Quotient.mk ((Module.UniformlyBoundedRank.linearMap R M F i) x)

theorem IsPatchingSystem.linearMap_bijective (R : Type u_1) [TopologicalSpace R] [CommRing R] {ι : Type u_2} (M : ι → Type u_3) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] (F : Ultrafilter ι) [∀ (i : ι), Module.Free (R ⧸ Module.annihilator R (M i)) (M i)] [Module.UniformlyBoundedRank R M] [IsPatchingSystem R M ↑F] (α : Ideal R) (hα : IsOpen ↑α) : ∀ᶠ (i : ι) in ↑F, Function.Bijective ⇑(linearMap R M F α i)

noncomputable def PatchingModule.equivComponent (R : Type u_1) [TopologicalSpace R] [CommRing R] [IsTopologicalRing R] [CompactSpace R] {ι : Type u_2} (M : ι → Type u_3) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] (F : Ultrafilter ι) [∀ (i : ι), Module.Free (R ⧸ Module.annihilator R (M i)) (M i)] [Module.UniformlyBoundedRank R M] [IsPatchingSystem R M ↑F] (α : Ideal R) (hα : IsOpen ↑α) : (Fin (Module.UniformlyBoundedRank.rank R M F) → R ⧸ α) ≃ₗ[R] Component R M F α

noncomputable def PatchingModule.mapOfIsPatchingSystem (R : Type u_1) [TopologicalSpace R] [CommRing R] [IsTopologicalRing R] [CompactSpace R] {ι : Type u_2} (M : ι → Type u_3) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] (F : Ultrafilter ι) [∀ (i : ι), Module.Free (R ⧸ Module.annihilator R (M i)) (M i)] [Module.UniformlyBoundedRank R M] [IsPatchingSystem R M ↑F] : (Fin (Module.UniformlyBoundedRank.rank R M F) → R) →ₗ[R] PatchingModule R M F

theorem PatchingModule.continuous_ofPi (R : Type u_1) [TopologicalSpace R] [CommRing R] [IsTopologicalRing R] [CompactSpace R] {ι : Type u_2} (M : ι → Type u_3) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] (F : Ultrafilter ι) [∀ (i : ι), Module.Free (R ⧸ Module.annihilator R (M i)) (M i)] [Module.UniformlyBoundedRank R M] [IsPatchingSystem R M ↑F] : Continuous ⇑(mapOfIsPatchingSystem R M F)

theorem PatchingModule.mapOfIsPatchingSystem_bijective (R : Type u_1) [TopologicalSpace R] [CommRing R] [IsTopologicalRing R] [CompactSpace R] {ι : Type u_2} (M : ι → Type u_3) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] (F : Ultrafilter ι) [∀ (i : ι), Module.Free (R ⧸ Module.annihilator R (M i)) (M i)] [Module.UniformlyBoundedRank R M] [IsPatchingSystem R M ↑F] [NonarchimedeanRing R] [T2Space R] : Function.Bijective ⇑(mapOfIsPatchingSystem R M F)

instance instFreePatchingModule (R : Type u_1) [TopologicalSpace R] [CommRing R] [IsTopologicalRing R] [CompactSpace R] {ι : Type u_2} (M : ι → Type u_3) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] (F : Ultrafilter ι) [∀ (i : ι), Module.Free (R ⧸ Module.annihilator R (M i)) (M i)] [Module.UniformlyBoundedRank R M] [IsPatchingSystem R M ↑F] [NonarchimedeanRing R] [T2Space R] : Module.Free R (PatchingModule R M F)

instance instFinitePatchingModule (R : Type u_1) [TopologicalSpace R] [CommRing R] [IsTopologicalRing R] [CompactSpace R] {ι : Type u_2} (M : ι → Type u_3) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] (F : Ultrafilter ι) [∀ (i : ι), Module.Free (R ⧸ Module.annihilator R (M i)) (M i)] [Module.UniformlyBoundedRank R M] [IsPatchingSystem R M ↑F] [NonarchimedeanRing R] [T2Space R] : Module.Finite R (PatchingModule R M F)

theorem PatchingModule.rank_patchingModule (R : Type u_1) [TopologicalSpace R] [CommRing R] [IsTopologicalRing R] [CompactSpace R] {ι : Type u_2} (M : ι → Type u_3) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] (F : Ultrafilter ι) [∀ (i : ι), Module.Free (R ⧸ Module.annihilator R (M i)) (M i)] [Module.UniformlyBoundedRank R M] [IsPatchingSystem R M ↑F] [NonarchimedeanRing R] [T2Space R] [Nontrivial R] : Module.rank R (PatchingModule R M F) = ↑(Module.UniformlyBoundedRank.rank R M F)