FLT.Patching.Utils.Lemmas

source

theorem IsUnit.pi_iff {ι : Type u_2} {M : ι → Type u_1} [(i : ι) → Monoid (M i)] {x : (i : ι) → M i} :

IsUnit x ↔ ∀ (i : ι), IsUnit (x i)

source

theorem forall_prod_iff {ι : Sort u_2} {β : ι → Type u_1} (P : (i : ι) → β i → Prop) [∀ (i : ι), Nonempty (β i)] :

(∀ (i : ι) (y : (i : ι) → β i), P i (y i)) ↔ ∀ (i : ι) (y : β i), P i y

source

🔸 coverage

def Ideal.idealQuotientEquiv {R : Type u_1} [CommRing R] (I : Ideal R) :

Ideal (R ⧸ I) ≃ { J : Ideal R // I ≤ J }

Equations

Instances For

source

📐 coverage

@[simp]

theorem Ideal.idealQuotientEquiv_apply_coe {R : Type u_1} [CommRing R] (I : Ideal R) (J : Ideal (R ⧸ I)) :

↑(I.idealQuotientEquiv J) = comap (Quotient.mk I) J

source

📐 coverage

@[simp]

theorem Ideal.idealQuotientEquiv_symm_apply {R : Type u_1} [CommRing R] (I : Ideal R) (J : { J : Ideal R // I ≤ J }) :

I.idealQuotientEquiv.symm J = map (Quotient.mk I) ↑J

source

🔸 coverage

def Submodule.pi' {ι : Type u_1} {R : ι → Type u_2} {M : ι → Type u_3} [(i : ι) → CommRing (R i)] [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module (R i) (M i)] (N : (i : ι) → Submodule (R i) (M i)) :

Submodule ((i : ι) → R i) ((i : ι) → M i)

Equations

Instances For

source

📐 coverage

@[simp]

theorem Submodule.mem_pi' {ι : Type u_1} {R : ι → Type u_2} {M : ι → Type u_3} [(i : ι) → CommRing (R i)] [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module (R i) (M i)] {N : (i : ι) → Submodule (R i) (M i)} {x : (i : ι) → M i} :

x ∈ pi' N ↔ ∀ (i : ι), x i ∈ N i

source

🔸 coverage

def LinearMap.piMap {ι : Type u_1} {R : ι → Type u_2} {M : ι → Type u_3} [(i : ι) → CommRing (R i)] [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module (R i) (M i)] {N : ι → Type u_4} [(i : ι) → AddCommGroup (N i)] [(i : ι) → Module (R i) (N i)] (f : (i : ι) → M i →ₗ[R i] N i) :

((i : ι) → M i) →ₗ[(i : ι) → R i] (i : ι) → N i

Equations

Instances For

source

📐 coverage

@[simp]

theorem LinearMap.piMap_apply {ι : Type u_1} {R : ι → Type u_2} {M : ι → Type u_3} [(i : ι) → CommRing (R i)] [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module (R i) (M i)] {N : ι → Type u_4} [(i : ι) → AddCommGroup (N i)] [(i : ι) → Module (R i) (N i)] (f : (i : ι) → M i →ₗ[R i] N i) (g : (i : ι) → M i) (i : ι) :

(piMap f) g i = (f i) (g i)

source

🔸 coverage

instance instAlgebraForall_fLT {ι : Type u_4} {R : ι → Type u_5} {A : ι → Type u_6} [(i : ι) → CommSemiring (R i)] [(i : ι) → Semiring (A i)] [(i : ι) → Algebra (R i) (A i)] :

Algebra ((i : ι) → R i) ((i : ι) → A i)

Equations

source

📐 coverage

theorem pi'_jacobson {ι : Type u_1} {R : ι → Type u_2} [(i : ι) → CommRing (R i)] :

(Submodule.pi' fun (i : ι) => ⊥.jacobson) = ⊥.jacobson

source

instance instCompactSpaceQuotientIdeal_fLT {R : Type u_4} [CommRing R] [TopologicalSpace R] [CompactSpace R] (I : Ideal R) :

CompactSpace (R ⧸ I)

source

theorem exists_subgroup_isOpen_and_subset {α : Type u_4} [TopologicalSpace α] [CompactSpace α] [T2Space α] [TotallyDisconnectedSpace α] [CommGroup α] [IsTopologicalGroup α] {U : Set α} (hU : U ∈ nhds 1) :

∃ (G : Subgroup α), IsOpen ↑G ∧ ↑G ⊆ U

source

theorem exists_addSubgroup_isOpen_and_subset {α : Type u_4} [TopologicalSpace α] [CompactSpace α] [T2Space α] [TotallyDisconnectedSpace α] [AddCommGroup α] [IsTopologicalAddGroup α] {U : Set α} (hU : U ∈ nhds 0) :

∃ (G : AddSubgroup α), IsOpen ↑G ∧ ↑G ⊆ U

source

@[simp]

theorem TwoSidedIdeal.span_le' {α : Type u_4} [NonUnitalNonAssocRing α] {s : Set α} {I : TwoSidedIdeal α} :

span s ≤ I ↔ s ⊆ ↑I

source

@[simp]

theorem TwoSidedIdeal.span_neg {α : Type u_4} [NonUnitalNonAssocRing α] (s : Set α) :

span (-s) = span s

source

@[simp]

theorem TwoSidedIdeal.span_singleton_zero {α : Type u_4} [NonUnitalNonAssocRing α] :

span {0} = ⊥

source

theorem TwoSidedIdeal.mem_span_singleton {α : Type u_4} [NonUnitalNonAssocRing α] {x : α} :

x ∈ span {x}

source

🔸 coverage

def TwoSidedIdeal.leAddSubgroup {α : Type u_4} [NonUnitalNonAssocRing α] (G : AddSubgroup α) :

TwoSidedIdeal α

Equations

Instances For

source

📐 coverage

theorem TwoSidedIdeal.leAddSubgroup_subset {α : Type u_4} [NonUnitalNonAssocRing α] (G : AddSubgroup α) :

↑(leAddSubgroup G) ⊆ ↑G

source

📐 coverage

theorem TwoSidedIdeal.mem_leAddSubgroup' {α : Type u_4} [NonUnitalNonAssocRing α] {G : AddSubgroup α} {x : α} :

x ∈ leAddSubgroup G ↔ ↑(span {x}) ⊆ ↑G

source

📐 coverage

theorem TwoSidedIdeal.mem_leAddSubgroup {α : Type u_4} [Ring α] {G : AddSubgroup α} {x : α} :

x ∈ leAddSubgroup G ↔ ∀ (a b : α), a * x * b ∈ G

source

theorem exists_twoSidedIdeal_isOpen_and_subset {α : Type u_4} [TopologicalSpace α] [CompactSpace α] [T2Space α] [TotallyDisconnectedSpace α] [Ring α] [IsTopologicalRing α] {U : Set α} (hU : U ∈ nhds 0) :

∃ (I : TwoSidedIdeal α), IsOpen ↑I ∧ ↑I ⊆ U

source

theorem exists_ideal_isOpen_and_subset {α : Type u_4} [TopologicalSpace α] [CompactSpace α] [T2Space α] [TotallyDisconnectedSpace α] [Ring α] [IsTopologicalRing α] {U : Set α} (hU : U ∈ nhds 0) :

∃ (I : Ideal α), IsOpen ↑I ∧ ↑I ⊆ U

source

@[instance 100]

instance instTotallyDisconnectedSpaceOfDiscreteTopology_fLT {α : Type u_4} [TopologicalSpace α] [DiscreteTopology α] :

TotallyDisconnectedSpace α

source

theorem WellFoundedGT.exists_eq_sup {α : Type u_4} [CompleteLattice α] [WellFoundedGT α] (f : ℕ →o α) :

∃ (i : ℕ), f i = ⨆ (i : ℕ), f i

source

theorem WellFoundedLT.exists_eq_inf {α : Type u_4} [CompleteLattice α] [WellFoundedLT α] (f : ℕ →o αᵒᵈ) :

∃ (i : ℕ), f i = ⨅ (i : ℕ), f i

source

theorem IsLocalRing.maximalIdeal_pow_card_smul_top_le {R : Type u_4} {M : Type u_5} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [AddCommGroup M] [Module R M] (N : Submodule R M) [Finite (M ⧸ N)] :

maximalIdeal R ^ Nat.card (M ⧸ N) • ⊤ ≤ N

source

theorem Submodule.comap_smul_of_le_range {R : Type u_4} {M : Type u_5} {M' : Type u_6} [CommRing R] [AddCommGroup M] [AddCommGroup M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') (S : Submodule R M') (hS : S ≤ f.range) (I : Ideal R) :

comap f (I • S) = I • comap f S ⊔ f.ker

source

theorem Submodule.comap_smul_of_surjective {R : Type u_4} {M : Type u_5} {M' : Type u_6} [CommRing R] [AddCommGroup M] [AddCommGroup M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') (S : Submodule R M') (hS : Function.Surjective ⇑f) (I : Ideal R) :

comap f (I • S) = I • comap f S ⊔ f.ker

source

🔸 coverage

noncomputable def Pi.liftQuotientₗ {ι : Type u_4} {R : Type u_5} {M : Type u_6} [CommRing R] [AddCommGroup M] [Module R M] [Finite ι] (f : (ι → R) →ₗ[R] M) (I : Ideal R) :

(ι → R ⧸ I) →ₗ[R] M ⧸ I • ⊤

Equations

Instances For

source

📐 coverage

theorem Pi.liftQuotientₗ_surjective {ι : Type u_4} {R : Type u_5} {M : Type u_6} [CommRing R] [AddCommGroup M] [Module R M] [Finite ι] (f : (ι → R) →ₗ[R] M) (I : Ideal R) (hf : Function.Surjective ⇑f) :

Function.Surjective ⇑(liftQuotientₗ f I)

source

📐 coverage

theorem Pi.liftQuotientₗ_bijective {ι : Type u_4} {R : Type u_5} {M : Type u_6} [CommRing R] [AddCommGroup M] [Module R M] [Finite ι] (f : (ι → R) →ₗ[R] M) (I : Ideal R) (hf : Function.Surjective ⇑f) (hf' : f.ker ≤ ((Algebra.linearMap R (R ⧸ I)).compLeft ι).ker) :

Function.Bijective ⇑(liftQuotientₗ f I)

source

theorem IsModuleTopology.compactSpace (R : Type u_4) (M : Type u_5) [CommRing R] [TopologicalSpace R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [IsModuleTopology R M] [CompactSpace R] [Module.Finite R M] :

CompactSpace M

source

theorem disjoint_nonZeroDivisors_of_mem_minimalPrimes {R : Type u_4} [CommRing R] (p : Ideal R) (hp : p ∈ minimalPrimes R) :

Disjoint ↑p ↑(nonZeroDivisors R)