From d4010c775e001722d7f106e781174829223dcfdb Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Mon, 6 Nov 2023 09:58:54 +1100 Subject: [PATCH] remove #align from remaining files --- Mathlib/Data/Set/Card.lean | 92 ----------- Mathlib/FieldTheory/Adjoin.lean | 146 ------------------ Mathlib/GroupTheory/Schreier.lean | 10 -- Mathlib/NumberTheory/Cyclotomic/Basic.lean | 46 ------ Mathlib/RingTheory/IntegralClosure.lean | 115 -------------- Mathlib/Topology/Connected/Basic.lean | 122 --------------- .../Topology/Connected/LocallyConnected.lean | 12 -- .../Connected/TotallyDisconnected.lean | 38 ----- 8 files changed, 581 deletions(-) diff --git a/Mathlib/Data/Set/Card.lean b/Mathlib/Data/Set/Card.lean index 8fa273b37547a..d5ae3781dd058 100644 --- a/Mathlib/Data/Set/Card.lean +++ b/Mathlib/Data/Set/Card.lean @@ -469,7 +469,6 @@ macro_rules /-- The cardinality of `s : Set α` . Has the junk value `0` if `s` is infinite -/ noncomputable def ncard (s : Set α) : ℕ := ENat.toNat s.encard -#align set.ncard Set.ncard theorem ncard_def (s : Set α) : s.ncard = ENat.toNat s.encard := rfl @@ -483,13 +482,11 @@ theorem Finite.cast_ncard_eq (hs : s.Finite) : s.ncard = s.encard := by toFinite_toFinset, toFinset_card, ENat.toNat_coe] have := infinite_coe_iff.2 h rw [ncard, h.encard_eq, Nat.card_eq_zero_of_infinite, ENat.toNat_top] -#align set.nat.card_coe_set_eq Set.Nat.card_coe_set_eq theorem ncard_eq_toFinset_card (s : Set α) (hs : s.Finite := by toFinite_tac) : s.ncard = hs.toFinset.card := by rw [←Nat.card_coe_set_eq, @Nat.card_eq_fintype_card _ hs.fintype, @Finite.card_toFinset _ _ hs.fintype hs] -#align set.ncard_eq_to_finset_card Set.ncard_eq_toFinset_card theorem ncard_eq_toFinset_card' (s : Set α) [Fintype s] : s.ncard = s.toFinset.card := by @@ -502,25 +499,20 @@ theorem encard_le_coe_iff_finite_ncard_le {k : ℕ} : s.encard ≤ k ↔ s.Finit theorem Infinite.ncard (hs : s.Infinite) : s.ncard = 0 := by rw [←Nat.card_coe_set_eq, @Nat.card_eq_zero_of_infinite _ hs.to_subtype] -#align set.infinite.ncard Set.Infinite.ncard theorem ncard_le_of_subset (hst : s ⊆ t) (ht : t.Finite := by toFinite_tac) : s.ncard ≤ t.ncard := by rw [←Nat.cast_le (α := ℕ∞), ht.cast_ncard_eq, (ht.subset hst).cast_ncard_eq] exact encard_mono hst -#align set.ncard_le_of_subset Set.ncard_le_of_subset theorem ncard_mono [Finite α] : @Monotone (Set α) _ _ _ ncard := fun _ _ ↦ ncard_le_of_subset -#align set.ncard_mono Set.ncard_mono @[simp] theorem ncard_eq_zero (hs : s.Finite := by toFinite_tac) : s.ncard = 0 ↔ s = ∅ := by rw [←Nat.cast_inj (R := ℕ∞), hs.cast_ncard_eq, Nat.cast_zero, encard_eq_zero] -#align set.ncard_eq_zero Set.ncard_eq_zero @[simp] theorem ncard_coe_Finset (s : Finset α) : (s : Set α).ncard = s.card := by rw [ncard_eq_toFinset_card _, Finset.finite_toSet_toFinset] -#align set.ncard_coe_finset Set.ncard_coe_Finset theorem ncard_univ (α : Type*) : (univ : Set α).ncard = Nat.card α := by cases' finite_or_infinite α with h h @@ -528,99 +520,80 @@ theorem ncard_univ (α : Type*) : (univ : Set α).ncard = Nat.card α := by rw [ncard_eq_toFinset_card, Finite.toFinset_univ, Finset.card_univ, Nat.card_eq_fintype_card] rw [Nat.card_eq_zero_of_infinite, Infinite.ncard] exact infinite_univ -#align set.ncard_univ Set.ncard_univ @[simp] theorem ncard_empty (α : Type*) : (∅ : Set α).ncard = 0 := by rw [ncard_eq_zero] -#align set.ncard_empty Set.ncard_empty theorem ncard_pos (hs : s.Finite := by toFinite_tac) : 0 < s.ncard ↔ s.Nonempty := by rw [pos_iff_ne_zero, Ne.def, ncard_eq_zero hs, nonempty_iff_ne_empty] -#align set.ncard_pos Set.ncard_pos theorem ncard_ne_zero_of_mem (h : a ∈ s) (hs : s.Finite := by toFinite_tac) : s.ncard ≠ 0 := ((ncard_pos hs).mpr ⟨a, h⟩).ne.symm -#align set.ncard_ne_zero_of_mem Set.ncard_ne_zero_of_mem theorem finite_of_ncard_ne_zero (hs : s.ncard ≠ 0) : s.Finite := s.finite_or_infinite.elim id fun h ↦ (hs h.ncard).elim -#align set.finite_of_ncard_ne_zero Set.finite_of_ncard_ne_zero theorem finite_of_ncard_pos (hs : 0 < s.ncard) : s.Finite := finite_of_ncard_ne_zero hs.ne.symm -#align set.finite_of_ncard_pos Set.finite_of_ncard_pos theorem nonempty_of_ncard_ne_zero (hs : s.ncard ≠ 0) : s.Nonempty := by rw [nonempty_iff_ne_empty]; rintro rfl; simp at hs -#align set.nonempty_of_ncard_ne_zero Set.nonempty_of_ncard_ne_zero @[simp] theorem ncard_singleton (a : α) : ({a} : Set α).ncard = 1 := by simp [ncard_eq_toFinset_card] -#align set.ncard_singleton Set.ncard_singleton theorem ncard_singleton_inter (a : α) (s : Set α) : ({a} ∩ s).ncard ≤ 1 := by rw [←Nat.cast_le (α := ℕ∞), (toFinite _).cast_ncard_eq, Nat.cast_one] apply encard_singleton_inter -#align set.ncard_singleton_inter Set.ncard_singleton_inter section InsertErase @[simp] theorem ncard_insert_of_not_mem (h : a ∉ s) (hs : s.Finite := by toFinite_tac) : (insert a s).ncard = s.ncard + 1 := by rw [←Nat.cast_inj (R := ℕ∞), (hs.insert a).cast_ncard_eq, Nat.cast_add, Nat.cast_one, hs.cast_ncard_eq, encard_insert_of_not_mem h] -#align set.ncard_insert_of_not_mem Set.ncard_insert_of_not_mem theorem ncard_insert_of_mem (h : a ∈ s) : ncard (insert a s) = s.ncard := by rw [insert_eq_of_mem h] -#align set.ncard_insert_of_mem Set.ncard_insert_of_mem theorem ncard_insert_le (a : α) (s : Set α) : (insert a s).ncard ≤ s.ncard + 1 := by obtain hs | hs := s.finite_or_infinite · to_encard_tac; rw [hs.cast_ncard_eq, (hs.insert _).cast_ncard_eq]; apply encard_insert_le rw [(hs.mono (subset_insert a s)).ncard] exact Nat.zero_le _ -#align set.ncard_insert_le Set.ncard_insert_le theorem ncard_insert_eq_ite [Decidable (a ∈ s)] (hs : s.Finite := by toFinite_tac) : ncard (insert a s) = if a ∈ s then s.ncard else s.ncard + 1 := by by_cases h : a ∈ s · rw [ncard_insert_of_mem h, if_pos h] · rw [ncard_insert_of_not_mem h hs, if_neg h] -#align set.ncard_insert_eq_ite Set.ncard_insert_eq_ite theorem ncard_le_ncard_insert (a : α) (s : Set α) : s.ncard ≤ (insert a s).ncard := by classical refine' s.finite_or_infinite.elim (fun h ↦ _) (fun h ↦ by (rw [h.ncard]; exact Nat.zero_le _)) rw [ncard_insert_eq_ite h]; split_ifs <;> simp -#align set.ncard_le_ncard_insert Set.ncard_le_ncard_insert @[simp] theorem ncard_pair (h : a ≠ b) : ({a, b} : Set α).ncard = 2 := by rw [ncard_insert_of_not_mem, ncard_singleton]; simpa -#align set.card_doubleton Set.ncard_pair @[simp] theorem ncard_diff_singleton_add_one (h : a ∈ s) (hs : s.Finite := by toFinite_tac) : (s \ {a}).ncard + 1 = s.ncard := by to_encard_tac; rw [hs.cast_ncard_eq, (hs.diff _).cast_ncard_eq, encard_diff_singleton_add_one h] -#align set.ncard_diff_singleton_add_one Set.ncard_diff_singleton_add_one @[simp] theorem ncard_diff_singleton_of_mem (h : a ∈ s) (hs : s.Finite := by toFinite_tac) : (s \ {a}).ncard = s.ncard - 1 := eq_tsub_of_add_eq (ncard_diff_singleton_add_one h hs) -#align set.ncard_diff_singleton_of_mem Set.ncard_diff_singleton_of_mem theorem ncard_diff_singleton_lt_of_mem (h : a ∈ s) (hs : s.Finite := by toFinite_tac) : (s \ {a}).ncard < s.ncard := by rw [← ncard_diff_singleton_add_one h hs]; apply lt_add_one -#align set.ncard_diff_singleton_lt_of_mem Set.ncard_diff_singleton_lt_of_mem theorem ncard_diff_singleton_le (s : Set α) (a : α) : (s \ {a}).ncard ≤ s.ncard := by obtain hs | hs := s.finite_or_infinite · apply ncard_le_of_subset (diff_subset _ _) hs convert @zero_le ℕ _ _ exact (hs.diff (by simp : Set.Finite {a})).ncard -#align set.ncard_diff_singleton_le Set.ncard_diff_singleton_le theorem pred_ncard_le_ncard_diff_singleton (s : Set α) (a : α) : s.ncard - 1 ≤ (s \ {a}).ncard := by cases' s.finite_or_infinite with hs hs @@ -630,47 +603,38 @@ theorem pred_ncard_le_ncard_diff_singleton (s : Set α) (a : α) : s.ncard - 1 apply Nat.pred_le convert Nat.zero_le _ rw [hs.ncard] -#align set.pred_ncard_le_ncard_diff_singleton Set.pred_ncard_le_ncard_diff_singleton theorem ncard_exchange (ha : a ∉ s) (hb : b ∈ s) : (insert a (s \ {b})).ncard = s.ncard := congr_arg ENat.toNat <| encard_exchange ha hb -#align set.ncard_exchange Set.ncard_exchange theorem ncard_exchange' (ha : a ∉ s) (hb : b ∈ s) : (insert a s \ {b}).ncard = s.ncard := by rw [← ncard_exchange ha hb, ← singleton_union, ← singleton_union, union_diff_distrib, @diff_singleton_eq_self _ b {a} fun h ↦ ha (by rwa [← mem_singleton_iff.mp h])] -#align set.ncard_exchange' Set.ncard_exchange' end InsertErase theorem ncard_image_le (hs : s.Finite := by toFinite_tac) : (f '' s).ncard ≤ s.ncard := by to_encard_tac; rw [hs.cast_ncard_eq, (hs.image _).cast_ncard_eq]; apply encard_image_le -#align set.ncard_image_le Set.ncard_image_le theorem ncard_image_of_injOn (H : Set.InjOn f s) : (f '' s).ncard = s.ncard := congr_arg ENat.toNat <| H.encard_image -#align set.ncard_image_of_inj_on Set.ncard_image_of_injOn theorem injOn_of_ncard_image_eq (h : (f '' s).ncard = s.ncard) (hs : s.Finite := by toFinite_tac) : Set.InjOn f s := by rw [←Nat.cast_inj (R := ℕ∞), hs.cast_ncard_eq, (hs.image _).cast_ncard_eq] at h exact hs.injOn_of_encard_image_eq h -#align set.inj_on_of_ncard_image_eq Set.injOn_of_ncard_image_eq theorem ncard_image_iff (hs : s.Finite := by toFinite_tac) : (f '' s).ncard = s.ncard ↔ Set.InjOn f s := ⟨fun h ↦ injOn_of_ncard_image_eq h hs, ncard_image_of_injOn⟩ -#align set.ncard_image_iff Set.ncard_image_iff theorem ncard_image_of_injective (s : Set α) (H : f.Injective) : (f '' s).ncard = s.ncard := ncard_image_of_injOn fun _ _ _ _ h ↦ H h -#align set.ncard_image_of_injective Set.ncard_image_of_injective theorem ncard_preimage_of_injective_subset_range {s : Set β} (H : f.Injective) (hs : s ⊆ Set.range f) : (f ⁻¹' s).ncard = s.ncard := by rw [← ncard_image_of_injective _ H, image_preimage_eq_iff.mpr hs] -#align set.ncard_preimage_of_injective_subset_range Set.ncard_preimage_of_injective_subset_range theorem fiber_ncard_ne_zero_iff_mem_image {y : β} (hs : s.Finite := by toFinite_tac) : { x ∈ s | f x = y }.ncard ≠ 0 ↔ y ∈ f '' s := by @@ -678,59 +642,48 @@ theorem fiber_ncard_ne_zero_iff_mem_image {y : β} (hs : s.Finite := by toFinite rintro ⟨z, hz, rfl⟩ exact @ncard_ne_zero_of_mem _ ({ x ∈ s | f x = f z }) z (mem_sep hz rfl) (hs.subset (sep_subset _ _)) -#align set.fiber_ncard_ne_zero_iff_mem_image Set.fiber_ncard_ne_zero_iff_mem_image @[simp] theorem ncard_map (f : α ↪ β) : (f '' s).ncard = s.ncard := ncard_image_of_injective _ f.inj' -#align set.ncard_map Set.ncard_map @[simp] theorem ncard_subtype (P : α → Prop) (s : Set α) : { x : Subtype P | (x : α) ∈ s }.ncard = (s ∩ setOf P).ncard := by convert (ncard_image_of_injective _ (@Subtype.coe_injective _ P)).symm ext x simp [←and_assoc, exists_eq_right] -#align set.ncard_subtype Set.ncard_subtype theorem ncard_inter_le_ncard_left (s t : Set α) (hs : s.Finite := by toFinite_tac) : (s ∩ t).ncard ≤ s.ncard := ncard_le_of_subset (inter_subset_left _ _) hs -#align set.ncard_inter_le_ncard_left Set.ncard_inter_le_ncard_left theorem ncard_inter_le_ncard_right (s t : Set α) (ht : t.Finite := by toFinite_tac) : (s ∩ t).ncard ≤ t.ncard := ncard_le_of_subset (inter_subset_right _ _) ht -#align set.ncard_inter_le_ncard_right Set.ncard_inter_le_ncard_right theorem eq_of_subset_of_ncard_le (h : s ⊆ t) (h' : t.ncard ≤ s.ncard) (ht : t.Finite := by toFinite_tac) : s = t := ht.eq_of_subset_of_encard_le h (by rwa [←Nat.cast_le (α := ℕ∞), ht.cast_ncard_eq, (ht.subset h).cast_ncard_eq] at h') -#align set.eq_of_subset_of_ncard_le Set.eq_of_subset_of_ncard_le theorem subset_iff_eq_of_ncard_le (h : t.ncard ≤ s.ncard) (ht : t.Finite := by toFinite_tac) : s ⊆ t ↔ s = t := ⟨fun hst ↦ eq_of_subset_of_ncard_le hst h ht, Eq.subset'⟩ -#align set.subset_iff_eq_of_ncard_le Set.subset_iff_eq_of_ncard_le theorem map_eq_of_subset {f : α ↪ α} (h : f '' s ⊆ s) (hs : s.Finite := by toFinite_tac) : f '' s = s := eq_of_subset_of_ncard_le h (ncard_map _).ge hs -#align set.map_eq_of_subset Set.map_eq_of_subset theorem sep_of_ncard_eq {P : α → Prop} (h : { x ∈ s | P x }.ncard = s.ncard) (ha : a ∈ s) (hs : s.Finite := by toFinite_tac) : P a := sep_eq_self_iff_mem_true.mp (eq_of_subset_of_ncard_le (by simp) h.symm.le hs) _ ha -#align set.sep_of_ncard_eq Set.sep_of_ncard_eq theorem ncard_lt_ncard (h : s ⊂ t) (ht : t.Finite := by toFinite_tac) : s.ncard < t.ncard := by rw [←Nat.cast_lt (α := ℕ∞), ht.cast_ncard_eq, (ht.subset h.subset).cast_ncard_eq] exact ht.encard_lt_encard h -#align set.ncard_lt_ncard Set.ncard_lt_ncard theorem ncard_strictMono [Finite α] : @StrictMono (Set α) _ _ _ ncard := fun _ _ h ↦ ncard_lt_ncard h -#align set.ncard_strict_mono Set.ncard_strictMono theorem ncard_eq_of_bijective {n : ℕ} (f : ∀ i, i < n → α) (hf : ∀ a ∈ s, ∃ i, ∃ h : i < n, f i h = a) (hf' : ∀ (i) (h : i < n), f i h ∈ s) @@ -740,7 +693,6 @@ theorem ncard_eq_of_bijective {n : ℕ} (f : ∀ i, i < n → α) rw [ncard_eq_toFinset_card _ hs] apply Finset.card_eq_of_bijective all_goals simpa -#align set.ncard_eq_of_bijective Set.ncard_eq_of_bijective theorem ncard_congr {t : Set β} (f : ∀ a ∈ s, β) (h₁ : ∀ a ha, f a ha ∈ t) (h₂ : ∀ a b ha hb, f a ha = f b hb → a = b) (h₃ : ∀ b ∈ t, ∃ a ha, f a ha = b) : @@ -757,14 +709,12 @@ theorem ncard_congr {t : Set β} (f : ∀ a ∈ s, β) (h₁ : ∀ a ha, f a ha exact ⟨_, ha, rfl⟩ simp_rw [←Nat.card_coe_set_eq] exact Nat.card_congr (Equiv.ofBijective f' hbij) -#align set.ncard_congr Set.ncard_congr theorem ncard_le_ncard_of_injOn {t : Set β} (f : α → β) (hf : ∀ a ∈ s, f a ∈ t) (f_inj : InjOn f s) (ht : t.Finite := by toFinite_tac) : s.ncard ≤ t.ncard := by have hle := encard_le_encard_of_injOn hf f_inj to_encard_tac; rwa [ht.cast_ncard_eq, (ht.finite_of_encard_le hle).cast_ncard_eq] -#align set.ncard_le_ncard_of_inj_on Set.ncard_le_ncard_of_injOn theorem exists_ne_map_eq_of_ncard_lt_of_maps_to {t : Set β} (hc : t.ncard < s.ncard) {f : α → β} (hf : ∀ a ∈ s, f a ∈ t) (ht : t.Finite := by toFinite_tac) : @@ -772,14 +722,12 @@ theorem exists_ne_map_eq_of_ncard_lt_of_maps_to {t : Set β} (hc : t.ncard < s.n by_contra h' simp only [Ne.def, exists_prop, not_exists, not_and, not_imp_not] at h' exact (ncard_le_ncard_of_injOn f hf h' ht).not_lt hc -#align set.exists_ne_map_eq_of_ncard_lt_of_maps_to Set.exists_ne_map_eq_of_ncard_lt_of_maps_to theorem le_ncard_of_inj_on_range {n : ℕ} (f : ℕ → α) (hf : ∀ i < n, f i ∈ s) (f_inj : ∀ i < n, ∀ j < n, f i = f j → i = j) (hs : s.Finite := by toFinite_tac) : n ≤ s.ncard := by rw [ncard_eq_toFinset_card _ hs] apply Finset.le_card_of_inj_on_range <;> simpa -#align set.le_ncard_of_inj_on_range Set.le_ncard_of_inj_on_range theorem surj_on_of_inj_on_of_ncard_le {t : Set β} (f : ∀ a ∈ s, β) (hf : ∀ a ha, f a ha ∈ t) (hinj : ∀ a₁ a₂ ha₁ ha₂, f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂) (hst : t.ncard ≤ s.ncard) @@ -801,7 +749,6 @@ theorem surj_on_of_inj_on_of_ncard_le {t : Set β} (f : ∀ a ∈ s, β) (hf : rw [mem_toFinset] at ha₁ ha₂ exact hinj _ _ ha₁ ha₂ h rwa [←ncard_eq_toFinset_card', ←ncard_eq_toFinset_card'] -#align set.surj_on_of_inj_on_of_ncard_le Set.surj_on_of_inj_on_of_ncard_le theorem inj_on_of_surj_on_of_ncard_le {t : Set β} (f : ∀ a ∈ s, β) (hf : ∀ a ha, f a ha ∈ t) (hsurj : ∀ b ∈ t, ∃ a ha, b = f a ha) (hst : s.ncard ≤ t.ncard) ⦃a₁ a₂⦄ (ha₁ : a₁ ∈ s) @@ -822,7 +769,6 @@ theorem inj_on_of_surj_on_of_ncard_le {t : Set β} (f : ∀ a ∈ s, β) (hf : (fun a ha ↦ by { rw [mem_toFinset] at ha ⊢; exact hf a ha }) (by simpa) (by { rwa [←ncard_eq_toFinset_card', ←ncard_eq_toFinset_card'] }) a₁ a₂ (by simpa) (by simpa) (by simpa) -#align set.inj_on_of_surj_on_of_ncard_le Set.inj_on_of_surj_on_of_ncard_le section Lattice @@ -830,12 +776,10 @@ theorem ncard_union_add_ncard_inter (s t : Set α) (hs : s.Finite := by toFinite (ht : t.Finite := by toFinite_tac) : (s ∪ t).ncard + (s ∩ t).ncard = s.ncard + t.ncard := by to_encard_tac; rw [hs.cast_ncard_eq, ht.cast_ncard_eq, (hs.union ht).cast_ncard_eq, (hs.subset (inter_subset_left _ _)).cast_ncard_eq, encard_union_add_encard_inter] -#align set.ncard_union_add_ncard_inter Set.ncard_union_add_ncard_inter theorem ncard_inter_add_ncard_union (s t : Set α) (hs : s.Finite := by toFinite_tac) (ht : t.Finite := by toFinite_tac) : (s ∩ t).ncard + (s ∪ t).ncard = s.ncard + t.ncard := by rw [add_comm, ncard_union_add_ncard_inter _ _ hs ht] -#align set.ncard_inter_add_ncard_union Set.ncard_inter_add_ncard_union theorem ncard_union_le (s t : Set α) : (s ∪ t).ncard ≤ s.ncard + t.ncard := by obtain (h | h) := (s ∪ t).finite_or_infinite @@ -845,25 +789,21 @@ theorem ncard_union_le (s t : Set α) : (s ∪ t).ncard ≤ s.ncard + t.ncard := apply encard_union_le rw [h.ncard] apply zero_le -#align set.ncard_union_le Set.ncard_union_le theorem ncard_union_eq (h : Disjoint s t) (hs : s.Finite := by toFinite_tac) (ht : t.Finite := by toFinite_tac) : (s ∪ t).ncard = s.ncard + t.ncard := by to_encard_tac rw [hs.cast_ncard_eq, ht.cast_ncard_eq, (hs.union ht).cast_ncard_eq, encard_union_eq h] -#align set.ncard_union_eq Set.ncard_union_eq theorem ncard_diff_add_ncard_of_subset (h : s ⊆ t) (ht : t.Finite := by toFinite_tac) : (t \ s).ncard + s.ncard = t.ncard := by to_encard_tac rw [ht.cast_ncard_eq, (ht.subset h).cast_ncard_eq, (ht.diff _).cast_ncard_eq, encard_diff_add_encard_of_subset h] -#align set.ncard_diff_add_ncard_eq_ncard Set.ncard_diff_add_ncard_of_subset theorem ncard_diff (h : s ⊆ t) (ht : t.Finite := by toFinite_tac) : (t \ s).ncard = t.ncard - s.ncard := by rw [← ncard_diff_add_ncard_of_subset h ht, add_tsub_cancel_right] -#align set.ncard_diff Set.ncard_diff theorem ncard_le_ncard_diff_add_ncard (s t : Set α) (ht : t.Finite := by toFinite_tac) : s.ncard ≤ (s \ t).ncard + t.ncard := by @@ -873,58 +813,48 @@ theorem ncard_le_ncard_diff_add_ncard (s t : Set α) (ht : t.Finite := by toFini apply encard_le_encard_diff_add_encard convert Nat.zero_le _ rw [hs.ncard] -#align set.ncard_le_ncard_diff_add_ncard Set.ncard_le_ncard_diff_add_ncard theorem le_ncard_diff (s t : Set α) (hs : s.Finite := by toFinite_tac) : t.ncard - s.ncard ≤ (t \ s).ncard := tsub_le_iff_left.mpr (by rw [add_comm]; apply ncard_le_ncard_diff_add_ncard _ _ hs) -#align set.le_ncard_diff Set.le_ncard_diff theorem ncard_diff_add_ncard (s t : Set α) (hs : s.Finite := by toFinite_tac) (ht : t.Finite := by toFinite_tac) : (s \ t).ncard + t.ncard = (s ∪ t).ncard := by rw [←ncard_union_eq disjoint_sdiff_left (hs.diff _) ht, diff_union_self] -#align set.ncard_diff_add_ncard Set.ncard_diff_add_ncard theorem diff_nonempty_of_ncard_lt_ncard (h : s.ncard < t.ncard) (hs : s.Finite := by toFinite_tac) : (t \ s).Nonempty := by rw [Set.nonempty_iff_ne_empty, Ne.def, diff_eq_empty] exact fun h' ↦ h.not_le (ncard_le_of_subset h' hs) -#align set.diff_nonempty_of_ncard_lt_ncard Set.diff_nonempty_of_ncard_lt_ncard theorem exists_mem_not_mem_of_ncard_lt_ncard (h : s.ncard < t.ncard) (hs : s.Finite := by toFinite_tac) : ∃ e, e ∈ t ∧ e ∉ s := diff_nonempty_of_ncard_lt_ncard h hs -#align set.exists_mem_not_mem_of_ncard_lt_ncard Set.exists_mem_not_mem_of_ncard_lt_ncard @[simp] theorem ncard_inter_add_ncard_diff_eq_ncard (s t : Set α) (hs : s.Finite := by toFinite_tac) : (s ∩ t).ncard + (s \ t).ncard = s.ncard := by rw [←ncard_union_eq (disjoint_of_subset_left (inter_subset_right _ _) disjoint_sdiff_right) (hs.inter_of_left _) (hs.diff _), union_comm, diff_union_inter] -#align set.ncard_inter_add_ncard_diff_eq_ncard Set.ncard_inter_add_ncard_diff_eq_ncard theorem ncard_eq_ncard_iff_ncard_diff_eq_ncard_diff (hs : s.Finite := by toFinite_tac) (ht : t.Finite := by toFinite_tac) : s.ncard = t.ncard ↔ (s \ t).ncard = (t \ s).ncard := by rw [← ncard_inter_add_ncard_diff_eq_ncard s t hs, ← ncard_inter_add_ncard_diff_eq_ncard t s ht, inter_comm, add_right_inj] -#align set.ncard_eq_ncard_iff_ncard_diff_eq_ncard_diff Set.ncard_eq_ncard_iff_ncard_diff_eq_ncard_diff theorem ncard_le_ncard_iff_ncard_diff_le_ncard_diff (hs : s.Finite := by toFinite_tac) (ht : t.Finite := by toFinite_tac) : s.ncard ≤ t.ncard ↔ (s \ t).ncard ≤ (t \ s).ncard := by rw [← ncard_inter_add_ncard_diff_eq_ncard s t hs, ← ncard_inter_add_ncard_diff_eq_ncard t s ht, inter_comm, add_le_add_iff_left] -#align set.ncard_le_ncard_iff_ncard_diff_le_ncard_diff Set.ncard_le_ncard_iff_ncard_diff_le_ncard_diff theorem ncard_lt_ncard_iff_ncard_diff_lt_ncard_diff (hs : s.Finite := by toFinite_tac) (ht : t.Finite := by toFinite_tac) : s.ncard < t.ncard ↔ (s \ t).ncard < (t \ s).ncard := by rw [← ncard_inter_add_ncard_diff_eq_ncard s t hs, ← ncard_inter_add_ncard_diff_eq_ncard t s ht, inter_comm, add_lt_add_iff_left] -#align set.ncard_lt_ncard_iff_ncard_diff_lt_ncard_diff Set.ncard_lt_ncard_iff_ncard_diff_lt_ncard_diff theorem ncard_add_ncard_compl (s : Set α) (hs : s.Finite := by toFinite_tac) (hsc : sᶜ.Finite := by toFinite_tac) : s.ncard + sᶜ.ncard = Nat.card α := by rw [← ncard_univ, ← ncard_union_eq (@disjoint_compl_right _ _ s) hs hsc, union_compl_self] -#align set.ncard_add_ncard_compl Set.ncard_add_ncard_compl end Lattice @@ -942,7 +872,6 @@ theorem exists_intermediate_Set (i : ℕ) (h₁ : i + s.ncard ≤ t.ncard) (h₂ rw [add_eq_zero_iff] at h₁' refine' ⟨t, h₂, rfl.subset, _⟩ rw [h₁'.2, h₁'.1, ht.ncard, add_zero] -#align set.exists_intermediate_set Set.exists_intermediate_Set theorem exists_intermediate_set' {m : ℕ} (hs : s.ncard ≤ m) (ht : m ≤ t.ncard) (h : s ⊆ t) : ∃ r : Set α, s ⊆ r ∧ r ⊆ t ∧ r.ncard = m := by @@ -950,14 +879,12 @@ theorem exists_intermediate_set' {m : ℕ} (hs : s.ncard ≤ m) (ht : m ≤ t.nc exists_intermediate_Set (m - s.ncard) (by rwa [tsub_add_cancel_of_le hs]) h rw [tsub_add_cancel_of_le hs] at hc exact ⟨r, hsr, hrt, hc⟩ -#align set.exists_intermediate_set' Set.exists_intermediate_set' /-- We can shrink `s` to any smaller size. -/ theorem exists_smaller_set (s : Set α) (i : ℕ) (h₁ : i ≤ s.ncard) : ∃ t : Set α, t ⊆ s ∧ t.ncard = i := (exists_intermediate_Set i (by simpa) (empty_subset s)).imp fun t ht ↦ ⟨ht.2.1, by simpa using ht.2.2⟩ -#align set.exists_smaller_set Set.exists_smaller_set theorem Infinite.exists_subset_ncard_eq {s : Set α} (hs : s.Infinite) (k : ℕ) : ∃ t, t ⊆ s ∧ t.Finite ∧ t.ncard = k := by @@ -966,7 +893,6 @@ theorem Infinite.exists_subset_ncard_eq {s : Set α} (hs : s.Infinite) (k : ℕ) refine' ⟨Subtype.val '' (t' : Set s), by simp, Finite.image _ (by simp), _⟩ rw [ncard_image_of_injective _ Subtype.coe_injective] simp -#align set.Infinite.exists_subset_ncard_eq Set.Infinite.exists_subset_ncard_eq theorem Infinite.exists_superset_ncard_eq {s t : Set α} (ht : t.Infinite) (hst : s ⊆ t) (hs : s.Finite) {k : ℕ} (hsk : s.ncard ≤ k) : ∃ s', s ⊆ s' ∧ s' ⊆ t ∧ s'.ncard = k := by @@ -974,7 +900,6 @@ theorem Infinite.exists_superset_ncard_eq {s t : Set α} (ht : t.Infinite) (hst refine' ⟨s ∪ s₁, subset_union_left _ _, union_subset hst (hs₁.trans (diff_subset _ _)), _⟩ rwa [ncard_union_eq (disjoint_of_subset_right hs₁ disjoint_sdiff_right) hs hs₁fin, hs₁card, add_tsub_cancel_of_le] -#align set.infinite.exists_supset_ncard_eq Set.Infinite.exists_superset_ncard_eq theorem exists_subset_or_subset_of_two_mul_lt_ncard {n : ℕ} (hst : 2 * n < (s ∪ t).ncard) : ∃ r : Set α, n < r.ncard ∧ (r ⊆ s ∨ r ⊆ t) := by @@ -985,7 +910,6 @@ theorem exists_subset_or_subset_of_two_mul_lt_ncard {n : ℕ} (hst : 2 * n < (s (hu.subset (subset_union_right _ _))] at hst obtain ⟨r', hnr', hr'⟩ := Finset.exists_subset_or_subset_of_two_mul_lt_card hst exact ⟨r', by simpa, by simpa using hr'⟩ -#align set.exists_subset_or_subset_of_two_mul_lt_ncard Set.exists_subset_or_subset_of_two_mul_lt_ncard /-! ### Explicit description of a set from its cardinality -/ @@ -997,7 +921,6 @@ theorem exists_subset_or_subset_of_two_mul_lt_ncard {n : ℕ} (hst : 2 * n < (s simp_rw [Set.ext_iff, mem_singleton_iff] simp only [Finset.ext_iff, mem_toFinset, Finset.mem_singleton] at ha exact ha -#align set.ncard_eq_one Set.ncard_eq_one theorem exists_eq_insert_iff_ncard (hs : s.Finite := by toFinite_tac) : (∃ (a : α) (_ : a ∉ s), insert a s = t) ↔ s ⊆ t ∧ s.ncard + 1 = t.ncard := by @@ -1011,18 +934,15 @@ theorem exists_eq_insert_iff_ncard (hs : s.Finite := by toFinite_tac) : simp only [ht.ncard, exists_prop, add_eq_zero, and_false, iff_false, not_exists, not_and] rintro x - rfl exact ht (hs.insert x) -#align set.exists_eq_insert_iff_ncard Set.exists_eq_insert_iff_ncard theorem ncard_le_one (hs : s.Finite := by toFinite_tac) : s.ncard ≤ 1 ↔ ∀ a ∈ s, ∀ b ∈ s, a = b := by simp_rw [ncard_eq_toFinset_card _ hs, Finset.card_le_one, Finite.mem_toFinset] -#align set.ncard_le_one Set.ncard_le_one theorem ncard_le_one_iff (hs : s.Finite := by toFinite_tac) : s.ncard ≤ 1 ↔ ∀ {a b}, a ∈ s → b ∈ s → a = b := by rw [ncard_le_one hs] tauto -#align set.ncard_le_one_iff Set.ncard_le_one_iff theorem ncard_le_one_iff_eq (hs : s.Finite := by toFinite_tac) : s.ncard ≤ 1 ↔ s = ∅ ∨ ∃ a, s = {a} := by @@ -1034,47 +954,39 @@ theorem ncard_le_one_iff_eq (hs : s.Finite := by toFinite_tac) : · exact (not_mem_empty _ hx).elim simp_rw [mem_singleton_iff] at hx ⊢; subst hx simp only [forall_eq_apply_imp_iff, imp_self, implies_true] -#align set.ncard_le_one_iff_eq Set.ncard_le_one_iff_eq theorem ncard_le_one_iff_subset_singleton [Nonempty α] (hs : s.Finite := by toFinite_tac) : s.ncard ≤ 1 ↔ ∃ x : α, s ⊆ {x} := by simp_rw [ncard_eq_toFinset_card _ hs, Finset.card_le_one_iff_subset_singleton, Finite.toFinset_subset, Finset.coe_singleton] -#align set.ncard_le_one_iff_subset_singleton Set.ncard_le_one_iff_subset_singleton /-- A `Set` of a subsingleton type has cardinality at most one. -/ theorem ncard_le_one_of_subsingleton [Subsingleton α] (s : Set α) : s.ncard ≤ 1 := by rw [ncard_eq_toFinset_card] exact Finset.card_le_one_of_subsingleton _ -#align ncard_le_one_of_subsingleton Set.ncard_le_one_of_subsingleton theorem one_lt_ncard (hs : s.Finite := by toFinite_tac) : 1 < s.ncard ↔ ∃ a ∈ s, ∃ b ∈ s, a ≠ b := by simp_rw [ncard_eq_toFinset_card _ hs, Finset.one_lt_card, Finite.mem_toFinset] -#align set.one_lt_ncard Set.one_lt_ncard theorem one_lt_ncard_iff (hs : s.Finite := by toFinite_tac) : 1 < s.ncard ↔ ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b := by rw [one_lt_ncard hs] simp only [exists_prop, exists_and_left] -#align set.one_lt_ncard_iff Set.one_lt_ncard_iff theorem two_lt_ncard_iff (hs : s.Finite := by toFinite_tac) : 2 < s.ncard ↔ ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c := by simp_rw [ncard_eq_toFinset_card _ hs, Finset.two_lt_card_iff, Finite.mem_toFinset] -#align set.two_lt_ncard_iff Set.two_lt_ncard_iff theorem two_lt_ncard (hs : s.Finite := by toFinite_tac) : 2 < s.ncard ↔ ∃ a ∈ s, ∃ b ∈ s, ∃ c ∈ s, a ≠ b ∧ a ≠ c ∧ b ≠ c := by simp only [two_lt_ncard_iff hs, exists_and_left, exists_prop] -#align set.two_lt_card Set.two_lt_ncard theorem exists_ne_of_one_lt_ncard (hs : 1 < s.ncard) (a : α) : ∃ b, b ∈ s ∧ b ≠ a := by have hsf := (finite_of_ncard_ne_zero (zero_lt_one.trans hs).ne.symm) rw [ncard_eq_toFinset_card _ hsf] at hs simpa only [Finite.mem_toFinset] using Finset.exists_ne_of_one_lt_card hs a -#align set.exists_ne_of_one_lt_ncard Set.exists_ne_of_one_lt_ncard theorem eq_insert_of_ncard_eq_succ {n : ℕ} (h : s.ncard = n + 1) : ∃ a t, a ∉ t ∧ insert a t = s ∧ t.ncard = n := by @@ -1087,27 +999,23 @@ theorem eq_insert_of_ncard_eq_succ {n : ℕ} (h : s.ncard = n + 1) : · simp only [Finset.mem_coe, ext_iff, mem_insert_iff] tauto simp -#align set.eq_insert_of_ncard_eq_succ Set.eq_insert_of_ncard_eq_succ theorem ncard_eq_succ {n : ℕ} (hs : s.Finite := by toFinite_tac) : s.ncard = n + 1 ↔ ∃ a t, a ∉ t ∧ insert a t = s ∧ t.ncard = n := by refine' ⟨eq_insert_of_ncard_eq_succ, _⟩ rintro ⟨a, t, hat, h, rfl⟩ rw [← h, ncard_insert_of_not_mem hat (hs.subset ((subset_insert a t).trans_eq h))] -#align set.ncard_eq_succ Set.ncard_eq_succ theorem ncard_eq_two : s.ncard = 2 ↔ ∃ x y, x ≠ y ∧ s = {x, y} := by rw [←encard_eq_two, ncard_def, ←Nat.cast_inj (R := ℕ∞), Nat.cast_ofNat] refine' ⟨fun h ↦ _, fun h ↦ _⟩ · rwa [ENat.coe_toNat] at h; rintro h'; simp [h'] at h rw [h]; rfl -#align set.ncard_eq_two Set.ncard_eq_two theorem ncard_eq_three : s.ncard = 3 ↔ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z} := by rw [←encard_eq_three, ncard_def, ←Nat.cast_inj (R := ℕ∞), Nat.cast_ofNat] refine' ⟨fun h ↦ _, fun h ↦ _⟩ · rwa [ENat.coe_toNat] at h; rintro h'; simp [h'] at h rw [h]; rfl -#align set.ncard_eq_three Set.ncard_eq_three end ncard diff --git a/Mathlib/FieldTheory/Adjoin.lean b/Mathlib/FieldTheory/Adjoin.lean index 751a80765321e..9351a78e76108 100644 --- a/Mathlib/FieldTheory/Adjoin.lean +++ b/Mathlib/FieldTheory/Adjoin.lean @@ -46,7 +46,6 @@ variable (F : Type*) [Field F] {E : Type*} [Field E] [Algebra F E] (S : Set E) def adjoin : IntermediateField F E := { Subfield.closure (Set.range (algebraMap F E) ∪ S) with algebraMap_mem' := fun x => Subfield.subset_closure (Or.inl (Set.mem_range_self x)) } -#align intermediate_field.adjoin IntermediateField.adjoin end AdjoinDef @@ -59,12 +58,10 @@ theorem adjoin_le_iff {S : Set E} {T : IntermediateField F E} : adjoin F S ≤ T ⟨fun H => le_trans (le_trans (Set.subset_union_right _ _) Subfield.subset_closure) H, fun H => (@Subfield.closure_le E _ (Set.range (algebraMap F E) ∪ S) T.toSubfield).mpr (Set.union_subset (IntermediateField.set_range_subset T) H)⟩ -#align intermediate_field.adjoin_le_iff IntermediateField.adjoin_le_iff theorem gc : GaloisConnection (adjoin F : Set E → IntermediateField F E) (fun (x : IntermediateField F E) => (x : Set E)) := fun _ _ => adjoin_le_iff -#align intermediate_field.gc IntermediateField.gc /-- Galois insertion between `adjoin` and `coe`. -/ def gi : GaloisInsertion (adjoin F : Set E → IntermediateField F E) @@ -73,7 +70,6 @@ def gi : GaloisInsertion (adjoin F : Set E → IntermediateField F E) gc := IntermediateField.gc le_l_u S := (IntermediateField.gc (S : Set E) (adjoin F S)).1 <| le_rfl choice_eq _ _ := copy_eq _ _ _ -#align intermediate_field.gi IntermediateField.gi instance : CompleteLattice (IntermediateField F E) where __ := GaloisInsertion.liftCompleteLattice IntermediateField.gi @@ -89,92 +85,75 @@ instance : Inhabited (IntermediateField F E) := ⟨⊤⟩ theorem coe_bot : ↑(⊥ : IntermediateField F E) = Set.range (algebraMap F E) := rfl -#align intermediate_field.coe_bot IntermediateField.coe_bot theorem mem_bot {x : E} : x ∈ (⊥ : IntermediateField F E) ↔ x ∈ Set.range (algebraMap F E) := Iff.rfl -#align intermediate_field.mem_bot IntermediateField.mem_bot @[simp] theorem bot_toSubalgebra : (⊥ : IntermediateField F E).toSubalgebra = ⊥ := rfl -#align intermediate_field.bot_to_subalgebra IntermediateField.bot_toSubalgebra @[simp] theorem coe_top : ↑(⊤ : IntermediateField F E) = (Set.univ : Set E) := rfl -#align intermediate_field.coe_top IntermediateField.coe_top @[simp] theorem mem_top {x : E} : x ∈ (⊤ : IntermediateField F E) := trivial -#align intermediate_field.mem_top IntermediateField.mem_top @[simp] theorem top_toSubalgebra : (⊤ : IntermediateField F E).toSubalgebra = ⊤ := rfl -#align intermediate_field.top_to_subalgebra IntermediateField.top_toSubalgebra @[simp] theorem top_toSubfield : (⊤ : IntermediateField F E).toSubfield = ⊤ := rfl -#align intermediate_field.top_to_subfield IntermediateField.top_toSubfield @[simp, norm_cast] theorem coe_inf (S T : IntermediateField F E) : (↑(S ⊓ T) : Set E) = (S : Set E) ∩ T := rfl -#align intermediate_field.coe_inf IntermediateField.coe_inf @[simp] theorem mem_inf {S T : IntermediateField F E} {x : E} : x ∈ S ⊓ T ↔ x ∈ S ∧ x ∈ T := Iff.rfl -#align intermediate_field.mem_inf IntermediateField.mem_inf @[simp] theorem inf_toSubalgebra (S T : IntermediateField F E) : (S ⊓ T).toSubalgebra = S.toSubalgebra ⊓ T.toSubalgebra := rfl -#align intermediate_field.inf_to_subalgebra IntermediateField.inf_toSubalgebra @[simp] theorem inf_toSubfield (S T : IntermediateField F E) : (S ⊓ T).toSubfield = S.toSubfield ⊓ T.toSubfield := rfl -#align intermediate_field.inf_to_subfield IntermediateField.inf_toSubfield @[simp, norm_cast] theorem coe_sInf (S : Set (IntermediateField F E)) : (↑(sInf S) : Set E) = sInf ((fun (x : IntermediateField F E) => (x : Set E)) '' S) := rfl -#align intermediate_field.coe_Inf IntermediateField.coe_sInf @[simp] theorem sInf_toSubalgebra (S : Set (IntermediateField F E)) : (sInf S).toSubalgebra = sInf (toSubalgebra '' S) := SetLike.coe_injective <| by simp [Set.sUnion_image] -#align intermediate_field.Inf_to_subalgebra IntermediateField.sInf_toSubalgebra @[simp] theorem sInf_toSubfield (S : Set (IntermediateField F E)) : (sInf S).toSubfield = sInf (toSubfield '' S) := SetLike.coe_injective <| by simp [Set.sUnion_image] -#align intermediate_field.Inf_to_subfield IntermediateField.sInf_toSubfield @[simp, norm_cast] theorem coe_iInf {ι : Sort*} (S : ι → IntermediateField F E) : (↑(iInf S) : Set E) = ⋂ i, S i := by simp [iInf] -#align intermediate_field.coe_infi IntermediateField.coe_iInf @[simp] theorem iInf_toSubalgebra {ι : Sort*} (S : ι → IntermediateField F E) : (iInf S).toSubalgebra = ⨅ i, (S i).toSubalgebra := SetLike.coe_injective <| by simp [iInf] -#align intermediate_field.infi_to_subalgebra IntermediateField.iInf_toSubalgebra @[simp] theorem iInf_toSubfield {ι : Sort*} (S : ι → IntermediateField F E) : (iInf S).toSubfield = ⨅ i, (S i).toSubfield := SetLike.coe_injective <| by simp [iInf] -#align intermediate_field.infi_to_subfield IntermediateField.iInf_toSubfield --Porting note: `left_inv`, `right_inv`, `map_mul'`, `map_add'` and `commutes` were not needed. /-- Construct an algebra isomorphism from an equality of intermediate fields -/ @@ -189,53 +168,44 @@ def equivOfEq {S T : IntermediateField F E} (h : S = T) : S ≃ₐ[F] T := by map_add' := fun _ _ => by ext; simp commutes' := fun _ => by ext; rfl } <;> aesop -#align intermediate_field.equiv_of_eq IntermediateField.equivOfEq @[simp] theorem equivOfEq_symm {S T : IntermediateField F E} (h : S = T) : (equivOfEq h).symm = equivOfEq h.symm := rfl -#align intermediate_field.equiv_of_eq_symm IntermediateField.equivOfEq_symm @[simp] theorem equivOfEq_rfl (S : IntermediateField F E) : equivOfEq (rfl : S = S) = AlgEquiv.refl := by ext; rfl -#align intermediate_field.equiv_of_eq_rfl IntermediateField.equivOfEq_rfl @[simp] theorem equivOfEq_trans {S T U : IntermediateField F E} (hST : S = T) (hTU : T = U) : (equivOfEq hST).trans (equivOfEq hTU) = equivOfEq (_root_.trans hST hTU) := rfl -#align intermediate_field.equiv_of_eq_trans IntermediateField.equivOfEq_trans variable (F E) /-- The bottom intermediate_field is isomorphic to the field. -/ noncomputable def botEquiv : (⊥ : IntermediateField F E) ≃ₐ[F] F := (Subalgebra.equivOfEq _ _ bot_toSubalgebra).trans (Algebra.botEquiv F E) -#align intermediate_field.bot_equiv IntermediateField.botEquiv variable {F E} -- Porting note: this was tagged `simp`. theorem botEquiv_def (x : F) : botEquiv F E (algebraMap F (⊥ : IntermediateField F E) x) = x := by simp -#align intermediate_field.bot_equiv_def IntermediateField.botEquiv_def @[simp] theorem botEquiv_symm (x : F) : (botEquiv F E).symm x = algebraMap F _ x := rfl -#align intermediate_field.bot_equiv_symm IntermediateField.botEquiv_symm noncomputable instance algebraOverBot : Algebra (⊥ : IntermediateField F E) F := (IntermediateField.botEquiv F E).toAlgHom.toRingHom.toAlgebra -#align intermediate_field.algebra_over_bot IntermediateField.algebraOverBot theorem coe_algebraMap_over_bot : (algebraMap (⊥ : IntermediateField F E) F : (⊥ : IntermediateField F E) → F) = IntermediateField.botEquiv F E := rfl -#align intermediate_field.coe_algebra_map_over_bot IntermediateField.coe_algebraMap_over_bot instance isScalarTower_over_bot : IsScalarTower (⊥ : IntermediateField F E) F E := IsScalarTower.of_algebraMap_eq @@ -244,7 +214,6 @@ instance isScalarTower_over_bot : IsScalarTower (⊥ : IntermediateField F E) F obtain ⟨y, rfl⟩ := (botEquiv F E).symm.surjective x rw [coe_algebraMap_over_bot, (botEquiv F E).apply_symm_apply, botEquiv_symm, IsScalarTower.algebraMap_apply F (⊥ : IntermediateField F E) E]) -#align intermediate_field.is_scalar_tower_over_bot IntermediateField.isScalarTower_over_bot /-- The top `IntermediateField` is isomorphic to the field. @@ -252,22 +221,18 @@ This is the intermediate field version of `Subalgebra.topEquiv`. -/ @[simps!] def topEquiv : (⊤ : IntermediateField F E) ≃ₐ[F] E := (Subalgebra.equivOfEq _ _ top_toSubalgebra).trans Subalgebra.topEquiv -#align intermediate_field.top_equiv IntermediateField.topEquiv -- Porting note: this theorem is now generated by the `@[simps!]` above. -#align intermediate_field.top_equiv_symm_apply_coe IntermediateField.topEquiv_symm_apply_coe @[simp] theorem restrictScalars_bot_eq_self (K : IntermediateField F E) : (⊥ : IntermediateField K E).restrictScalars _ = K := SetLike.coe_injective Subtype.range_coe -#align intermediate_field.restrict_scalars_bot_eq_self IntermediateField.restrictScalars_bot_eq_self @[simp] theorem restrictScalars_top {K : Type*} [Field K] [Algebra K E] [Algebra K F] [IsScalarTower K F E] : (⊤ : IntermediateField F E).restrictScalars K = ⊤ := rfl -#align intermediate_field.restrict_scalars_top IntermediateField.restrictScalars_top @[simp] theorem map_bot {K : Type*} [Field K] [Algebra F K] (f : E →ₐ[F] K) : @@ -277,23 +242,19 @@ theorem map_bot {K : Type*} [Field K] [Algebra F K] (f : E →ₐ[F] K) : theorem _root_.AlgHom.fieldRange_eq_map {K : Type*} [Field K] [Algebra F K] (f : E →ₐ[F] K) : f.fieldRange = IntermediateField.map f ⊤ := SetLike.ext' Set.image_univ.symm -#align alg_hom.field_range_eq_map AlgHom.fieldRange_eq_map theorem _root_.AlgHom.map_fieldRange {K L : Type*} [Field K] [Field L] [Algebra F K] [Algebra F L] (f : E →ₐ[F] K) (g : K →ₐ[F] L) : f.fieldRange.map g = (g.comp f).fieldRange := SetLike.ext' (Set.range_comp g f).symm -#align alg_hom.map_field_range AlgHom.map_fieldRange theorem _root_.AlgHom.fieldRange_eq_top {K : Type*} [Field K] [Algebra F K] {f : E →ₐ[F] K} : f.fieldRange = ⊤ ↔ Function.Surjective f := SetLike.ext'_iff.trans Set.range_iff_surjective -#align alg_hom.field_range_eq_top AlgHom.fieldRange_eq_top @[simp] theorem _root_.AlgEquiv.fieldRange_eq_top {K : Type*} [Field K] [Algebra F K] (f : E ≃ₐ[F] K) : (f : E →ₐ[F] K).fieldRange = ⊤ := AlgHom.fieldRange_eq_top.mpr f.surjective -#align alg_equiv.field_range_eq_top AlgEquiv.fieldRange_eq_top end Lattice @@ -304,56 +265,44 @@ variable (F : Type*) [Field F] {E : Type*} [Field E] [Algebra F E] (S : Set E) theorem adjoin_eq_range_algebraMap_adjoin : (adjoin F S : Set E) = Set.range (algebraMap (adjoin F S) E) := Subtype.range_coe.symm -#align intermediate_field.adjoin_eq_range_algebra_map_adjoin IntermediateField.adjoin_eq_range_algebraMap_adjoin theorem adjoin.algebraMap_mem (x : F) : algebraMap F E x ∈ adjoin F S := IntermediateField.algebraMap_mem (adjoin F S) x -#align intermediate_field.adjoin.algebra_map_mem IntermediateField.adjoin.algebraMap_mem theorem adjoin.range_algebraMap_subset : Set.range (algebraMap F E) ⊆ adjoin F S := by intro x hx cases' hx with f hf rw [← hf] exact adjoin.algebraMap_mem F S f -#align intermediate_field.adjoin.range_algebra_map_subset IntermediateField.adjoin.range_algebraMap_subset instance adjoin.fieldCoe : CoeTC F (adjoin F S) where coe x := ⟨algebraMap F E x, adjoin.algebraMap_mem F S x⟩ -#align intermediate_field.adjoin.field_coe IntermediateField.adjoin.fieldCoe theorem subset_adjoin : S ⊆ adjoin F S := fun _ hx => Subfield.subset_closure (Or.inr hx) -#align intermediate_field.subset_adjoin IntermediateField.subset_adjoin instance adjoin.setCoe : CoeTC S (adjoin F S) where coe x := ⟨x, subset_adjoin F S (Subtype.mem x)⟩ -#align intermediate_field.adjoin.set_coe IntermediateField.adjoin.setCoe @[mono] theorem adjoin.mono (T : Set E) (h : S ⊆ T) : adjoin F S ≤ adjoin F T := GaloisConnection.monotone_l gc h -#align intermediate_field.adjoin.mono IntermediateField.adjoin.mono theorem adjoin_contains_field_as_subfield (F : Subfield E) : (F : Set E) ⊆ adjoin F S := fun x hx => adjoin.algebraMap_mem F S ⟨x, hx⟩ -#align intermediate_field.adjoin_contains_field_as_subfield IntermediateField.adjoin_contains_field_as_subfield theorem subset_adjoin_of_subset_left {F : Subfield E} {T : Set E} (HT : T ⊆ F) : T ⊆ adjoin F S := fun x hx => (adjoin F S).algebraMap_mem ⟨x, HT hx⟩ -#align intermediate_field.subset_adjoin_of_subset_left IntermediateField.subset_adjoin_of_subset_left theorem subset_adjoin_of_subset_right {T : Set E} (H : T ⊆ S) : T ⊆ adjoin F S := fun _ hx => subset_adjoin F S (H hx) -#align intermediate_field.subset_adjoin_of_subset_right IntermediateField.subset_adjoin_of_subset_right @[simp] theorem adjoin_empty (F E : Type*) [Field F] [Field E] [Algebra F E] : adjoin F (∅ : Set E) = ⊥ := eq_bot_iff.mpr (adjoin_le_iff.mpr (Set.empty_subset _)) -#align intermediate_field.adjoin_empty IntermediateField.adjoin_empty @[simp] theorem adjoin_univ (F E : Type*) [Field F] [Field E] [Algebra F E] : adjoin F (Set.univ : Set E) = ⊤ := eq_top_iff.mpr <| subset_adjoin _ _ -#align intermediate_field.adjoin_univ IntermediateField.adjoin_univ /-- If `K` is a field with `F ⊆ K` and `S ⊆ K` then `adjoin F S ≤ K`. -/ theorem adjoin_le_subfield {K : Subfield E} (HF : Set.range (algebraMap F E) ⊆ K) (HS : S ⊆ K) : @@ -361,7 +310,6 @@ theorem adjoin_le_subfield {K : Subfield E} (HF : Set.range (algebraMap F E) ⊆ apply Subfield.closure_le.mpr rw [Set.union_subset_iff] exact ⟨HF, HS⟩ -#align intermediate_field.adjoin_le_subfield IntermediateField.adjoin_le_subfield theorem adjoin_subset_adjoin_iff {F' : Type*} [Field F'] [Algebra F' E] {S S' : Set E} : (adjoin F S : Set E) ⊆ adjoin F' S' ↔ @@ -369,7 +317,6 @@ theorem adjoin_subset_adjoin_iff {F' : Type*} [Field F'] [Algebra F' E] {S S' : ⟨fun h => ⟨_root_.trans (adjoin.range_algebraMap_subset _ _) h, _root_.trans (subset_adjoin _ _) h⟩, fun ⟨hF, hS⟩ => (Subfield.closure_le (t := (adjoin F' S').toSubfield)).mpr (Set.union_subset hF hS)⟩ -#align intermediate_field.adjoin_subset_adjoin_iff IntermediateField.adjoin_subset_adjoin_iff /-- `F[S][T] = F[S ∪ T]` -/ theorem adjoin_adjoin_left (T : Set E) : @@ -393,7 +340,6 @@ theorem adjoin_adjoin_left (T : Set E) : exact hx · right exact hx -#align intermediate_field.adjoin_adjoin_left IntermediateField.adjoin_adjoin_left @[simp] theorem adjoin_insert_adjoin (x : E) : @@ -404,13 +350,11 @@ theorem adjoin_insert_adjoin (x : E) : ⟨subset_adjoin _ _ (Set.mem_insert _ _), adjoin_le_iff.mpr (subset_adjoin_of_subset_right _ _ (Set.subset_insert _ _))⟩)) (adjoin.mono _ _ _ (Set.insert_subset_insert (subset_adjoin _ _))) -#align intermediate_field.adjoin_insert_adjoin IntermediateField.adjoin_insert_adjoin /-- `F[S][T] = F[T][S]` -/ theorem adjoin_adjoin_comm (T : Set E) : (adjoin (adjoin F S) T).restrictScalars F = (adjoin (adjoin F T) S).restrictScalars F := by rw [adjoin_adjoin_left, adjoin_adjoin_left, Set.union_comm] -#align intermediate_field.adjoin_adjoin_comm IntermediateField.adjoin_adjoin_comm theorem adjoin_map {E' : Type*} [Field E'] [Algebra F E'] (f : E →ₐ[F] E') : (adjoin F S).map f = adjoin F (f '' S) := by @@ -421,11 +365,9 @@ theorem adjoin_map {E' : Type*} [Field E'] [Algebra F E'] (f : E →ₐ[F] E') : rw [RingHom.map_field_closure, Set.image_union, ← Set.range_comp, ← RingHom.coe_comp, f.comp_algebraMap] rfl -#align intermediate_field.adjoin_map IntermediateField.adjoin_map theorem algebra_adjoin_le_adjoin : Algebra.adjoin F S ≤ (adjoin F S).toSubalgebra := Algebra.adjoin_le (subset_adjoin _ _) -#align intermediate_field.algebra_adjoin_le_adjoin IntermediateField.algebra_adjoin_le_adjoin theorem adjoin_eq_algebra_adjoin (inv_mem : ∀ x ∈ Algebra.adjoin F S, x⁻¹ ∈ Algebra.adjoin F S) : (adjoin F S).toSubalgebra = Algebra.adjoin F S := @@ -435,7 +377,6 @@ theorem adjoin_eq_algebra_adjoin (inv_mem : ∀ x ∈ Algebra.adjoin F S, x⁻¹ inv_mem' := inv_mem } from adjoin_le_iff.mpr Algebra.subset_adjoin) (algebra_adjoin_le_adjoin _ _) -#align intermediate_field.adjoin_eq_algebra_adjoin IntermediateField.adjoin_eq_algebra_adjoin theorem eq_adjoin_of_eq_algebra_adjoin (K : IntermediateField F E) (h : K.toSubalgebra = Algebra.adjoin F S) : K = adjoin F S := by @@ -444,7 +385,6 @@ theorem eq_adjoin_of_eq_algebra_adjoin (K : IntermediateField F E) refine' (adjoin_eq_algebra_adjoin F _ _).symm intro x convert K.inv_mem (x := x) <;> rw [← h] <;> rfl -#align intermediate_field.eq_adjoin_of_eq_algebra_adjoin IntermediateField.eq_adjoin_of_eq_algebra_adjoin @[elab_as_elim] @@ -454,7 +394,6 @@ theorem adjoin_induction {s : Set E} {p : E → Prop} {x} (h : x ∈ adjoin F s) p x := Subfield.closure_induction h (fun x hx => Or.casesOn hx (fun ⟨x, hx⟩ => hx ▸ Hmap x) (Hs x)) ((algebraMap F E).map_one ▸ Hmap 1) Hadd Hneg Hinv Hmul -#align intermediate_field.adjoin_induction IntermediateField.adjoin_induction /- Porting note (kmill): this notation is replacing the typeclass-based one I had previously written, and it gives true `{x₁, x₂, ..., xₙ}` sets in the `adjoin` term. -/ @@ -505,31 +444,25 @@ variable (α : E) -- Porting note: in all the theorems below, mathport translated `F⟮α⟯` into `F⟮⟯`. theorem mem_adjoin_simple_self : α ∈ F⟮α⟯ := subset_adjoin F {α} (Set.mem_singleton α) -#align intermediate_field.mem_adjoin_simple_self IntermediateField.mem_adjoin_simple_self /-- generator of `F⟮α⟯` -/ def AdjoinSimple.gen : F⟮α⟯ := ⟨α, mem_adjoin_simple_self F α⟩ -#align intermediate_field.adjoin_simple.gen IntermediateField.AdjoinSimple.gen @[simp] theorem AdjoinSimple.algebraMap_gen : algebraMap F⟮α⟯ E (AdjoinSimple.gen F α) = α := rfl -#align intermediate_field.adjoin_simple.algebra_map_gen IntermediateField.AdjoinSimple.algebraMap_gen @[simp] theorem AdjoinSimple.isIntegral_gen : IsIntegral F (AdjoinSimple.gen F α) ↔ IsIntegral F α := by conv_rhs => rw [← AdjoinSimple.algebraMap_gen F α] rw [isIntegral_algebraMap_iff (algebraMap F⟮α⟯ E).injective] -#align intermediate_field.adjoin_simple.is_integral_gen IntermediateField.AdjoinSimple.isIntegral_gen theorem adjoin_simple_adjoin_simple (β : E) : F⟮α⟯⟮β⟯.restrictScalars F = F⟮α, β⟯ := adjoin_adjoin_left _ _ _ -#align intermediate_field.adjoin_simple_adjoin_simple IntermediateField.adjoin_simple_adjoin_simple theorem adjoin_simple_comm (β : E) : F⟮α⟯⟮β⟯.restrictScalars F = F⟮β⟯⟮α⟯.restrictScalars F := adjoin_adjoin_comm _ _ _ -#align intermediate_field.adjoin_simple_comm IntermediateField.adjoin_simple_comm variable {F} {α} @@ -540,14 +473,12 @@ theorem adjoin_algebraic_toSubalgebra {S : Set E} (hS : ∀ x ∈ S, IsAlgebraic rwa [← le_integralClosure_iff_isIntegral, Algebra.adjoin_le_iff] have := isField_of_isIntegral_of_isField' this (Field.toIsField F) rw [← ((Algebra.adjoin F S).toIntermediateField' this).eq_adjoin_of_eq_algebra_adjoin F S] <;> rfl -#align intermediate_field.adjoin_algebraic_to_subalgebra IntermediateField.adjoin_algebraic_toSubalgebra theorem adjoin_simple_toSubalgebra_of_integral (hα : IsIntegral F α) : F⟮α⟯.toSubalgebra = Algebra.adjoin F {α} := by apply adjoin_algebraic_toSubalgebra rintro x (rfl : x = α) rwa [isAlgebraic_iff_isIntegral] -#align intermediate_field.adjoin_simple_to_subalgebra_of_integral IntermediateField.adjoin_simple_toSubalgebra_of_integral theorem isSplittingField_iff {p : F[X]} {K : IntermediateField F E} : p.IsSplittingField F K ↔ p.Splits (algebraMap F K) ∧ K = adjoin F (p.rootSet E) := by @@ -557,12 +488,10 @@ theorem isSplittingField_iff {p : F[X]} {K : IntermediateField F E} : rw [adjoin_algebraic_toSubalgebra fun x => isAlgebraic_of_mem_rootSet] refine' fun hp => (adjoin_rootSet_eq_range hp K.val).symm.trans _ rw [← K.range_val, eq_comm] -#align intermediate_field.is_splitting_field_iff IntermediateField.isSplittingField_iff theorem adjoin_rootSet_isSplittingField {p : F[X]} (hp : p.Splits (algebraMap F E)) : p.IsSplittingField F (adjoin F (p.rootSet E)) := isSplittingField_iff.mpr ⟨splits_of_splits hp fun _ hx => subset_adjoin F (p.rootSet E) hx, rfl⟩ -#align intermediate_field.adjoin_root_set_is_splitting_field IntermediateField.adjoin_rootSet_isSplittingField open scoped BigOperators @@ -580,14 +509,12 @@ theorem isSplittingField_iSup {ι : Type*} {t : ι → IntermediateField F E} {p _⟩ simp only [rootSet_prod p s h0, ← Set.iSup_eq_iUnion, (@gc F _ E _ _).l_iSup₂] exact iSup_congr fun i => iSup_congr fun hi => (h i hi).2 -#align intermediate_field.is_splitting_field_supr IntermediateField.isSplittingField_iSup open Set CompleteLattice /- Porting note: this was tagged `simp`, but the LHS can be simplified now that the notation has been improved. -/ theorem adjoin_simple_le_iff {K : IntermediateField F E} : F⟮α⟯ ≤ K ↔ α ∈ K := by simp -#align intermediate_field.adjoin_simple_le_iff IntermediateField.adjoin_simple_le_iff /-- Adjoining a single element is compact in the lattice of intermediate fields. -/ theorem adjoin_simple_isCompactElement (x : E) : IsCompactElement F⟮x⟯ := by @@ -617,7 +544,6 @@ theorem adjoin_simple_isCompactElement (x : E) : IsCompactElement F⟮x⟯ := by simpa [hE1] using hx obtain ⟨-, ⟨E, rfl⟩, -, ⟨hE, rfl⟩, hx⟩ := key hx exact ⟨E, hE, hx⟩ -#align intermediate_field.adjoin_simple_is_compact_element IntermediateField.adjoin_simple_isCompactElement -- Porting note: original proof times out. /-- Adjoining a finite subset is compact in the lattice of intermediate fields. -/ @@ -630,12 +556,10 @@ theorem adjoin_finset_isCompactElement (S : Finset E) : (iSup_le fun x => iSup_le fun hx => adjoin_simple_le_iff.mpr (subset_adjoin F S hx)) rw [key, ← Finset.sup_eq_iSup] exact finset_sup_compact_of_compact S fun x _ => adjoin_simple_isCompactElement x -#align intermediate_field.adjoin_finset_is_compact_element IntermediateField.adjoin_finset_isCompactElement /-- Adjoining a finite subset is compact in the lattice of intermediate fields. -/ theorem adjoin_finite_isCompactElement {S : Set E} (h : S.Finite) : IsCompactElement (adjoin F S) := Finite.coe_toFinset h ▸ adjoin_finset_isCompactElement h.toFinset -#align intermediate_field.adjoin_finite_is_compact_element IntermediateField.adjoin_finite_isCompactElement /-- The lattice of intermediate fields is compactly generated. -/ instance : IsCompactlyGenerated (IntermediateField F E) := @@ -652,7 +576,6 @@ theorem exists_finset_of_mem_iSup {ι : Type*} {f : ι → IntermediateField F E (IntermediateField F E) f simp only [adjoin_simple_le_iff] at this exact this hx -#align intermediate_field.exists_finset_of_mem_supr IntermediateField.exists_finset_of_mem_iSup theorem exists_finset_of_mem_supr' {ι : Type*} {f : ι → IntermediateField F E} {x : E} (hx : x ∈ ⨆ i, f i) : ∃ s : Finset (Σ i, f i), x ∈ ⨆ i ∈ s, F⟮(i.2 : E)⟯ := by @@ -660,7 +583,6 @@ theorem exists_finset_of_mem_supr' {ι : Type*} {f : ι → IntermediateField F refine' exists_finset_of_mem_iSup (SetLike.le_def.mp (iSup_le (fun i => _)) hx) intro x h exact SetLike.le_def.mp (le_iSup_of_le ⟨i, x, h⟩ (by simp)) (mem_adjoin_simple_self F x) -#align intermediate_field.exists_finset_of_mem_supr' IntermediateField.exists_finset_of_mem_supr' theorem exists_finset_of_mem_supr'' {ι : Type*} {f : ι → IntermediateField F E} (h : ∀ i, Algebra.IsAlgebraic F (f i)) {x : E} (hx : x ∈ ⨆ i, f i) : @@ -673,7 +595,6 @@ theorem exists_finset_of_mem_supr'' {ι : Type*} {f : ι → IntermediateField F · rw [IntermediateField.minpoly_eq, Subtype.coe_mk] · rw [mem_rootSet_of_ne, minpoly.aeval] exact minpoly.ne_zero (isIntegral_iff.mp (isAlgebraic_iff_isIntegral.mp (h i ⟨x1, hx1⟩))) -#align intermediate_field.exists_finset_of_mem_supr'' IntermediateField.exists_finset_of_mem_supr'' end AdjoinSimple @@ -686,32 +607,26 @@ variable {F : Type*} [Field F] {E : Type*} [Field E] [Algebra F E] {α : E} {S : @[simp] theorem adjoin_eq_bot_iff : adjoin F S = ⊥ ↔ S ⊆ (⊥ : IntermediateField F E) := by rw [eq_bot_iff, adjoin_le_iff]; rfl -#align intermediate_field.adjoin_eq_bot_iff IntermediateField.adjoin_eq_bot_iff /- Porting note: this was tagged `simp`. -/ theorem adjoin_simple_eq_bot_iff : F⟮α⟯ = ⊥ ↔ α ∈ (⊥ : IntermediateField F E) := by simp -#align intermediate_field.adjoin_simple_eq_bot_iff IntermediateField.adjoin_simple_eq_bot_iff @[simp] theorem adjoin_zero : F⟮(0 : E)⟯ = ⊥ := adjoin_simple_eq_bot_iff.mpr (zero_mem ⊥) -#align intermediate_field.adjoin_zero IntermediateField.adjoin_zero @[simp] theorem adjoin_one : F⟮(1 : E)⟯ = ⊥ := adjoin_simple_eq_bot_iff.mpr (one_mem ⊥) -#align intermediate_field.adjoin_one IntermediateField.adjoin_one @[simp] theorem adjoin_int (n : ℤ) : F⟮(n : E)⟯ = ⊥ := by refine' adjoin_simple_eq_bot_iff.mpr (coe_int_mem ⊥ n) -#align intermediate_field.adjoin_int IntermediateField.adjoin_int @[simp] theorem adjoin_nat (n : ℕ) : F⟮(n : E)⟯ = ⊥ := adjoin_simple_eq_bot_iff.mpr (coe_nat_mem ⊥ n) -#align intermediate_field.adjoin_nat IntermediateField.adjoin_nat section AdjoinRank @@ -723,38 +638,30 @@ variable {K L : IntermediateField F E} theorem rank_eq_one_iff : Module.rank F K = 1 ↔ K = ⊥ := by rw [← toSubalgebra_eq_iff, ← rank_eq_rank_subalgebra, Subalgebra.rank_eq_one_iff, bot_toSubalgebra] -#align intermediate_field.rank_eq_one_iff IntermediateField.rank_eq_one_iff @[simp] theorem finrank_eq_one_iff : finrank F K = 1 ↔ K = ⊥ := by rw [← toSubalgebra_eq_iff, ← finrank_eq_finrank_subalgebra, Subalgebra.finrank_eq_one_iff, bot_toSubalgebra] -#align intermediate_field.finrank_eq_one_iff IntermediateField.finrank_eq_one_iff @[simp] theorem rank_bot : Module.rank F (⊥ : IntermediateField F E) = 1 := by rw [rank_eq_one_iff] -#align intermediate_field.rank_bot IntermediateField.rank_bot @[simp] theorem finrank_bot : finrank F (⊥ : IntermediateField F E) = 1 := by rw [finrank_eq_one_iff] -#align intermediate_field.finrank_bot IntermediateField.finrank_bot theorem rank_adjoin_eq_one_iff : Module.rank F (adjoin F S) = 1 ↔ S ⊆ (⊥ : IntermediateField F E) := Iff.trans rank_eq_one_iff adjoin_eq_bot_iff -#align intermediate_field.rank_adjoin_eq_one_iff IntermediateField.rank_adjoin_eq_one_iff theorem rank_adjoin_simple_eq_one_iff : Module.rank F F⟮α⟯ = 1 ↔ α ∈ (⊥ : IntermediateField F E) := by rw [rank_adjoin_eq_one_iff]; exact Set.singleton_subset_iff -#align intermediate_field.rank_adjoin_simple_eq_one_iff IntermediateField.rank_adjoin_simple_eq_one_iff theorem finrank_adjoin_eq_one_iff : finrank F (adjoin F S) = 1 ↔ S ⊆ (⊥ : IntermediateField F E) := Iff.trans finrank_eq_one_iff adjoin_eq_bot_iff -#align intermediate_field.finrank_adjoin_eq_one_iff IntermediateField.finrank_adjoin_eq_one_iff theorem finrank_adjoin_simple_eq_one_iff : finrank F F⟮α⟯ = 1 ↔ α ∈ (⊥ : IntermediateField F E) := by rw [finrank_adjoin_eq_one_iff]; exact Set.singleton_subset_iff -#align intermediate_field.finrank_adjoin_simple_eq_one_iff IntermediateField.finrank_adjoin_simple_eq_one_iff /-- If `F⟮x⟯` has dimension `1` over `F` for every `x ∈ E` then `F = E`. -/ theorem bot_eq_top_of_rank_adjoin_eq_one (h : ∀ x : E, Module.rank F F⟮x⟯ = 1) : @@ -762,36 +669,30 @@ theorem bot_eq_top_of_rank_adjoin_eq_one (h : ∀ x : E, Module.rank F F⟮x⟯ ext y rw [iff_true_right IntermediateField.mem_top] exact rank_adjoin_simple_eq_one_iff.mp (h y) -#align intermediate_field.bot_eq_top_of_rank_adjoin_eq_one IntermediateField.bot_eq_top_of_rank_adjoin_eq_one theorem bot_eq_top_of_finrank_adjoin_eq_one (h : ∀ x : E, finrank F F⟮x⟯ = 1) : (⊥ : IntermediateField F E) = ⊤ := by ext y rw [iff_true_right IntermediateField.mem_top] exact finrank_adjoin_simple_eq_one_iff.mp (h y) -#align intermediate_field.bot_eq_top_of_finrank_adjoin_eq_one IntermediateField.bot_eq_top_of_finrank_adjoin_eq_one theorem subsingleton_of_rank_adjoin_eq_one (h : ∀ x : E, Module.rank F F⟮x⟯ = 1) : Subsingleton (IntermediateField F E) := subsingleton_of_bot_eq_top (bot_eq_top_of_rank_adjoin_eq_one h) -#align intermediate_field.subsingleton_of_rank_adjoin_eq_one IntermediateField.subsingleton_of_rank_adjoin_eq_one theorem subsingleton_of_finrank_adjoin_eq_one (h : ∀ x : E, finrank F F⟮x⟯ = 1) : Subsingleton (IntermediateField F E) := subsingleton_of_bot_eq_top (bot_eq_top_of_finrank_adjoin_eq_one h) -#align intermediate_field.subsingleton_of_finrank_adjoin_eq_one IntermediateField.subsingleton_of_finrank_adjoin_eq_one /-- If `F⟮x⟯` has dimension `≤1` over `F` for every `x ∈ E` then `F = E`. -/ theorem bot_eq_top_of_finrank_adjoin_le_one [FiniteDimensional F E] (h : ∀ x : E, finrank F F⟮x⟯ ≤ 1) : (⊥ : IntermediateField F E) = ⊤ := by apply bot_eq_top_of_finrank_adjoin_eq_one exact fun x => by linarith [h x, show 0 < finrank F F⟮x⟯ from finrank_pos] -#align intermediate_field.bot_eq_top_of_finrank_adjoin_le_one IntermediateField.bot_eq_top_of_finrank_adjoin_le_one theorem subsingleton_of_finrank_adjoin_le_one [FiniteDimensional F E] (h : ∀ x : E, finrank F F⟮x⟯ ≤ 1) : Subsingleton (IntermediateField F E) := subsingleton_of_bot_eq_top (bot_eq_top_of_finrank_adjoin_le_one h) -#align intermediate_field.subsingleton_of_finrank_adjoin_le_one IntermediateField.subsingleton_of_finrank_adjoin_le_one end AdjoinRank @@ -806,14 +707,12 @@ variable {K : Type*} [Field K] [Algebra F K] theorem minpoly_gen (α : E) : minpoly F (AdjoinSimple.gen F α) = minpoly F α := by rw [← minpoly.algebraMap_eq (algebraMap F⟮α⟯ E).injective, AdjoinSimple.algebraMap_gen] -#align intermediate_field.minpoly_gen IntermediateField.minpoly_genₓ theorem aeval_gen_minpoly (α : E) : aeval (AdjoinSimple.gen F α) (minpoly F α) = 0 := by ext convert minpoly.aeval F α conv in aeval α => rw [← AdjoinSimple.algebraMap_gen F α] exact (aeval_algebraMap_apply E (AdjoinSimple.gen F α) _).symm -#align intermediate_field.aeval_gen_minpoly IntermediateField.aeval_gen_minpoly --Porting note: original proof used `Exists.cases_on`. /-- algebra isomorphism between `AdjoinRoot` and `F⟮α⟯` -/ @@ -840,12 +739,10 @@ noncomputable def adjoinRootEquivAdjoin (h : IsIntegral F α) : -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 erw [RingHom.comp_apply, AdjoinRoot.lift_root (aeval_gen_minpoly F α)] rfl) -#align intermediate_field.adjoin_root_equiv_adjoin IntermediateField.adjoinRootEquivAdjoin theorem adjoinRootEquivAdjoin_apply_root (h : IsIntegral F α) : adjoinRootEquivAdjoin F h (AdjoinRoot.root (minpoly F α)) = AdjoinSimple.gen F α := AdjoinRoot.lift_root (aeval_gen_minpoly F α) -#align intermediate_field.adjoin_root_equiv_adjoin_apply_root IntermediateField.adjoinRootEquivAdjoin_apply_root section PowerBasis @@ -856,7 +753,6 @@ where `d` is the degree of the minimal polynomial of `x`. -/ noncomputable def powerBasisAux {x : L} (hx : IsIntegral K x) : Basis (Fin (minpoly K x).natDegree) K K⟮x⟯ := (AdjoinRoot.powerBasis (minpoly.ne_zero hx)).basis.map (adjoinRootEquivAdjoin K hx).toLinearEquiv -#align intermediate_field.power_basis_aux IntermediateField.powerBasisAux /-- The power basis `1, x, ..., x ^ (d - 1)` for `K⟮x⟯`, where `d` is the degree of the minimal polynomial of `x`. -/ @@ -869,28 +765,23 @@ noncomputable def adjoin.powerBasis {x : L} (hx : IsIntegral K x) : PowerBasis K -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 erw [powerBasisAux, Basis.map_apply, PowerBasis.basis_eq_pow, AlgEquiv.toLinearEquiv_apply, AlgEquiv.map_pow, AdjoinRoot.powerBasis_gen, adjoinRootEquivAdjoin_apply_root] -#align intermediate_field.adjoin.power_basis IntermediateField.adjoin.powerBasis theorem adjoin.finiteDimensional {x : L} (hx : IsIntegral K x) : FiniteDimensional K K⟮x⟯ := PowerBasis.finiteDimensional (adjoin.powerBasis hx) -#align intermediate_field.adjoin.finite_dimensional IntermediateField.adjoin.finiteDimensional theorem adjoin.finrank {x : L} (hx : IsIntegral K x) : FiniteDimensional.finrank K K⟮x⟯ = (minpoly K x).natDegree := by rw [PowerBasis.finrank (adjoin.powerBasis hx : _)] rfl -#align intermediate_field.adjoin.finrank IntermediateField.adjoin.finrank theorem _root_.minpoly.natDegree_le (x : L) [FiniteDimensional K L] : (minpoly K x).natDegree ≤ finrank K L := le_of_eq_of_le (IntermediateField.adjoin.finrank (isIntegral_of_finite _ _)).symm K⟮x⟯.toSubmodule.finrank_le -#align minpoly.nat_degree_le minpoly.natDegree_le theorem _root_.minpoly.degree_le (x : L) [FiniteDimensional K L] : (minpoly K x).degree ≤ finrank K L := degree_le_of_natDegree_le (minpoly.natDegree_le x) -#align minpoly.degree_le minpoly.degree_le end PowerBasis @@ -901,7 +792,6 @@ noncomputable def algHomAdjoinIntegralEquiv (h : IsIntegral F α) : (adjoin.powerBasis h).liftEquiv'.trans ((Equiv.refl _).subtypeEquiv fun x => by rw [adjoin.powerBasis_gen, minpoly_gen, Equiv.refl_apply]) -#align intermediate_field.alg_hom_adjoin_integral_equiv IntermediateField.algHomAdjoinIntegralEquiv lemma algHomAdjoinIntegralEquiv_symm_apply_gen (h : IsIntegral F α) (x : { x // x ∈ (minpoly F α).aroots K }) : @@ -912,14 +802,12 @@ lemma algHomAdjoinIntegralEquiv_symm_apply_gen (h : IsIntegral F α) /-- Fintype of algebra homomorphism `F⟮α⟯ →ₐ[F] K` -/ noncomputable def fintypeOfAlgHomAdjoinIntegral (h : IsIntegral F α) : Fintype (F⟮α⟯ →ₐ[F] K) := PowerBasis.AlgHom.fintype (adjoin.powerBasis h) -#align intermediate_field.fintype_of_alg_hom_adjoin_integral IntermediateField.fintypeOfAlgHomAdjoinIntegral theorem card_algHom_adjoin_integral (h : IsIntegral F α) (h_sep : (minpoly F α).Separable) (h_splits : (minpoly F α).Splits (algebraMap F K)) : @Fintype.card (F⟮α⟯ →ₐ[F] K) (fintypeOfAlgHomAdjoinIntegral F h) = (minpoly F α).natDegree := by rw [AlgHom.card_of_powerBasis] <;> simp only [adjoin.powerBasis_dim, adjoin.powerBasis_gen, minpoly_gen, h_sep, h_splits] -#align intermediate_field.card_alg_hom_adjoin_integral IntermediateField.card_algHom_adjoin_integral end AdjoinIntegralElement @@ -931,29 +819,23 @@ variable {F : Type*} [Field F] {E : Type*} [Field E] [Algebra F E] `IntermediateField.adjoin F t = S`. -/ def FG (S : IntermediateField F E) : Prop := ∃ t : Finset E, adjoin F ↑t = S -#align intermediate_field.fg IntermediateField.FG theorem fg_adjoin_finset (t : Finset E) : (adjoin F (↑t : Set E)).FG := ⟨t, rfl⟩ -#align intermediate_field.fg_adjoin_finset IntermediateField.fg_adjoin_finset theorem fg_def {S : IntermediateField F E} : S.FG ↔ ∃ t : Set E, Set.Finite t ∧ adjoin F t = S := Iff.symm Set.exists_finite_iff_finset -#align intermediate_field.fg_def IntermediateField.fg_def theorem fg_bot : (⊥ : IntermediateField F E).FG := -- porting note: was `⟨∅, adjoin_empty F E⟩` ⟨∅, by simp only [Finset.coe_empty, adjoin_empty]⟩ -#align intermediate_field.fg_bot IntermediateField.fg_bot theorem fG_of_fG_toSubalgebra (S : IntermediateField F E) (h : S.toSubalgebra.FG) : S.FG := by cases' h with t ht exact ⟨t, (eq_adjoin_of_eq_algebra_adjoin _ _ _ ht.symm).symm⟩ -#align intermediate_field.fg_of_fg_to_subalgebra IntermediateField.fG_of_fG_toSubalgebra theorem fg_of_noetherian (S : IntermediateField F E) [IsNoetherian F E] : S.FG := S.fG_of_fG_toSubalgebra S.toSubalgebra.fg_of_noetherian -#align intermediate_field.fg_of_noetherian IntermediateField.fg_of_noetherian theorem induction_on_adjoin_finset (S : Finset E) (P : IntermediateField F E → Prop) (base : P ⊥) (ih : ∀ (K : IntermediateField F E), ∀ x ∈ S, P K → P (K⟮x⟯.restrictScalars F)) : @@ -962,21 +844,18 @@ theorem induction_on_adjoin_finset (S : Finset E) (P : IntermediateField F E → · simp [base] · rw [Finset.coe_insert, Set.insert_eq, Set.union_comm, ← adjoin_adjoin_left] exact ih (adjoin F _) _ ha h -#align intermediate_field.induction_on_adjoin_finset IntermediateField.induction_on_adjoin_finset theorem induction_on_adjoin_fg (P : IntermediateField F E → Prop) (base : P ⊥) (ih : ∀ (K : IntermediateField F E) (x : E), P K → P (K⟮x⟯.restrictScalars F)) (K : IntermediateField F E) (hK : K.FG) : P K := by obtain ⟨S, rfl⟩ := hK exact induction_on_adjoin_finset S P base fun K x _ hK => ih K x hK -#align intermediate_field.induction_on_adjoin_fg IntermediateField.induction_on_adjoin_fg theorem induction_on_adjoin [FiniteDimensional F E] (P : IntermediateField F E → Prop) (base : P ⊥) (ih : ∀ (K : IntermediateField F E) (x : E), P K → P (K⟮x⟯.restrictScalars F)) (K : IntermediateField F E) : P K := letI : IsNoetherian F E := IsNoetherian.iff_fg.2 inferInstance induction_on_adjoin_fg P base ih K K.fg_of_noetherian -#align intermediate_field.induction_on_adjoin IntermediateField.induction_on_adjoin end Induction @@ -987,7 +866,6 @@ variable (F E K : Type*) [Field F] [Field E] [Field K] [Algebra F E] [Algebra F /-- Lifts `L → K` of `F → K` -/ def Lifts := Σ L : IntermediateField F E, L →ₐ[F] K -#align intermediate_field.lifts IntermediateField.Lifts variable {F E K} @@ -1016,7 +894,6 @@ noncomputable instance : Inhabited (Lifts F E K) := theorem Lifts.eq_of_le {x y : Lifts F E K} (hxy : x ≤ y) (s : x.1) : x.2 s = y.2 ⟨s, hxy.1 s.mem⟩ := hxy.2 s ⟨s, hxy.1 s.mem⟩ rfl -#align intermediate_field.lifts.eq_of_le IntermediateField.Lifts.eq_of_le theorem Lifts.exists_max_two {c : Set (Lifts F E K)} {x y : Lifts F E K} (hc : IsChain (· ≤ ·) c) (hx : x ∈ insert ⊥ c) (hy : y ∈ insert ⊥ c) : @@ -1024,7 +901,6 @@ theorem Lifts.exists_max_two {c : Set (Lifts F E K)} {x y : Lifts F E K} (hc : I cases' (hc.insert fun _ _ _ => Or.inl bot_le).total hx hy with hxy hyx · exact ⟨y, hy, hxy, le_refl y⟩ · exact ⟨x, hx, le_refl x, hyx⟩ -#align intermediate_field.lifts.exists_max_two IntermediateField.Lifts.exists_max_two theorem Lifts.exists_max_three {c : Set (Lifts F E K)} {x y z : Lifts F E K} (hc : IsChain (· ≤ ·) c) (hx : x ∈ insert ⊥ c) (hy : y ∈ insert ⊥ c) @@ -1033,7 +909,6 @@ theorem Lifts.exists_max_three {c : Set (Lifts F E K)} {x y z : Lifts F E K} obtain ⟨v, hv, hxv, hyv⟩ := Lifts.exists_max_two hc hx hy obtain ⟨w, hw, hzw, hvw⟩ := Lifts.exists_max_two hc hz hv exact ⟨w, hw, le_trans hxv hvw, le_trans hyv hvw, hzw⟩ -#align intermediate_field.lifts.exists_max_three IntermediateField.Lifts.exists_max_three /-- An upper bound on a chain of lifts -/ def Lifts.upperBoundIntermediateField {c : Set (Lifts F E K)} (hc : IsChain (· ≤ ·) c) : @@ -1051,7 +926,6 @@ def Lifts.upperBoundIntermediateField {c : Set (Lifts F E K)} (hc : IsChain (· obtain ⟨z, hz, hxz, hyz⟩ := Lifts.exists_max_two hc hx hy exact ⟨z, hz, z.1.mul_mem (hxz.1 ha) (hyz.1 hb)⟩ algebraMap_mem' s := ⟨⊥, Set.mem_insert ⊥ c, algebraMap_mem ⊥ s⟩ -#align intermediate_field.lifts.upper_bound_intermediate_field IntermediateField.Lifts.upperBoundIntermediateField /-- The lift on the upper bound on a chain of lifts -/ noncomputable def Lifts.upperBoundAlgHom {c : Set (Lifts F E K)} (hc : IsChain (· ≤ ·) c) : @@ -1075,12 +949,10 @@ noncomputable def Lifts.upperBoundAlgHom {c : Set (Lifts F E K)} (hc : IsChain ( coe_toSubalgebra, Lifts.eq_of_le hzw, Lifts.eq_of_le hxw, Lifts.eq_of_le hyw, ← w.2.map_mul, Submonoid.mk_mul_mk] commutes' _ := AlgHom.commutes _ _ -#align intermediate_field.lifts.upper_bound_alg_hom IntermediateField.Lifts.upperBoundAlgHom /-- An upper bound on a chain of lifts -/ noncomputable def Lifts.upperBound {c : Set (Lifts F E K)} (hc : IsChain (· ≤ ·) c) : Lifts F E K := ⟨Lifts.upperBoundIntermediateField hc, Lifts.upperBoundAlgHom hc⟩ -#align intermediate_field.lifts.upper_bound IntermediateField.Lifts.upperBound theorem Lifts.exists_upper_bound (c : Set (Lifts F E K)) (hc : IsChain (· ≤ ·) c) : ∃ ub, ∀ a ∈ c, a ≤ ub := @@ -1094,7 +966,6 @@ theorem Lifts.exists_upper_bound (c : Set (Lifts F E K)) (hc : IsChain (· ≤ Lifts.exists_max_two hc (Set.mem_insert_of_mem ⊥ hx) (Classical.choose_spec t.mem).1 rw [Lifts.eq_of_le hxz, Lifts.eq_of_le hyz] exact congr_arg z.2 (Subtype.ext hst)⟩ -#align intermediate_field.lifts.exists_upper_bound IntermediateField.Lifts.exists_upper_bound -- Porting note: instance `alg` added by hand. The proof is very slow. /-- Extend a lift `x : Lifts F E K` to an element `s : E` whose conjugates are all in `K` -/ @@ -1116,7 +987,6 @@ noncomputable def Lifts.liftOfSplits (x : Lifts F E K) {s : E} (h1 : IsIntegral ⟨rootOfSplits x.2.toRingHom key (ne_of_gt (minpoly.degree_pos h3)), by rw [mem_aroots, and_iff_right (minpoly.ne_zero h3)] exact map_rootOfSplits x.2.toRingHom key (ne_of_gt (minpoly.degree_pos h3))⟩⟩⟩ -#align intermediate_field.lifts.lift_of_splits IntermediateField.Lifts.liftOfSplits -- Porting note: instance `alg` added by hand. -- Porting note: Lean3 is able to guess `φ` @@ -1142,17 +1012,14 @@ theorem Lifts.le_lifts_of_splits (x : Lifts F E K) {s : E} (h1 : IsIntegral F s) ⟨rootOfSplits (AlgHom.toRingHom x.2) key I2, I3⟩) exact AlgHom.commutes φ t)⟩ -#align intermediate_field.lifts.le_lifts_of_splits IntermediateField.Lifts.le_lifts_of_splits theorem Lifts.mem_lifts_of_splits (x : Lifts F E K) {s : E} (h1 : IsIntegral F s) (h2 : (minpoly F s).Splits (algebraMap F K)) : s ∈ (x.liftOfSplits h1 h2).1 := mem_adjoin_simple_self x.1 s -#align intermediate_field.lifts.mem_lifts_of_splits IntermediateField.Lifts.mem_lifts_of_splits theorem Lifts.exists_lift_of_splits (x : Lifts F E K) {s : E} (h1 : IsIntegral F s) (h2 : (minpoly F s).Splits (algebraMap F K)) : ∃ y, x ≤ y ∧ s ∈ y.1 := ⟨x.liftOfSplits h1 h2, x.le_lifts_of_splits h1 h2, x.mem_lifts_of_splits h1 h2⟩ -#align intermediate_field.lifts.exists_lift_of_splits IntermediateField.Lifts.exists_lift_of_splits theorem algHom_mk_adjoin_splits (hK : ∀ s ∈ S, IsIntegral F (s : E) ∧ (minpoly F s).Splits (algebraMap F K)) : @@ -1168,7 +1035,6 @@ theorem algHom_mk_adjoin_splits commutes' := x.2.commutes }⟩ rcases x.exists_lift_of_splits (hK s hs).1 (hK s hs).2 with ⟨y, h1, h2⟩ rwa [hx y h1] at h2 -#align intermediate_field.alg_hom_mk_adjoin_splits IntermediateField.algHom_mk_adjoin_splits theorem algHom_mk_adjoin_splits' (hS : adjoin F S = ⊤) (hK : ∀ x ∈ S, IsIntegral F (x : E) ∧ (minpoly F x).Splits (algebraMap F K)) : @@ -1176,7 +1042,6 @@ theorem algHom_mk_adjoin_splits' (hS : adjoin F S = ⊤) cases' algHom_mk_adjoin_splits hK with ϕ rw [hS] at ϕ exact ⟨ϕ.comp topEquiv.symm.toAlgHom⟩ -#align intermediate_field.alg_hom_mk_adjoin_splits' IntermediateField.algHom_mk_adjoin_splits' end AlgHomMkAdjoinSplits @@ -1186,7 +1051,6 @@ variable {K L : Type*} [Field K] [Field L] [Algebra K L] (E1 E2 : IntermediateFi theorem le_sup_toSubalgebra : E1.toSubalgebra ⊔ E2.toSubalgebra ≤ (E1 ⊔ E2).toSubalgebra := sup_le (show E1 ≤ E1 ⊔ E2 from le_sup_left) (show E2 ≤ E1 ⊔ E2 from le_sup_right) -#align intermediate_field.le_sup_to_subalgebra IntermediateField.le_sup_toSubalgebra theorem sup_toSubalgebra [h1 : FiniteDimensional K E1] [h2 : FiniteDimensional K E2] : (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra := by @@ -1208,7 +1072,6 @@ theorem sup_toSubalgebra [h1 : FiniteDimensional K E1] [h2 : FiniteDimensional K isField_of_isIntegral_of_isField' (isIntegral_sup.mpr ⟨Algebra.isIntegral_of_finite K E1, Algebra.isIntegral_of_finite K E2⟩) (Field.toIsField K) -#align intermediate_field.sup_to_subalgebra IntermediateField.sup_toSubalgebra instance finiteDimensional_sup [h1 : FiniteDimensional K E1] [h2 : FiniteDimensional K E2] : FiniteDimensional K (E1 ⊔ E2 : IntermediateField K L) := by @@ -1218,7 +1081,6 @@ instance finiteDimensional_sup [h1 : FiniteDimensional K E1] [h2 : FiniteDimensi g.toLinearMap.finiteDimensional_range rwa [this] at h rw [Algebra.TensorProduct.productMap_range, E1.range_val, E2.range_val, sup_toSubalgebra] -#align intermediate_field.finite_dimensional_sup IntermediateField.finiteDimensional_sup instance finiteDimensional_iSup_of_finite {ι : Type*} {t : ι → IntermediateField K L} [h : Finite ι] [∀ i, FiniteDimensional K (t i)] : @@ -1234,7 +1096,6 @@ instance finiteDimensional_iSup_of_finite {ι : Type*} {t : ι → IntermediateF · intro _ s _ _ hs rw [iSup_insert] exact IntermediateField.finiteDimensional_sup _ _ -#align intermediate_field.finite_dimensional_supr_of_finite IntermediateField.finiteDimensional_iSup_of_finite instance finiteDimensional_iSup_of_finset {ι : Type*} {f : ι → IntermediateField K L} /-Porting note: changed `h` from `∀ i ∈ s, FiniteDimensional K (f i)` because this caused an @@ -1247,7 +1108,6 @@ instance finiteDimensional_iSup_of_finset {ι : Type*} {f : ι → IntermediateF le_antisymm (iSup_le fun i => iSup_le fun h => le_iSup (fun i : { i // i ∈ s } => f i) ⟨i, h⟩) (iSup_le fun i => le_iSup_of_le i (le_iSup_of_le i.2 le_rfl)) exact this.symm ▸ IntermediateField.finiteDimensional_iSup_of_finite -#align intermediate_field.finite_dimensional_supr_of_finset IntermediateField.finiteDimensional_iSup_of_finset theorem finiteDimensional_iSup_of_finset' {ι : Type*} {f : ι → IntermediateField K L} /-Porting note: this was the mathlib3 version. Using `[h : ...]`, as in mathlib3, causes the @@ -1271,7 +1131,6 @@ theorem isAlgebraic_iSup {ι : Type*} {f : ι → IntermediateField K L} haveI : ∀ i : Σ i, f i, FiniteDimensional K K⟮(i.2 : L)⟯ := fun ⟨i, x⟩ => adjoin.finiteDimensional (isIntegral_iff.1 (isAlgebraic_iff_isIntegral.1 (h i x))) apply Algebra.isAlgebraic_of_finite -#align intermediate_field.is_algebraic_supr IntermediateField.isAlgebraic_iSup end Supremum @@ -1289,31 +1148,26 @@ open IntermediateField noncomputable def equivAdjoinSimple (pb : PowerBasis K L) : K⟮pb.gen⟯ ≃ₐ[K] L := (adjoin.powerBasis pb.isIntegral_gen).equivOfMinpoly pb <| by rw [adjoin.powerBasis_gen, minpoly_gen] -#align power_basis.equiv_adjoin_simple PowerBasis.equivAdjoinSimple @[simp] theorem equivAdjoinSimple_aeval (pb : PowerBasis K L) (f : K[X]) : pb.equivAdjoinSimple (aeval (AdjoinSimple.gen K pb.gen) f) = aeval pb.gen f := equivOfMinpoly_aeval _ pb _ f -#align power_basis.equiv_adjoin_simple_aeval PowerBasis.equivAdjoinSimple_aeval @[simp] theorem equivAdjoinSimple_gen (pb : PowerBasis K L) : pb.equivAdjoinSimple (AdjoinSimple.gen K pb.gen) = pb.gen := equivOfMinpoly_gen _ pb _ -#align power_basis.equiv_adjoin_simple_gen PowerBasis.equivAdjoinSimple_gen @[simp] theorem equivAdjoinSimple_symm_aeval (pb : PowerBasis K L) (f : K[X]) : pb.equivAdjoinSimple.symm (aeval pb.gen f) = aeval (AdjoinSimple.gen K pb.gen) f := by rw [equivAdjoinSimple, equivOfMinpoly_symm, equivOfMinpoly_aeval, adjoin.powerBasis_gen] -#align power_basis.equiv_adjoin_simple_symm_aeval PowerBasis.equivAdjoinSimple_symm_aeval @[simp] theorem equivAdjoinSimple_symm_gen (pb : PowerBasis K L) : pb.equivAdjoinSimple.symm pb.gen = AdjoinSimple.gen K pb.gen := by rw [equivAdjoinSimple, equivOfMinpoly_symm, equivOfMinpoly_gen, adjoin.powerBasis_gen] -#align power_basis.equiv_adjoin_simple_symm_gen PowerBasis.equivAdjoinSimple_symm_gen end PowerBasis diff --git a/Mathlib/GroupTheory/Schreier.lean b/Mathlib/GroupTheory/Schreier.lean index a6a5e45d6ec1b..dbccedc1560c2 100644 --- a/Mathlib/GroupTheory/Schreier.lean +++ b/Mathlib/GroupTheory/Schreier.lean @@ -56,7 +56,6 @@ theorem closure_mul_image_mul_eq_top (mul_inv_toFun_mem hR (f (r * s⁻¹) * s)) rw [mul_assoc, ← inv_inv s, ← mul_inv_rev, inv_inv] exact toFun_mul_inv_mem hR (r * s⁻¹) -#align subgroup.closure_mul_image_mul_eq_top Subgroup.closure_mul_image_mul_eq_top /-- **Schreier's Lemma**: If `R : Set G` is a `rightTransversal of` `H : Subgroup G` with `1 ∈ R`, and if `G` is generated by `S : Set G`, then `H` is generated by the `Set` @@ -77,7 +76,6 @@ theorem closure_mul_image_eq (hR : R ∈ rightTransversals (H : Set G)) (hR1 : ( exact H.one_mem · rw [Subtype.coe_mk, inv_one, mul_one] exact (H.mul_mem_cancel_left (hU hg)).mp hh -#align subgroup.closure_mul_image_eq Subgroup.closure_mul_image_eq /-- **Schreier's Lemma**: If `R : Set G` is a `rightTransversal` of `H : Subgroup G` with `1 ∈ R`, and if `G` is generated by `S : Set G`, then `H` is generated by the `Set` @@ -87,7 +85,6 @@ theorem closure_mul_image_eq_top (hR : R ∈ rightTransversals (H : Set G)) (hR1 ⟨g * (toFun hR g : G)⁻¹, mul_inv_toFun_mem hR g⟩ : Set H) = ⊤ := by rw [eq_top_iff, ← map_subtype_le_map_subtype, MonoidHom.map_closure, Set.image_image] exact (map_subtype_le ⊤).trans (ge_of_eq (closure_mul_image_eq hR hR1 hS)) -#align subgroup.closure_mul_image_eq_top Subgroup.closure_mul_image_eq_top /-- **Schreier's Lemma**: If `R : Finset G` is a `rightTransversal` of `H : Subgroup G` with `1 ∈ R`, and if `G` is generated by `S : Finset G`, then `H` is generated by the `Finset` @@ -98,7 +95,6 @@ theorem closure_mul_image_eq_top' [DecidableEq G] {R S : Finset G} closure (((R * S).image fun g => ⟨_, mul_inv_toFun_mem hR g⟩ : Finset H) : Set H) = ⊤ := by rw [Finset.coe_image, Finset.coe_mul] exact closure_mul_image_eq_top hR hR1 hS -#align subgroup.closure_mul_image_eq_top' Subgroup.closure_mul_image_eq_top' variable (H) @@ -122,7 +118,6 @@ theorem exists_finset_card_le_mul [FiniteIndex H] {S : Finset G} (hS : closure ( _ = _ := (Fintype.card_congr (toEquiv hR)).symm _ = Fintype.card (G ⧸ H) := (QuotientGroup.card_quotient_rightRel H) _ = H.index := H.index_eq_card.symm -#align subgroup.exists_finset_card_le_mul Subgroup.exists_finset_card_le_mul /-- **Schreier's Lemma**: A finite index subgroup of a finitely generated group is finitely generated. -/ @@ -130,7 +125,6 @@ instance fg_of_index_ne_zero [hG : Group.FG G] [FiniteIndex H] : Group.FG H := b obtain ⟨S, hS⟩ := hG.1 obtain ⟨T, -, hT⟩ := exists_finset_card_le_mul H hS exact ⟨⟨T, hT⟩⟩ -#align subgroup.fg_of_index_ne_zero Subgroup.fg_of_index_ne_zero theorem rank_le_index_mul_rank [hG : Group.FG G] [FiniteIndex H] : Group.rank H ≤ H.index * Group.rank G := by @@ -141,7 +135,6 @@ theorem rank_le_index_mul_rank [hG : Group.FG G] [FiniteIndex H] : Group.rank H ≤ T.card := Group.rank_le H hT _ ≤ H.index * S.card := hT₀ _ = H.index * Group.rank G := congr_arg ((· * ·) H.index) hS₀ -#align subgroup.rank_le_index_mul_rank Subgroup.rank_le_index_mul_rank variable (G) @@ -176,12 +169,10 @@ theorem card_commutator_dvd_index_center_pow [Finite (commutatorSet G)] : have := Abelianization.commutator_subset_ker (MonoidHom.transferCenterPow G) g.1.2 -- `transfer g` is defeq to `g ^ [G : Z(G)]`, so we are done simpa only [MonoidHom.mem_ker, Subtype.ext_iff] using this -#align subgroup.card_commutator_dvd_index_center_pow Subgroup.card_commutator_dvd_index_center_pow /-- A bound for the size of the commutator subgroup in terms of the number of commutators. -/ def cardCommutatorBound (n : ℕ) := (n ^ (2 * n)) ^ (n ^ (2 * n + 1) + 1) -#align subgroup.card_commutator_bound Subgroup.cardCommutatorBound /-- A theorem of Schur: The size of the commutator subgroup is bounded in terms of the number of commutators. -/ @@ -198,7 +189,6 @@ theorem card_commutator_le_of_finite_commutatorSet [Finite (commutatorSet G)] : rw [← pow_succ'] at h2 refine' (Nat.le_of_dvd _ h2).trans (Nat.pow_le_pow_of_le_left h1 _) exact pow_pos (Nat.pos_of_ne_zero FiniteIndex.finiteIndex) _ -#align subgroup.card_commutator_le_of_finite_commutator_set Subgroup.card_commutator_le_of_finite_commutatorSet /-- A theorem of Schur: A group with finitely many commutators has finite commutator subgroup. -/ instance [Finite (commutatorSet G)] : Finite (_root_.commutator G) := by diff --git a/Mathlib/NumberTheory/Cyclotomic/Basic.lean b/Mathlib/NumberTheory/Cyclotomic/Basic.lean index abe75829e79be..52603e5dcf548 100644 --- a/Mathlib/NumberTheory/Cyclotomic/Basic.lean +++ b/Mathlib/NumberTheory/Cyclotomic/Basic.lean @@ -84,7 +84,6 @@ class IsCyclotomicExtension : Prop where exists_prim_root {n : ℕ+} (ha : n ∈ S) : ∃ r : B, IsPrimitiveRoot r n /-- The `n`-th roots of unity, for `n ∈ S`, generate `B` as an `A`-algebra. -/ adjoin_roots : ∀ x : B, x ∈ adjoin A {b : B | ∃ n : ℕ+, n ∈ S ∧ b ^ (n : ℕ) = 1} -#align is_cyclotomic_extension IsCyclotomicExtension namespace IsCyclotomicExtension @@ -97,25 +96,21 @@ theorem iff_adjoin_eq_top : adjoin A {b : B | ∃ n : ℕ+, n ∈ S ∧ b ^ (n : ℕ) = 1} = ⊤ := ⟨fun h => ⟨fun _ => h.exists_prim_root, Algebra.eq_top_iff.2 h.adjoin_roots⟩, fun h => ⟨h.1 _, Algebra.eq_top_iff.1 h.2⟩⟩ -#align is_cyclotomic_extension.iff_adjoin_eq_top IsCyclotomicExtension.iff_adjoin_eq_top /-- A reformulation of `IsCyclotomicExtension` in the case `S` is a singleton. -/ theorem iff_singleton : IsCyclotomicExtension {n} A B ↔ (∃ r : B, IsPrimitiveRoot r n) ∧ ∀ x, x ∈ adjoin A {b : B | b ^ (n : ℕ) = 1} := by simp [IsCyclotomicExtension_iff] -#align is_cyclotomic_extension.iff_singleton IsCyclotomicExtension.iff_singleton /-- If `IsCyclotomicExtension ∅ A B`, then the image of `A` in `B` equals `B`. -/ theorem empty [h : IsCyclotomicExtension ∅ A B] : (⊥ : Subalgebra A B) = ⊤ := by simpa [Algebra.eq_top_iff, IsCyclotomicExtension_iff] using h -#align is_cyclotomic_extension.empty IsCyclotomicExtension.empty /-- If `IsCyclotomicExtension {1} A B`, then the image of `A` in `B` equals `B`. -/ theorem singleton_one [h : IsCyclotomicExtension {1} A B] : (⊥ : Subalgebra A B) = ⊤ := Algebra.eq_top_iff.2 fun x => by simpa [adjoin_singleton_one] using ((IsCyclotomicExtension_iff _ _ _).1 h).2 x -#align is_cyclotomic_extension.singleton_one IsCyclotomicExtension.singleton_one variable {A B} @@ -127,7 +122,6 @@ theorem singleton_zero_of_bot_eq_top (h : (⊥ : Subalgebra A B) = ⊤) : ⟨fun s hs => by simp at hs, _root_.eq_top_iff.2 fun x hx => _⟩ rw [← h] at hx simpa using hx -#align is_cyclotomic_extension.singleton_zero_of_bot_eq_top IsCyclotomicExtension.singleton_zero_of_bot_eq_top variable (A B) @@ -151,7 +145,6 @@ theorem trans (C : Type w) [CommRing C] [Algebra A C] [Algebra B C] [IsScalarTow refine' adjoin_mono (fun y hy => _) hb obtain ⟨b₁, ⟨⟨n, hn⟩, h₁⟩⟩ := hy exact ⟨n, ⟨mem_union_left T hn.1, by rw [← h₁, ← AlgHom.map_pow, hn.2, AlgHom.map_one]⟩⟩ -#align is_cyclotomic_extension.trans IsCyclotomicExtension.trans @[nontriviality] theorem subsingleton_iff [Subsingleton B] : IsCyclotomicExtension S A B ↔ S = { } ∨ S = {1} := by @@ -168,7 +161,6 @@ theorem subsingleton_iff [Subsingleton B] : IsCyclotomicExtension S A B ↔ S = · rw [iff_singleton] exact ⟨⟨0, IsPrimitiveRoot.of_subsingleton 0⟩, fun x => by convert (mem_top (R := A) : x ∈ ⊤)⟩ -#align is_cyclotomic_extension.subsingleton_iff IsCyclotomicExtension.subsingleton_iff /-- If `B` is a cyclotomic extension of `A` given by roots of unity of order in `S ∪ T`, then `B` is a cyclotomic extension of `adjoin A { b : B | ∃ a : ℕ+, a ∈ S ∧ b ^ (a : ℕ) = 1 }` given by @@ -188,7 +180,6 @@ theorem union_right [h : IsCyclotomicExtension (S ∪ T) A B] : refine' ⟨fun hn => ((IsCyclotomicExtension_iff _ A _).1 h).1 (mem_union_right S hn), fun b => _⟩ replace h := ((IsCyclotomicExtension_iff _ _ _).1 h).2 b rwa [this, adjoin_union_eq_adjoin_adjoin, Subalgebra.mem_restrictScalars] at h -#align is_cyclotomic_extension.union_right IsCyclotomicExtension.union_right /-- If `B` is a cyclotomic extension of `A` given by roots of unity of order in `T` and `S ⊆ T`, then `adjoin A { b : B | ∃ a : ℕ+, a ∈ S ∧ b ^ (a : ℕ) = 1 }` is a cyclotomic extension of `B` @@ -202,7 +193,6 @@ theorem union_left [h : IsCyclotomicExtension T A B] (hS : S ⊆ T) : · convert mem_top (R := A) (x := b) rw [← adjoin_adjoin_coe_preimage, preimage_setOf_eq] norm_cast -#align is_cyclotomic_extension.union_left IsCyclotomicExtension.union_left variable {n S} @@ -226,7 +216,6 @@ theorem of_union_of_dvd (h : ∀ s ∈ S, n ∣ s) (hS : S.Nonempty) [H : IsCycl simp only [union_singleton, mem_insert_iff, mem_setOf_eq] at hx ⊢ obtain ⟨m, hm⟩ := hx exact ⟨m, ⟨Or.inr hm.1, hm.2⟩⟩ -#align is_cyclotomic_extension.of_union_of_dvd IsCyclotomicExtension.of_union_of_dvd /-- If `∀ s ∈ S, n ∣ s` and `S` is not empty, then `IsCyclotomicExtension S A B` if and only if `IsCyclotomicExtension (S ∪ {n}) A B`. -/ @@ -244,7 +233,6 @@ theorem iff_union_of_dvd (h : ∀ s ∈ S, n ∣ s) (hS : S.Nonempty) : obtain ⟨z, rfl⟩ := h y hy simp only [PNat.mul_coe, pow_mul, hxpow, one_pow] · exact ⟨m, ⟨hm, hxpow⟩⟩ -#align is_cyclotomic_extension.iff_union_of_dvd IsCyclotomicExtension.iff_union_of_dvd variable (n S) @@ -259,7 +247,6 @@ theorem iff_union_singleton_one : simp [adjoin_singleton_one, empty] · refine' (iff_adjoin_eq_top _ A _).2 ⟨fun s hs => (not_mem_empty s hs).elim, _⟩ simp [@singleton_one A B _ _ _ H] -#align is_cyclotomic_extension.iff_union_singleton_one IsCyclotomicExtension.iff_union_singleton_one variable {A B} @@ -268,13 +255,11 @@ theorem singleton_one_of_bot_eq_top (h : (⊥ : Subalgebra A B) = ⊤) : IsCyclotomicExtension {1} A B := by convert (iff_union_singleton_one _ A _).1 (singleton_zero_of_bot_eq_top h) simp -#align is_cyclotomic_extension.singleton_one_of_bot_eq_top IsCyclotomicExtension.singleton_one_of_bot_eq_top /-- If `Function.Surjective (algebraMap A B)`, then `IsCyclotomicExtension {1} A B`. -/ theorem singleton_one_of_algebraMap_bijective (h : Function.Surjective (algebraMap A B)) : IsCyclotomicExtension {1} A B := singleton_one_of_bot_eq_top (surjective_algebraMap_iff.1 h).symm -#align is_cyclotomic_extension.singleton_one_of_algebra_map_bijective IsCyclotomicExtension.singleton_one_of_algebraMap_bijective variable (A B) @@ -287,19 +272,16 @@ theorem equiv {C : Type*} [CommRing C] [Algebra A C] [h : IsCyclotomicExtension haveI : IsCyclotomicExtension {1} B C := singleton_one_of_algebraMap_bijective f.surjective haveI : IsScalarTower A B C := IsScalarTower.of_ring_hom f.toAlgHom exact (iff_union_singleton_one _ _ _).2 (trans S {1} A B C f.injective) -#align is_cyclotomic_extension.equiv IsCyclotomicExtension.equiv protected theorem neZero [h : IsCyclotomicExtension {n} A B] [IsDomain B] : NeZero ((n : ℕ) : B) := by obtain ⟨⟨r, hr⟩, -⟩ := (iff_singleton n A B).1 h exact hr.neZero' -#align is_cyclotomic_extension.ne_zero IsCyclotomicExtension.neZero protected theorem neZero' [IsCyclotomicExtension {n} A B] [IsDomain B] : NeZero ((n : ℕ) : A) := by haveI := IsCyclotomicExtension.neZero n A B exact NeZero.nat_of_neZero (algebraMap A B) -#align is_cyclotomic_extension.ne_zero' IsCyclotomicExtension.neZero' end Basic @@ -317,7 +299,6 @@ theorem finite_of_singleton [IsDomain B] [h : IsCyclotomicExtension {n} A B] : exact (nthRoots (↑n) 1).toFinset.finite_toSet · simp only [mem_singleton_iff, exists_eq_left, mem_setOf_eq] at hb refine' ⟨X ^ (n : ℕ) - 1, ⟨monic_X_pow_sub_C _ n.pos.ne.symm, by simp [hb]⟩⟩ -#align is_cyclotomic_extension.finite_of_singleton IsCyclotomicExtension.finite_of_singleton /-- If `S` is finite and `IsCyclotomicExtension S A B`, then `B` is a finite `A`-algebra. -/ protected @@ -338,7 +319,6 @@ theorem finite [IsDomain B] [h₁ : Finite S] [h₂ : IsCyclotomicExtension S A letI := @union_right S {n} A B _ _ _ h exact finite_of_singleton n _ _ exact Module.Finite.trans (adjoin A {b : B | ∃ n : ℕ+, n ∈ S ∧ b ^ (n : ℕ) = 1}) _ -#align is_cyclotomic_extension.finite IsCyclotomicExtension.finite /-- A cyclotomic finite extension of a number field is a number field. -/ theorem numberField [h : NumberField K] [Finite S] [IsCyclotomicExtension S K L] : NumberField L := @@ -347,20 +327,17 @@ theorem numberField [h : NumberField K] [Finite S] [IsCyclotomicExtension S K L] haveI := charZero_of_injective_algebraMap (algebraMap K L).injective haveI := IsCyclotomicExtension.finite S K L exact Module.Finite.trans K _ } -#align is_cyclotomic_extension.number_field IsCyclotomicExtension.numberField /-- A finite cyclotomic extension of an integral noetherian domain is integral -/ theorem integral [IsDomain B] [IsNoetherianRing A] [Finite S] [IsCyclotomicExtension S A B] : Algebra.IsIntegral A B := letI := IsCyclotomicExtension.finite S A B; isIntegral_of_noetherian <| isNoetherian_of_isNoetherianRing_of_finite A B -#align is_cyclotomic_extension.integral IsCyclotomicExtension.integral /-- If `S` is finite and `IsCyclotomicExtension S K A`, then `finiteDimensional K A`. -/ theorem finiteDimensional (C : Type z) [Finite S] [CommRing C] [Algebra K C] [IsDomain C] [IsCyclotomicExtension S K C] : FiniteDimensional K C := IsCyclotomicExtension.finite S K C -#align is_cyclotomic_extension.finite_dimensional IsCyclotomicExtension.finiteDimensional end Fintype @@ -385,7 +362,6 @@ theorem adjoin_roots_cyclotomic_eq_adjoin_nth_roots [IsDomain B] {ζ : B} {n : refine' SetLike.mem_coe.2 (Subalgebra.pow_mem _ (subset_adjoin _) _) rw [mem_rootSet', map_cyclotomic, aeval_def, ← eval_map, map_cyclotomic, ← IsRoot] refine' ⟨cyclotomic_ne_zero n B, hζ.isRoot_cyclotomic n.pos⟩ -#align is_cyclotomic_extension.adjoin_roots_cyclotomic_eq_adjoin_nth_roots IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_nth_roots theorem adjoin_roots_cyclotomic_eq_adjoin_root_cyclotomic {n : ℕ+} [IsDomain B] {ζ : B} (hζ : IsPrimitiveRoot ζ n) : adjoin A ((cyclotomic n A).rootSet B) = adjoin A {ζ} := by @@ -400,7 +376,6 @@ theorem adjoin_roots_cyclotomic_eq_adjoin_root_cyclotomic {n : ℕ+} [IsDomain B · simp only [mem_singleton_iff, exists_eq_left, mem_setOf_eq] at hx simpa only [hx, mem_rootSet', map_cyclotomic, aeval_def, ← eval_map, IsRoot] using And.intro (cyclotomic_ne_zero n B) (hζ.isRoot_cyclotomic n.pos) -#align is_cyclotomic_extension.adjoin_roots_cyclotomic_eq_adjoin_root_cyclotomic IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_root_cyclotomic theorem adjoin_primitive_root_eq_top {n : ℕ+} [IsDomain B] [h : IsCyclotomicExtension {n} A B] {ζ : B} (hζ : IsPrimitiveRoot ζ n) : adjoin A ({ζ} : Set B) = ⊤ := by @@ -408,7 +383,6 @@ theorem adjoin_primitive_root_eq_top {n : ℕ+} [IsDomain B] [h : IsCyclotomicEx rw [← adjoin_roots_cyclotomic_eq_adjoin_root_cyclotomic hζ] rw [adjoin_roots_cyclotomic_eq_adjoin_nth_roots hζ] exact ((iff_adjoin_eq_top {n} A B).mp h).2 -#align is_cyclotomic_extension.adjoin_primitive_root_eq_top IsCyclotomicExtension.adjoin_primitive_root_eq_top variable (A) @@ -431,7 +405,6 @@ theorem _root_.IsPrimitiveRoot.adjoin_isCyclotomicExtension {ζ : B} {n : ℕ+} · exact Subalgebra.algebraMap_mem _ _ · exact Subalgebra.add_mem _ hb₁ hb₂ · exact Subalgebra.mul_mem _ hb₁ hb₂ } -#align is_primitive_root.adjoin_is_cyclotomic_extension IsPrimitiveRoot.adjoin_isCyclotomicExtension end @@ -447,7 +420,6 @@ theorem splits_X_pow_sub_one [H : IsCyclotomicExtension S K L] (hS : n ∈ S) : obtain ⟨z, hz⟩ := ((IsCyclotomicExtension_iff _ _ _).1 H).1 hS exact X_pow_sub_one_splits hz set_option linter.uppercaseLean3 false in -#align is_cyclotomic_extension.splits_X_pow_sub_one IsCyclotomicExtension.splits_X_pow_sub_one /-- A cyclotomic extension splits `cyclotomic n K` if `n ∈ S` and `ne_zero (n : K)`.-/ theorem splits_cyclotomic [IsCyclotomicExtension S K L] (hS : n ∈ S) : @@ -455,7 +427,6 @@ theorem splits_cyclotomic [IsCyclotomicExtension S K L] (hS : n ∈ S) : refine' splits_of_splits_of_dvd _ (X_pow_sub_C_ne_zero n.pos _) (splits_X_pow_sub_one K L hS) _ use ∏ i : ℕ in (n : ℕ).properDivisors, Polynomial.cyclotomic i K rw [(eq_cyclotomic_iff n.pos _).1 rfl, RingHom.map_one] -#align is_cyclotomic_extension.splits_cyclotomic IsCyclotomicExtension.splits_cyclotomic variable (n S) @@ -476,7 +447,6 @@ theorem isSplittingField_X_pow_sub_one : IsSplittingField K L (X ^ (n : ℕ) - 1 and_iff_right_iff_imp, Polynomial.map_sub, Polynomial.map_pow, Polynomial.map_one] exact fun _ => X_pow_sub_C_ne_zero n.pos (1 : L) } set_option linter.uppercaseLean3 false in -#align is_cyclotomic_extension.splitting_field_X_pow_sub_one IsCyclotomicExtension.isSplittingField_X_pow_sub_one /-- Any two `n`-th cyclotomic extensions are isomorphic. -/ def algEquiv (L' : Type*) [Field L'] [Algebra K L'] [IsCyclotomicExtension {n} K L'] : @@ -485,7 +455,6 @@ def algEquiv (L' : Type*) [Field L'] [Algebra K L'] [IsCyclotomicExtension {n} K let h₂ := isSplittingField_X_pow_sub_one n K L' (@IsSplittingField.algEquiv K L _ _ _ (X ^ (n : ℕ) - 1) h₁).trans (@IsSplittingField.algEquiv K L' _ _ _ (X ^ (n : ℕ) - 1) h₂).symm -#align is_cyclotomic_extension.alg_equiv IsCyclotomicExtension.algEquiv scoped[Cyclotomic] attribute [instance] IsCyclotomicExtension.isSplittingField_X_pow_sub_one @@ -493,7 +462,6 @@ theorem isGalois : IsGalois K L := letI := isSplittingField_X_pow_sub_one n K L IsGalois.of_separable_splitting_field (X_pow_sub_one_separable_iff.2 (IsCyclotomicExtension.neZero' n K L).1) -#align is_cyclotomic_extension.is_galois IsCyclotomicExtension.isGalois /-- If `IsCyclotomicExtension {n} K L`, then `L` is the splitting field of `cyclotomic n K`. -/ theorem splitting_field_cyclotomic : IsSplittingField K L (cyclotomic n K) := @@ -504,7 +472,6 @@ theorem splitting_field_cyclotomic : IsSplittingField K L (cyclotomic n K) := -- todo: make `exists_prim_root` take an explicit `L` obtain ⟨ζ : L, hζ⟩ := IsCyclotomicExtension.exists_prim_root K (B := L) (mem_singleton n) exact adjoin_roots_cyclotomic_eq_adjoin_nth_roots hζ } -#align is_cyclotomic_extension.splitting_field_cyclotomic IsCyclotomicExtension.splitting_field_cyclotomic scoped[Cyclotomic] attribute [instance] IsCyclotomicExtension.splitting_field_cyclotomic @@ -521,7 +488,6 @@ splitting field of `cyclotomic n K`. If `n` is nonzero in `K`, it has the instance `IsCyclotomicExtension {n} K (CyclotomicField n K)`. -/ def CyclotomicField : Type w := (cyclotomic n K).SplittingField -#align cyclotomic_field CyclotomicField namespace CyclotomicField @@ -555,7 +521,6 @@ instance isCyclotomicExtension [NeZero ((n : ℕ) : K)] : exact ⟨ζ, hζ⟩ · rw [← Algebra.eq_top_iff, ← SplittingField.adjoin_rootSet, eq_comm] exact IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_nth_roots hζ -#align cyclotomic_field.is_cyclotomic_extension CyclotomicField.isCyclotomicExtension end CyclotomicField @@ -572,7 +537,6 @@ section CyclotomicRing @[nolint unusedArguments] instance CyclotomicField.algebraBase : Algebra A (CyclotomicField n K) := SplittingField.algebra' (cyclotomic n K) -#align cyclotomic_field.algebra_base CyclotomicField.algebraBase /-- Ensure there are no diamonds when `A = ℤ`. -/ example : algebraInt (CyclotomicField n ℚ) = CyclotomicField.algebraBase _ _ _ := @@ -581,7 +545,6 @@ example : algebraInt (CyclotomicField n ℚ) = CyclotomicField.algebraBase _ _ _ instance CyclotomicField.algebra' {R : Type*} [CommRing R] [Algebra R K] : Algebra R (CyclotomicField n K) := SplittingField.algebra' (cyclotomic n K) -#align cyclotomic_field.algebra' CyclotomicField.algebra' instance {R : Type*} [CommRing R] [Algebra R K] : IsScalarTower R K (CyclotomicField n K) := SplittingField.isScalarTower _ @@ -592,7 +555,6 @@ instance CyclotomicField.noZeroSMulDivisors : NoZeroSMulDivisors A (CyclotomicFi exact (Function.Injective.comp (NoZeroSMulDivisors.algebraMap_injective K (CyclotomicField n K)) (IsFractionRing.injective A K) : _) -#align cyclotomic_field.no_zero_smul_divisors CyclotomicField.noZeroSMulDivisors /-- If `A` is a domain with fraction field `K` and `n : ℕ+`, we define `CyclotomicRing n A K` as the `A`-subalgebra of `CyclotomicField n K` generated by the roots of `X ^ n - 1`. If `n` @@ -601,7 +563,6 @@ is nonzero in `A`, it has the instance `IsCyclotomicExtension {n} A (CyclotomicR def CyclotomicRing : Type w := adjoin A {b : CyclotomicField n K | b ^ (n : ℕ) = 1} --deriving CommRing, IsDomain, Inhabited -#align cyclotomic_ring CyclotomicRing namespace CyclotomicRing @@ -620,7 +581,6 @@ instance : Inhabited (CyclotomicRing n A K) := by /-- The `A`-algebra structure on `CyclotomicRing n A K`. -/ instance algebraBase : Algebra A (CyclotomicRing n A K) := (adjoin A _).algebra -#align cyclotomic_ring.algebra_base CyclotomicRing.algebraBase -- Ensure that there is no diamonds with ℤ. example {n : ℕ+} : CyclotomicRing.algebraBase n ℤ ℚ = algebraInt _ := @@ -631,7 +591,6 @@ instance : NoZeroSMulDivisors A (CyclotomicRing n A K) := theorem algebraBase_injective : Function.Injective <| algebraMap A (CyclotomicRing n A K) := NoZeroSMulDivisors.algebraMap_injective _ _ -#align cyclotomic_ring.algebra_base_injective CyclotomicRing.algebraBase_injective instance : Algebra (CyclotomicRing n A K) (CyclotomicField n K) := (adjoin A _).toAlgebra @@ -639,7 +598,6 @@ instance : Algebra (CyclotomicRing n A K) (CyclotomicField n K) := theorem adjoin_algebra_injective : Function.Injective <| algebraMap (CyclotomicRing n A K) (CyclotomicField n K) := Subtype.val_injective -#align cyclotomic_ring.adjoin_algebra_injective CyclotomicRing.adjoin_algebra_injective instance : NoZeroSMulDivisors (CyclotomicRing n A K) (CyclotomicField n K) := NoZeroSMulDivisors.of_algebraMap_injective (adjoin_algebra_injective n A K) @@ -669,7 +627,6 @@ instance isCyclotomicExtension [NeZero ((n : ℕ) : A)] : · exact Subalgebra.algebraMap_mem _ a · exact Subalgebra.add_mem _ hy hz · exact Subalgebra.mul_mem _ hy hz -#align cyclotomic_ring.is_cyclotomic_extension CyclotomicRing.isCyclotomicExtension instance [IsDomain A] [NeZero ((n : ℕ) : A)] : IsFractionRing (CyclotomicRing n A K) (CyclotomicField n K) where @@ -717,7 +674,6 @@ theorem eq_adjoin_primitive_root {μ : CyclotomicField n K} (h : IsPrimitiveRoot rw [← IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_root_cyclotomic h, IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_nth_roots h] simp [CyclotomicRing] -#align cyclotomic_ring.eq_adjoin_primitive_root CyclotomicRing.eq_adjoin_primitive_root end CyclotomicRing @@ -738,11 +694,9 @@ theorem IsAlgClosed.isCyclotomicExtension (h : ∀ a ∈ S, NeZero ((a : ℕ) : refine' ⟨r, _⟩ haveI := h a ha rwa [coe_aeval_eq_eval, ← IsRoot.def, isRoot_cyclotomic_iff] at hr -#align is_alg_closed.is_cyclotomic_extension IsAlgClosed.isCyclotomicExtension instance IsAlgClosedOfCharZero.isCyclotomicExtension [CharZero K] : ∀ S, IsCyclotomicExtension S K K := fun S => IsAlgClosed.isCyclotomicExtension S K fun _ _ => inferInstance -#align is_alg_closed_of_char_zero.is_cyclotomic_extension IsAlgClosedOfCharZero.isCyclotomicExtension end IsAlgClosed diff --git a/Mathlib/RingTheory/IntegralClosure.lean b/Mathlib/RingTheory/IntegralClosure.lean index c09543aebeccf..325434bb89e08 100644 --- a/Mathlib/RingTheory/IntegralClosure.lean +++ b/Mathlib/RingTheory/IntegralClosure.lean @@ -45,13 +45,11 @@ variable [CommRing R] [Ring A] [Ring S] (f : R →+* S) if it is a root of a monic polynomial `p : R[X]` evaluated under `f` -/ def RingHom.IsIntegralElem (f : R →+* A) (x : A) := ∃ p : R[X], Monic p ∧ eval₂ f x p = 0 -#align ring_hom.is_integral_elem RingHom.IsIntegralElem /-- A ring homomorphism `f : R →+* A` is said to be integral if every element `A` is integral with respect to the map `f` -/ def RingHom.IsIntegral (f : R →+* A) := ∀ x : A, f.IsIntegralElem x -#align ring_hom.is_integral RingHom.IsIntegral variable [Algebra R A] (R) @@ -60,24 +58,20 @@ if it is a root of some monic polynomial `p : R[X]`. Equivalently, the element is integral over `R` with respect to the induced `algebraMap` -/ def IsIntegral (x : A) : Prop := (algebraMap R A).IsIntegralElem x -#align is_integral IsIntegral variable (A) /-- An algebra is integral if every element of the extension is integral over the base ring -/ protected def Algebra.IsIntegral : Prop := (algebraMap R A).IsIntegral -#align algebra.is_integral Algebra.IsIntegral variable {R A} theorem RingHom.is_integral_map {x : R} : f.IsIntegralElem (f x) := ⟨X - C x, monic_X_sub_C _, by simp⟩ -#align ring_hom.is_integral_map RingHom.is_integral_map theorem isIntegral_algebraMap {x : R} : IsIntegral R (algebraMap R A x) := (algebraMap R A).is_integral_map -#align is_integral_algebra_map isIntegral_algebraMap theorem isIntegral_of_noetherian (H : IsNoetherian R A) (x : A) : IsIntegral R x := by let leval : R[X] →ₗ[R] A := (aeval x).toLinearMap @@ -96,7 +90,6 @@ theorem isIntegral_of_noetherian (H : IsNoetherian R A) (x : A) : IsIntegral R x refine' ⟨X ^ (N + 1) - p, monic_X_pow_sub (mem_degreeLE.1 hdp), _⟩ show leval (X ^ (N + 1) - p) = 0 rw [LinearMap.map_sub, hpe, sub_self] -#align is_integral_of_noetherian isIntegral_of_noetherian theorem isIntegral_of_submodule_noetherian (S : Subalgebra R A) (H : IsNoetherian R (Subalgebra.toSubmodule S)) (x : A) (hx : x ∈ S) : IsIntegral R x := by @@ -109,7 +102,6 @@ theorem isIntegral_of_submodule_noetherian (S : Subalgebra R A) refine' Finset.sum_congr rfl fun n _hn => _ rw [S.val.map_mul, S.val.map_pow, S.val.commutes, S.val_apply, Subtype.coe_mk] refine' isIntegral_of_noetherian H ⟨x, hx⟩ -#align is_integral_of_submodule_noetherian isIntegral_of_submodule_noetherian end Ring @@ -129,7 +121,6 @@ variable (A) /-- A field extension is integral if it is finite. -/ theorem Algebra.isIntegral_of_finite : Algebra.IsIntegral K A := fun x => isIntegral_of_submodule_noetherian ⊤ (IsNoetherian.iff_fg.2 inferInstance) x Algebra.mem_top -#align algebra.is_integral_of_finite Algebra.isIntegral_of_finite end @@ -148,7 +139,6 @@ theorem map_isIntegral {B C F : Type*} [Ring B] [Ring C] [Algebra R B] [Algebra refine' ⟨P, hP.1, _⟩ rw [← aeval_def, show (aeval (f b)) P = (aeval (f b)) (P.map (algebraMap R A)) by simp, aeval_algHom_apply, aeval_map_algebraMap, aeval_def, hP.2, _root_.map_zero] -#align map_is_integral map_isIntegral theorem isIntegral_map_of_comp_eq_of_isIntegral {R S T U : Type*} [CommRing R] [CommRing S] [CommRing T] [CommRing U] [Algebra R S] [Algebra T U] (φ : R →+* T) (ψ : S →+* U) @@ -159,7 +149,6 @@ theorem isIntegral_map_of_comp_eq_of_isIntegral {R S T U : Type*} [CommRing R] [ refine' ⟨p.map φ, hp.left.map _, _⟩ rw [← eval_map, map_map, h, ← map_map, eval_map, eval₂_at_apply, eval_map, hp.right, RingHom.map_zero] -#align is_integral_map_of_comp_eq_of_is_integral isIntegral_map_of_comp_eq_of_isIntegral theorem isIntegral_algHom_iff {A B : Type*} [Ring A] [Ring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (hf : Function.Injective f) {x : A} : IsIntegral R (f x) ↔ IsIntegral R x := by @@ -168,41 +157,34 @@ theorem isIntegral_algHom_iff {A B : Type*} [Ring A] [Ring B] [Algebra R A] [Alg use p, hp rwa [← f.comp_algebraMap, ← AlgHom.coe_toRingHom, ← Polynomial.hom_eval₂, AlgHom.coe_toRingHom, map_eq_zero_iff f hf] at hx -#align is_integral_alg_hom_iff isIntegral_algHom_iff @[simp] theorem isIntegral_algEquiv {A B : Type*} [Ring A] [Ring B] [Algebra R A] [Algebra R B] (f : A ≃ₐ[R] B) {x : A} : IsIntegral R (f x) ↔ IsIntegral R x := ⟨fun h => by simpa using map_isIntegral f.symm.toAlgHom h, map_isIntegral f.toAlgHom⟩ -#align is_integral_alg_equiv isIntegral_algEquiv theorem isIntegral_of_isScalarTower [Algebra A B] [IsScalarTower R A B] {x : B} (hx : IsIntegral R x) : IsIntegral A x := let ⟨p, hp, hpx⟩ := hx ⟨p.map <| algebraMap R A, hp.map _, by rw [← aeval_def, aeval_map_algebraMap, aeval_def, hpx]⟩ -#align is_integral_of_is_scalar_tower isIntegral_of_isScalarTower theorem map_isIntegral_int {B C F : Type*} [Ring B] [Ring C] {b : B} [RingHomClass F B C] (f : F) (hb : IsIntegral ℤ b) : IsIntegral ℤ (f b) := map_isIntegral (f : B →+* C).toIntAlgHom hb -#align map_is_integral_int map_isIntegral_int theorem isIntegral_ofSubring {x : A} (T : Subring R) (hx : IsIntegral T x) : IsIntegral R x := isIntegral_of_isScalarTower hx -#align is_integral_of_subring isIntegral_ofSubring theorem IsIntegral.algebraMap [Algebra A B] [IsScalarTower R A B] {x : A} (h : IsIntegral R x) : IsIntegral R (algebraMap A B x) := by rcases h with ⟨f, hf, hx⟩ use f, hf rw [IsScalarTower.algebraMap_eq R A B, ← hom_eval₂, hx, RingHom.map_zero] -#align is_integral.algebra_map IsIntegral.algebraMap theorem isIntegral_algebraMap_iff [Algebra A B] [IsScalarTower R A B] {x : A} (hAB : Function.Injective (algebraMap A B)) : IsIntegral R (algebraMap A B x) ↔ IsIntegral R x := isIntegral_algHom_iff (IsScalarTower.toAlgHom R A B) hAB -#align is_integral_algebra_map_iff isIntegral_algebraMap_iff theorem isIntegral_iff_isIntegral_closure_finite {r : A} : IsIntegral R r ↔ ∃ s : Set R, s.Finite ∧ IsIntegral (Subring.closure s) r := by @@ -212,7 +194,6 @@ theorem isIntegral_iff_isIntegral_closure_finite {r : A} : rw [← aeval_def, ← aeval_map_algebraMap R r p.restriction, map_restriction, aeval_def, hpr] rcases hr with ⟨s, _, hsr⟩ exact isIntegral_ofSubring _ hsr -#align is_integral_iff_is_integral_closure_finite isIntegral_iff_isIntegral_closure_finite theorem FG_adjoin_singleton_of_integral (x : A) (hx : IsIntegral R x) : (Algebra.adjoin R ({x} : Set A)).toSubmodule.FG := by @@ -242,7 +223,6 @@ theorem FG_adjoin_singleton_of_integral (x : A) (hx : IsIntegral R x) : rw [degree_le_iff_coeff_zero] at this rw [mem_support_iff] at hkq; apply hkq; apply this exact lt_of_le_of_lt degree_le_natDegree (WithBot.coe_lt_coe.2 hk) -#align fg_adjoin_singleton_of_integral FG_adjoin_singleton_of_integral theorem FG_adjoin_of_finite {s : Set A} (hfs : s.Finite) (his : ∀ x ∈ s, IsIntegral R x) : (Algebra.adjoin R s).toSubmodule.FG := @@ -257,12 +237,10 @@ theorem FG_adjoin_of_finite {s : Set A} (hfs : s.Finite) (his : ∀ x ∈ s, IsI FG.mul (ih fun i hi => his i <| Set.mem_insert_of_mem a hi) (FG_adjoin_singleton_of_integral _ <| his a <| Set.mem_insert a s)) his -#align fg_adjoin_of_finite FG_adjoin_of_finite theorem isNoetherian_adjoin_finset [IsNoetherianRing R] (s : Finset A) (hs : ∀ x ∈ s, IsIntegral R x) : IsNoetherian R (Algebra.adjoin R (↑s : Set A)) := isNoetherian_of_fg_of_noetherian _ (FG_adjoin_of_finite s.finite_toSet hs) -#align is_noetherian_adjoin_finset isNoetherian_adjoin_finset /-- If `S` is a sub-`R`-algebra of `A` and `S` is finitely-generated as an `R`-module, then all elements of `S` are integral over `R`. -/ @@ -365,12 +343,10 @@ theorem isIntegral_of_mem_of_FG (S : Subalgebra R A) (HS : S.toSubmodule.FG) (x change (⟨_, this⟩ : S₀) • r ∈ _ rw [Finsupp.mem_supported] at hlx1 exact Subalgebra.smul_mem _ (Algebra.subset_adjoin <| hlx1 hr) _ -#align is_integral_of_mem_of_fg isIntegral_of_mem_of_FG theorem Module.End.isIntegral {M : Type*} [AddCommGroup M] [Module R M] [Module.Finite R M] : Algebra.IsIntegral R (Module.End R M) := LinearMap.exists_monic_and_aeval_eq_zero R -#align module.End.is_integral Module.End.isIntegral /-- Suppose `A` is an `R`-algebra, `M` is an `A`-module such that `a • m ≠ 0` for all non-zero `a` and `m`. If `x : A` fixes a nontrivial f.g. `R`-submodule `N` of `M`, then `x` is `R`-integral. -/ @@ -413,17 +389,14 @@ theorem isIntegral_of_smul_mem_submodule {M : Type*} [AddCommGroup M] [Module R rw [isIntegral_algHom_iff A'.val Subtype.val_injective, ← isIntegral_algHom_iff f this] haveI : Module.Finite R N := by rwa [Module.finite_def, Submodule.fg_top] apply Module.End.isIntegral -#align is_integral_of_smul_mem_submodule isIntegral_of_smul_mem_submodule variable {f} theorem RingHom.Finite.to_isIntegral (h : f.Finite) : f.IsIntegral := letI := f.toAlgebra fun _ => isIntegral_of_mem_of_FG ⊤ h.1 _ trivial -#align ring_hom.finite.to_is_integral RingHom.Finite.to_isIntegral alias RingHom.IsIntegral.of_finite := RingHom.Finite.to_isIntegral -#align ring_hom.is_integral.of_finite RingHom.IsIntegral.of_finite theorem RingHom.IsIntegral.to_finite (h : f.IsIntegral) (h' : f.FiniteType) : f.Finite := by letI := f.toAlgebra @@ -432,15 +405,12 @@ theorem RingHom.IsIntegral.to_finite (h : f.IsIntegral) (h' : f.FiniteType) : f. change (⊤ : Subalgebra R S).toSubmodule.FG rw [← hs] exact FG_adjoin_of_finite (Set.toFinite _) fun x _ => h x -#align ring_hom.is_integral.to_finite RingHom.IsIntegral.to_finite alias RingHom.Finite.of_isIntegral_of_finiteType := RingHom.IsIntegral.to_finite -#align ring_hom.finite.of_is_integral_of_finite_type RingHom.Finite.of_isIntegral_of_finiteType /-- finite = integral + finite type -/ theorem RingHom.finite_iff_isIntegral_and_finiteType : f.Finite ↔ f.IsIntegral ∧ f.FiniteType := ⟨fun h => ⟨h.to_isIntegral, h.to_finiteType⟩, fun ⟨h, h'⟩ => h.to_finite h'⟩ -#align ring_hom.finite_iff_is_integral_and_finite_type RingHom.finite_iff_isIntegral_and_finiteType theorem Algebra.IsIntegral.finite (h : Algebra.IsIntegral R A) [h' : Algebra.FiniteType R A] : Module.Finite R A := by @@ -456,17 +426,14 @@ theorem Algebra.IsIntegral.finite (h : Algebra.IsIntegral R A) [h' : Algebra.Fin convert this ext exact Algebra.smul_def _ _ -#align algebra.is_integral.finite Algebra.IsIntegral.finite theorem Algebra.IsIntegral.of_finite [h : Module.Finite R A] : Algebra.IsIntegral R A := fun _ ↦ isIntegral_of_mem_of_FG ⊤ h.1 _ trivial -#align algebra.is_integral.of_finite Algebra.IsIntegral.of_finite /-- finite = integral + finite type -/ theorem Algebra.finite_iff_isIntegral_and_finiteType : Module.Finite R A ↔ Algebra.IsIntegral R A ∧ Algebra.FiniteType R A := ⟨fun _ => ⟨Algebra.IsIntegral.of_finite, inferInstance⟩, fun ⟨h, _⟩ => h.finite⟩ -#align algebra.finite_iff_is_integral_and_finite_type Algebra.finite_iff_isIntegral_and_finiteType variable (f) @@ -478,74 +445,59 @@ theorem RingHom.is_integral_of_mem_closure {x y z : S} (hx : f.IsIntegralElem x) exact isIntegral_of_mem_of_FG (Algebra.adjoin R {x, y}) this z (Algebra.mem_adjoin_iff.2 <| Subring.closure_mono (Set.subset_union_right _ _) hz) -#align ring_hom.is_integral_of_mem_closure RingHom.is_integral_of_mem_closure theorem isIntegral_of_mem_closure {x y z : A} (hx : IsIntegral R x) (hy : IsIntegral R y) (hz : z ∈ Subring.closure ({x, y} : Set A)) : IsIntegral R z := (algebraMap R A).is_integral_of_mem_closure hx hy hz -#align is_integral_of_mem_closure isIntegral_of_mem_closure theorem RingHom.is_integral_zero : f.IsIntegralElem 0 := f.map_zero ▸ f.is_integral_map -#align ring_hom.is_integral_zero RingHom.is_integral_zero theorem isIntegral_zero : IsIntegral R (0 : A) := (algebraMap R A).is_integral_zero -#align is_integral_zero isIntegral_zero theorem RingHom.is_integral_one : f.IsIntegralElem 1 := f.map_one ▸ f.is_integral_map -#align ring_hom.is_integral_one RingHom.is_integral_one theorem isIntegral_one : IsIntegral R (1 : A) := (algebraMap R A).is_integral_one -#align is_integral_one isIntegral_one theorem RingHom.is_integral_add {x y : S} (hx : f.IsIntegralElem x) (hy : f.IsIntegralElem y) : f.IsIntegralElem (x + y) := f.is_integral_of_mem_closure hx hy <| Subring.add_mem _ (Subring.subset_closure (Or.inl rfl)) (Subring.subset_closure (Or.inr rfl)) -#align ring_hom.is_integral_add RingHom.is_integral_add theorem isIntegral_add {x y : A} (hx : IsIntegral R x) (hy : IsIntegral R y) : IsIntegral R (x + y) := (algebraMap R A).is_integral_add hx hy -#align is_integral_add isIntegral_add theorem RingHom.is_integral_neg {x : S} (hx : f.IsIntegralElem x) : f.IsIntegralElem (-x) := f.is_integral_of_mem_closure hx hx (Subring.neg_mem _ (Subring.subset_closure (Or.inl rfl))) -#align ring_hom.is_integral_neg RingHom.is_integral_neg theorem isIntegral_neg {x : A} (hx : IsIntegral R x) : IsIntegral R (-x) := (algebraMap R A).is_integral_neg hx -#align is_integral_neg isIntegral_neg theorem RingHom.is_integral_sub {x y : S} (hx : f.IsIntegralElem x) (hy : f.IsIntegralElem y) : f.IsIntegralElem (x - y) := by simpa only [sub_eq_add_neg] using f.is_integral_add hx (f.is_integral_neg hy) -#align ring_hom.is_integral_sub RingHom.is_integral_sub theorem isIntegral_sub {x y : A} (hx : IsIntegral R x) (hy : IsIntegral R y) : IsIntegral R (x - y) := (algebraMap R A).is_integral_sub hx hy -#align is_integral_sub isIntegral_sub theorem RingHom.is_integral_mul {x y : S} (hx : f.IsIntegralElem x) (hy : f.IsIntegralElem y) : f.IsIntegralElem (x * y) := f.is_integral_of_mem_closure hx hy (Subring.mul_mem _ (Subring.subset_closure (Or.inl rfl)) (Subring.subset_closure (Or.inr rfl))) -#align ring_hom.is_integral_mul RingHom.is_integral_mul theorem isIntegral_mul {x y : A} (hx : IsIntegral R x) (hy : IsIntegral R y) : IsIntegral R (x * y) := (algebraMap R A).is_integral_mul hx hy -#align is_integral_mul isIntegral_mul theorem isIntegral_smul [Algebra S A] [Algebra R S] [IsScalarTower R S A] {x : A} (r : R) (hx : IsIntegral S x) : IsIntegral S (r • x) := by rw [Algebra.smul_def, IsScalarTower.algebraMap_apply R S A] exact isIntegral_mul isIntegral_algebraMap hx -#align is_integral_smul isIntegral_smul theorem isIntegral_of_pow {x : A} {n : ℕ} (hn : 0 < n) (hx : IsIntegral R <| x ^ n) : IsIntegral R x := by @@ -553,7 +505,6 @@ theorem isIntegral_of_pow {x : A} {n : ℕ} (hn : 0 < n) (hx : IsIntegral R <| x exact ⟨expand R n p, Monic.expand hn hmonic, by rwa [eval₂_eq_eval_map, map_expand, expand_eval, ← eval₂_eq_eval_map]⟩ -#align is_integral_of_pow isIntegral_of_pow variable (R A) @@ -565,14 +516,12 @@ def integralClosure : Subalgebra R A where add_mem' := isIntegral_add mul_mem' := isIntegral_mul algebraMap_mem' _ := isIntegral_algebraMap -#align integral_closure integralClosure theorem mem_integralClosure_iff_mem_FG {r : A} : r ∈ integralClosure R A ↔ ∃ M : Subalgebra R A, M.toSubmodule.FG ∧ r ∈ M := ⟨fun hr => ⟨Algebra.adjoin R {r}, FG_adjoin_singleton_of_integral _ hr, Algebra.subset_adjoin rfl⟩, fun ⟨M, Hf, hrM⟩ => isIntegral_of_mem_of_FG M Hf _ hrM⟩ -#align mem_integral_closure_iff_mem_fg mem_integralClosure_iff_mem_FG variable {R} {A} @@ -581,7 +530,6 @@ theorem adjoin_le_integralClosure {x : A} (hx : IsIntegral R x) : rw [Algebra.adjoin_le_iff] simp only [SetLike.mem_coe, Set.singleton_subset_iff] exact hx -#align adjoin_le_integral_closure adjoin_le_integralClosure theorem le_integralClosure_iff_isIntegral {S : Subalgebra R A} : S ≤ integralClosure R A ↔ Algebra.IsIntegral R S := @@ -589,13 +537,11 @@ theorem le_integralClosure_iff_isIntegral {S : Subalgebra R A} : (forall_congr' fun x => show IsIntegral R (algebraMap S A x) ↔ IsIntegral R x from isIntegral_algebraMap_iff Subtype.coe_injective) -#align le_integral_closure_iff_is_integral le_integralClosure_iff_isIntegral theorem isIntegral_sup {S T : Subalgebra R A} : Algebra.IsIntegral R (S ⊔ T : Subalgebra R A) ↔ Algebra.IsIntegral R S ∧ Algebra.IsIntegral R T := by simp only [← le_integralClosure_iff_isIntegral, sup_le_iff] -#align is_integral_sup isIntegral_sup /-- Mapping an integral closure along an `AlgEquiv` gives the integral closure. -/ theorem integralClosure_map_algEquiv (f : A ≃ₐ[R] B) : @@ -608,14 +554,12 @@ theorem integralClosure_map_algEquiv (f : A ≃ₐ[R] B) : · intro hy use f.symm y, map_isIntegral (f.symm : B →ₐ[R] A) hy simp -#align integral_closure_map_alg_equiv integralClosure_map_algEquiv theorem integralClosure.isIntegral (x : integralClosure R A) : IsIntegral R x := let ⟨p, hpm, hpx⟩ := x.2 ⟨p, hpm, Subtype.eq <| by rwa [← aeval_def, ← Subalgebra.val_apply, aeval_algHom_apply] at hpx⟩ -#align integral_closure.is_integral integralClosure.isIntegral theorem RingHom.isIntegral_of_isIntegral_mul_unit (x y : S) (r : R) (hr : f r * y = 1) (hx : f.IsIntegralElem (x * y)) : f.IsIntegralElem x := by @@ -623,67 +567,54 @@ theorem RingHom.isIntegral_of_isIntegral_mul_unit (x y : S) (r : R) (hr : f r * refine' ⟨scaleRoots p r, ⟨(monic_scaleRoots_iff r).2 p_monic, _⟩⟩ convert scaleRoots_eval₂_eq_zero f hp rw [mul_comm x y, ← mul_assoc, hr, one_mul] -#align ring_hom.is_integral_of_is_integral_mul_unit RingHom.isIntegral_of_isIntegral_mul_unit theorem isIntegral_of_isIntegral_mul_unit {x y : A} {r : R} (hr : algebraMap R A r * y = 1) (hx : IsIntegral R (x * y)) : IsIntegral R x := (algebraMap R A).isIntegral_of_isIntegral_mul_unit x y r hr hx -#align is_integral_of_is_integral_mul_unit isIntegral_of_isIntegral_mul_unit /-- Generalization of `isIntegral_of_mem_closure` bootstrapped up from that lemma -/ theorem isIntegral_of_mem_closure' (G : Set A) (hG : ∀ x ∈ G, IsIntegral R x) : ∀ x ∈ Subring.closure G, IsIntegral R x := fun _ hx => Subring.closure_induction hx hG isIntegral_zero isIntegral_one (fun _ _ => isIntegral_add) (fun _ => isIntegral_neg) fun _ _ => isIntegral_mul -#align is_integral_of_mem_closure' isIntegral_of_mem_closure' theorem isIntegral_of_mem_closure'' {S : Type*} [CommRing S] {f : R →+* S} (G : Set S) (hG : ∀ x ∈ G, f.IsIntegralElem x) : ∀ x ∈ Subring.closure G, f.IsIntegralElem x := fun x hx => @isIntegral_of_mem_closure' R S _ _ f.toAlgebra G hG x hx -#align is_integral_of_mem_closure'' isIntegral_of_mem_closure'' theorem IsIntegral.pow {x : A} (h : IsIntegral R x) (n : ℕ) : IsIntegral R (x ^ n) := (integralClosure R A).pow_mem h n -#align is_integral.pow IsIntegral.pow theorem IsIntegral.nsmul {x : A} (h : IsIntegral R x) (n : ℕ) : IsIntegral R (n • x) := (integralClosure R A).nsmul_mem h n -#align is_integral.nsmul IsIntegral.nsmul theorem IsIntegral.zsmul {x : A} (h : IsIntegral R x) (n : ℤ) : IsIntegral R (n • x) := (integralClosure R A).zsmul_mem h n -#align is_integral.zsmul IsIntegral.zsmul theorem IsIntegral.multiset_prod {s : Multiset A} (h : ∀ x ∈ s, IsIntegral R x) : IsIntegral R s.prod := (integralClosure R A).multiset_prod_mem h -#align is_integral.multiset_prod IsIntegral.multiset_prod theorem IsIntegral.multiset_sum {s : Multiset A} (h : ∀ x ∈ s, IsIntegral R x) : IsIntegral R s.sum := (integralClosure R A).multiset_sum_mem h -#align is_integral.multiset_sum IsIntegral.multiset_sum theorem IsIntegral.prod {α : Type*} {s : Finset α} (f : α → A) (h : ∀ x ∈ s, IsIntegral R (f x)) : IsIntegral R (∏ x in s, f x) := (integralClosure R A).prod_mem h -#align is_integral.prod IsIntegral.prod theorem IsIntegral.sum {α : Type*} {s : Finset α} (f : α → A) (h : ∀ x ∈ s, IsIntegral R (f x)) : IsIntegral R (∑ x in s, f x) := (integralClosure R A).sum_mem h -#align is_integral.sum IsIntegral.sum theorem IsIntegral.det {n : Type*} [Fintype n] [DecidableEq n] {M : Matrix n n A} (h : ∀ i j, IsIntegral R (M i j)) : IsIntegral R M.det := by rw [Matrix.det_apply] exact IsIntegral.sum _ fun σ _hσ => IsIntegral.zsmul (IsIntegral.prod _ fun i _hi => h _ _) _ -#align is_integral.det IsIntegral.det @[simp] theorem IsIntegral.pow_iff {x : A} {n : ℕ} (hn : 0 < n) : IsIntegral R (x ^ n) ↔ IsIntegral R x := ⟨isIntegral_of_pow hn, fun hx => IsIntegral.pow hx n⟩ -#align is_integral.pow_iff IsIntegral.pow_iff open TensorProduct @@ -707,7 +638,6 @@ theorem IsIntegral.tmul (x : A) {y : B} (h : IsIntegral R y) : IsIntegral A (x convert Polynomial.eval₂_at_apply (Algebra.TensorProduct.includeRight : B →ₐ[R] A ⊗[R] B).toRingHom y rw [Polynomial.eval_map, hp', _root_.map_zero] -#align is_integral.tmul IsIntegral.tmul section @@ -717,7 +647,6 @@ variable (p : R[X]) (x : S) noncomputable def normalizeScaleRoots (p : R[X]) : R[X] := ∑ i in p.support, monomial i (if i = p.natDegree then 1 else p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i)) -#align normalize_scale_roots normalizeScaleRoots theorem normalizeScaleRoots_coeff_mul_leadingCoeff_pow (i : ℕ) (hp : 1 ≤ natDegree p) : (normalizeScaleRoots p).coeff i * p.leadingCoeff ^ i = @@ -731,7 +660,6 @@ theorem normalizeScaleRoots_coeff_mul_leadingCoeff_pow (i : ℕ) (hp : 1 ≤ nat apply Nat.le_sub_one_of_lt rw [lt_iff_le_and_ne] exact ⟨le_natDegree_of_ne_zero h₁, h₂⟩ -#align normalize_scale_roots_coeff_mul_leading_coeff_pow normalizeScaleRoots_coeff_mul_leadingCoeff_pow theorem leadingCoeff_smul_normalizeScaleRoots (p : R[X]) : p.leadingCoeff • normalizeScaleRoots p = scaleRoots p p.leadingCoeff := by @@ -748,7 +676,6 @@ theorem leadingCoeff_smul_normalizeScaleRoots (p : R[X]) : tsub_add_cancel_of_le] rw [Nat.succ_le_iff] exact tsub_pos_of_lt (lt_of_le_of_ne (le_natDegree_of_ne_zero h₁) h₂) -#align leading_coeff_smul_normalize_scale_roots leadingCoeff_smul_normalizeScaleRoots theorem normalizeScaleRoots_support : (normalizeScaleRoots p).support ≤ p.support := by intro x @@ -757,14 +684,12 @@ theorem normalizeScaleRoots_support : (normalizeScaleRoots p).support ≤ p.supp Finset.sum_ite_eq', mem_support_iff, Ne.def, Classical.not_not, ite_eq_right_iff] intro h₁ h₂ exact (h₂ h₁).elim -#align normalize_scale_roots_support normalizeScaleRoots_support theorem normalizeScaleRoots_degree : (normalizeScaleRoots p).degree = p.degree := by apply le_antisymm · exact Finset.sup_mono (normalizeScaleRoots_support p) · rw [← degree_scaleRoots, ← leadingCoeff_smul_normalizeScaleRoots] exact degree_smul_le _ _ -#align normalize_scale_roots_degree normalizeScaleRoots_degree theorem normalizeScaleRoots_eval₂_leadingCoeff_mul (h : 1 ≤ p.natDegree) (f : R →+* S) (x : S) : (normalizeScaleRoots p).eval₂ f (f p.leadingCoeff * x) = @@ -776,14 +701,12 @@ theorem normalizeScaleRoots_eval₂_leadingCoeff_mul (h : 1 ≤ p.natDegree) (f rw [mul_pow, ← mul_assoc, ← f.map_pow, ← f.map_mul, normalizeScaleRoots_coeff_mul_leadingCoeff_pow _ _ h, f.map_mul, f.map_pow] ring -#align normalize_scale_roots_eval₂_leading_coeff_mul normalizeScaleRoots_eval₂_leadingCoeff_mul theorem normalizeScaleRoots_monic (h : p ≠ 0) : (normalizeScaleRoots p).Monic := by delta Monic leadingCoeff rw [natDegree_eq_of_degree_eq (normalizeScaleRoots_degree p)] suffices p = 0 → (0 : R) = 1 by simpa [normalizeScaleRoots, coeff_monomial] exact fun h' => (h h').elim -#align normalize_scale_roots_monic normalizeScaleRoots_monic /-- Given a `p : R[X]` and a `x : S` such that `p.eval₂ f x = 0`, `f p.leadingCoeff * x` is integral. -/ @@ -805,7 +728,6 @@ theorem RingHom.isIntegralElem_leadingCoeff_mul (h : p.eval₂ f x = 0) : rw [eq_C_of_natDegree_eq_zero h', eval₂_C] at h suffices p.map f = 0 by exact (hp this).elim rw [eq_C_of_natDegree_eq_zero h', map_C, h, C_eq_zero] -#align ring_hom.is_integral_elem_leading_coeff_mul RingHom.isIntegralElem_leadingCoeff_mul /-- Given a `p : R[X]` and a root `x : S`, then `p.leadingCoeff • x : S` is integral over `R`. -/ @@ -814,7 +736,6 @@ theorem isIntegral_leadingCoeff_smul [Algebra R S] (h : aeval x p = 0) : rw [aeval_def] at h rw [Algebra.smul_def] exact (algebraMap R S).isIntegralElem_leadingCoeff_mul p x h -#align is_integral_leading_coeff_smul isIntegral_leadingCoeff_smul end @@ -830,13 +751,11 @@ class IsIntegralClosure (A R B : Type*) [CommRing R] [CommSemiring A] [CommRing [Algebra A B] : Prop where algebraMap_injective' : Function.Injective (algebraMap A B) isIntegral_iff : ∀ {x : B}, IsIntegral R x ↔ ∃ y, algebraMap A B y = x -#align is_integral_closure IsIntegralClosure instance integralClosure.isIntegralClosure (R A : Type*) [CommRing R] [CommRing A] [Algebra R A] : IsIntegralClosure (integralClosure R A) R A where algebraMap_injective' := Subtype.coe_injective isIntegral_iff {x} := ⟨fun h => ⟨⟨x, h⟩, rfl⟩, by rintro ⟨⟨_, h⟩, rfl⟩; exact h⟩ -#align integral_closure.is_integral_closure integralClosure.isIntegralClosure namespace IsIntegralClosure @@ -854,11 +773,9 @@ variable (R) (B) -- porting note: `{A}` was a `redundant binder annotation updat protected theorem isIntegral [Algebra R A] [IsScalarTower R A B] (x : A) : IsIntegral R x := (isIntegral_algebraMap_iff (algebraMap_injective A R B)).mp <| show IsIntegral R (algebraMap A B x) from isIntegral_iff.mpr ⟨x, rfl⟩ -#align is_integral_closure.is_integral IsIntegralClosure.isIntegral theorem isIntegral_algebra [Algebra R A] [IsScalarTower R A B] : Algebra.IsIntegral R A := fun x => IsIntegralClosure.isIntegral R B x -#align is_integral_closure.is_integral_algebra IsIntegralClosure.isIntegral_algebra theorem noZeroSMulDivisors [Algebra R A] [IsScalarTower R A B] [NoZeroSMulDivisors R B] : NoZeroSMulDivisors R A := by @@ -866,48 +783,40 @@ theorem noZeroSMulDivisors [Algebra R A] [IsScalarTower R A B] [NoZeroSMulDiviso Function.Injective.noZeroSMulDivisors _ (IsIntegralClosure.algebraMap_injective A R B) (map_zero _) fun _ _ => _ simp only [Algebra.algebraMap_eq_smul_one, IsScalarTower.smul_assoc] -#align is_integral_closure.no_zero_smul_divisors IsIntegralClosure.noZeroSMulDivisors variable {R} (A) {B} /-- If `x : B` is integral over `R`, then it is an element of the integral closure of `R` in `B`. -/ noncomputable def mk' (x : B) (hx : IsIntegral R x) : A := Classical.choose (isIntegral_iff.mp hx) -#align is_integral_closure.mk' IsIntegralClosure.mk' @[simp] theorem algebraMap_mk' (x : B) (hx : IsIntegral R x) : algebraMap A B (mk' A x hx) = x := Classical.choose_spec (isIntegral_iff.mp hx) -#align is_integral_closure.algebra_map_mk' IsIntegralClosure.algebraMap_mk' @[simp] theorem mk'_one (h : IsIntegral R (1 : B) := isIntegral_one) : mk' A 1 h = 1 := algebraMap_injective A R B <| by rw [algebraMap_mk', RingHom.map_one] -#align is_integral_closure.mk'_one IsIntegralClosure.mk'_one @[simp] theorem mk'_zero (h : IsIntegral R (0 : B) := isIntegral_zero) : mk' A 0 h = 0 := algebraMap_injective A R B <| by rw [algebraMap_mk', RingHom.map_zero] -#align is_integral_closure.mk'_zero IsIntegralClosure.mk'_zero -- Porting note: Left-hand side does not simplify @[simp] theorem mk'_add (x y : B) (hx : IsIntegral R x) (hy : IsIntegral R y) : mk' A (x + y) (isIntegral_add hx hy) = mk' A x hx + mk' A y hy := algebraMap_injective A R B <| by simp only [algebraMap_mk', RingHom.map_add] -#align is_integral_closure.mk'_add IsIntegralClosure.mk'_add -- Porting note: Left-hand side does not simplify @[simp] theorem mk'_mul (x y : B) (hx : IsIntegral R x) (hy : IsIntegral R y) : mk' A (x * y) (isIntegral_mul hx hy) = mk' A x hx * mk' A y hy := algebraMap_injective A R B <| by simp only [algebraMap_mk', RingHom.map_mul] -#align is_integral_closure.mk'_mul IsIntegralClosure.mk'_mul @[simp] theorem mk'_algebraMap [Algebra R A] [IsScalarTower R A B] (x : R) (h : IsIntegral R (algebraMap R B x) := isIntegral_algebraMap) : IsIntegralClosure.mk' A (algebraMap R B x) h = algebraMap R A x := algebraMap_injective A R B <| by rw [algebraMap_mk', ← IsScalarTower.algebraMap_apply] -#align is_integral_closure.mk'_algebra_map IsIntegralClosure.mk'_algebraMap section lift @@ -927,12 +836,10 @@ noncomputable def lift : S →ₐ[R] A where map_add' x y := by simp_rw [← mk'_add, RingHom.map_add] map_mul' x y := by simp_rw [← mk'_mul, RingHom.map_mul] commutes' x := by simp_rw [← IsScalarTower.algebraMap_apply, mk'_algebraMap] -#align is_integral_closure.lift IsIntegralClosure.lift @[simp] theorem algebraMap_lift (x : S) : algebraMap A B (lift A B h x) = algebraMap S B x := algebraMap_mk' A (algebraMap S B x) (IsIntegral.algebraMap (h x)) -#align is_integral_closure.algebra_map_lift IsIntegralClosure.algebraMap_lift end lift @@ -954,12 +861,10 @@ noncomputable def equiv : A ≃ₐ[R] A' := ext x apply algebraMap_injective A R B simp) -#align is_integral_closure.equiv IsIntegralClosure.equiv @[simp] theorem algebraMap_equiv (x : A) : algebraMap A' B (equiv R A B A' x) = algebraMap A B x := algebraMap_lift A' B (isIntegral_algebra R B) x -#align is_integral_closure.algebra_map_equiv IsIntegralClosure.algebraMap_equiv end Equiv @@ -1001,7 +906,6 @@ theorem isIntegral_trans_aux (x : B) {p : A[X]} (pmonic : Monic p) (hp : aeval x · convert hp using 1 replace hq := congr_arg (eval x) hq convert hq using 1 <;> symm <;> apply eval_map -#align is_integral_trans_aux isIntegral_trans_aux variable [Algebra R A] [IsScalarTower R A B] @@ -1019,7 +923,6 @@ theorem isIntegral_trans (A_int : Algebra.IsIntegral R A) (x : B) (hx : IsIntegr exact map_isIntegral (IsScalarTower.toAlgHom R A B) (A_int _) · apply FG_adjoin_singleton_of_integral exact isIntegral_trans_aux _ pmonic hp -#align is_integral_trans isIntegral_trans /-- If A is an R-algebra all of whose elements are integral over R, and B is an A-algebra all of whose elements are integral over A, @@ -1027,23 +930,19 @@ then all elements of B are integral over R.-/ nonrec theorem Algebra.isIntegral_trans (hA : Algebra.IsIntegral R A) (hB : Algebra.IsIntegral A B) : Algebra.IsIntegral R B := fun x => isIntegral_trans hA x (hB x) -#align algebra.is_integral_trans Algebra.isIntegral_trans theorem RingHom.isIntegral_trans (hf : f.IsIntegral) (hg : g.IsIntegral) : (g.comp f).IsIntegral := @Algebra.isIntegral_trans R S T _ _ _ g.toAlgebra (g.comp f).toAlgebra f.toAlgebra (@IsScalarTower.of_algebraMap_eq R S T _ _ _ f.toAlgebra g.toAlgebra (g.comp f).toAlgebra (RingHom.comp_apply g f)) hf hg -#align ring_hom.is_integral_trans RingHom.isIntegral_trans theorem RingHom.isIntegral_of_surjective (hf : Function.Surjective f) : f.IsIntegral := fun x => (hf x).recOn fun _y hy => (hy ▸ f.is_integral_map : f.IsIntegralElem x) -#align ring_hom.is_integral_of_surjective RingHom.isIntegral_of_surjective theorem isIntegral_of_surjective (h : Function.Surjective (algebraMap R A)) : Algebra.IsIntegral R A := (algebraMap R A).isIntegral_of_surjective h -#align is_integral_of_surjective isIntegral_of_surjective /-- If `R → A → B` is an algebra tower with `A → B` injective, then if the entire tower is an integral extension so is `R → A` -/ @@ -1055,7 +954,6 @@ theorem isIntegral_tower_bot_of_isIntegral (H : Function.Injective (algebraMap A RingHom.map_zero (algebraMap A B)] at hp' rw [eval₂_eq_eval_map] exact H hp' -#align is_integral_tower_bot_of_is_integral isIntegral_tower_bot_of_isIntegral nonrec theorem RingHom.isIntegral_tower_bot_of_isIntegral (hg : Function.Injective g) (hfg : (g.comp f).IsIntegral) : f.IsIntegral := fun x => @@ -1063,23 +961,19 @@ nonrec theorem RingHom.isIntegral_tower_bot_of_isIntegral (hg : Function.Injecti (@IsScalarTower.of_algebraMap_eq R S T _ _ _ f.toAlgebra g.toAlgebra (g.comp f).toAlgebra (RingHom.comp_apply g f)) hg x (hfg (g x)) -#align ring_hom.is_integral_tower_bot_of_is_integral RingHom.isIntegral_tower_bot_of_isIntegral theorem isIntegral_tower_bot_of_isIntegral_field {R A B : Type*} [CommRing R] [Field A] [CommRing B] [Nontrivial B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] {x : A} (h : IsIntegral R (algebraMap A B x)) : IsIntegral R x := isIntegral_tower_bot_of_isIntegral (algebraMap A B).injective h -#align is_integral_tower_bot_of_is_integral_field isIntegral_tower_bot_of_isIntegral_field theorem RingHom.isIntegralElem_of_isIntegralElem_comp {x : T} (h : (g.comp f).IsIntegralElem x) : g.IsIntegralElem x := let ⟨p, ⟨hp, hp'⟩⟩ := h ⟨p.map f, hp.map f, by rwa [← eval₂_map] at hp'⟩ -#align ring_hom.is_integral_elem_of_is_integral_elem_comp RingHom.isIntegralElem_of_isIntegralElem_comp theorem RingHom.isIntegral_tower_top_of_isIntegral (h : (g.comp f).IsIntegral) : g.IsIntegral := fun x => RingHom.isIntegralElem_of_isIntegralElem_comp f g (h x) -#align ring_hom.is_integral_tower_top_of_is_integral RingHom.isIntegral_tower_top_of_isIntegral /-- If `R → A → B` is an algebra tower, then if the entire tower is an integral extension so is `A → B`. -/ @@ -1088,7 +982,6 @@ theorem isIntegral_tower_top_of_isIntegral {x : B} (h : IsIntegral R x) : IsInte refine' ⟨p.map (algebraMap R A), ⟨hp.map (algebraMap R A), _⟩⟩ rw [IsScalarTower.algebraMap_eq R A B, ← eval₂_map] at hp' exact hp' -#align is_integral_tower_top_of_is_integral isIntegral_tower_top_of_isIntegral theorem RingHom.isIntegral_quotient_of_isIntegral {I : Ideal S} (hf : f.IsIntegral) : (Ideal.quotientMap I f le_rfl).IsIntegral := by @@ -1096,12 +989,10 @@ theorem RingHom.isIntegral_quotient_of_isIntegral {I : Ideal S} (hf : f.IsIntegr obtain ⟨p, ⟨p_monic, hpx⟩⟩ := hf x refine' ⟨p.map (Ideal.Quotient.mk _), ⟨p_monic.map _, _⟩⟩ simpa only [hom_eval₂, eval₂_map] using congr_arg (Ideal.Quotient.mk I) hpx -#align ring_hom.is_integral_quotient_of_is_integral RingHom.isIntegral_quotient_of_isIntegral theorem isIntegral_quotient_of_isIntegral {I : Ideal A} (hRA : Algebra.IsIntegral R A) : Algebra.IsIntegral (R ⧸ I.comap (algebraMap R A)) (A ⧸ I) := (algebraMap R A).isIntegral_quotient_of_isIntegral hRA -#align is_integral_quotient_of_is_integral isIntegral_quotient_of_isIntegral theorem isIntegral_quotientMap_iff {I : Ideal S} : (Ideal.quotientMap I f le_rfl).IsIntegral ↔ @@ -1113,7 +1004,6 @@ theorem isIntegral_quotientMap_iff {I : Ideal S} : refine' ⟨fun h => _, fun h => RingHom.isIntegral_tower_top_of_isIntegral g _ (this ▸ h)⟩ refine' this ▸ RingHom.isIntegral_trans g (Ideal.quotientMap I f le_rfl) _ h exact RingHom.isIntegral_of_surjective g Ideal.Quotient.mk_surjective -#align is_integral_quotient_map_iff isIntegral_quotientMap_iff /-- If the integral extension `R → S` is injective, and `S` is a field, then `R` is also a field. -/ theorem isField_of_isIntegral_of_isField {R S : Type*} [CommRing R] [Nontrivial R] [CommRing S] @@ -1152,7 +1042,6 @@ theorem isField_of_isIntegral_of_isField {R S : Type*} [CommRing R] [Nontrivial refine' Finset.sum_congr rfl fun i hi => _ have : 1 ≤ p.natDegree - i := le_tsub_of_add_le_left (Finset.mem_range.mp hi) rw [mul_assoc, ← pow_succ', tsub_add_cancel_of_le this] -#align is_field_of_is_integral_of_is_field isField_of_isIntegral_of_isField theorem isField_of_isIntegral_of_isField' {R S : Type*} [CommRing R] [CommRing S] [IsDomain S] [Algebra R S] (H : Algebra.IsIntegral R S) (hR : IsField R) : IsField S := by @@ -1169,13 +1058,11 @@ theorem isField_of_isIntegral_of_isField' {R S : Type*} [CommRing R] [CommRing S hx (Subtype.ext_iff.mp h)) 1 exact ⟨y, Subtype.ext_iff.mp hy⟩ -#align is_field_of_is_integral_of_is_field' isField_of_isIntegral_of_isField' theorem Algebra.IsIntegral.isField_iff_isField {R S : Type*} [CommRing R] [Nontrivial R] [CommRing S] [IsDomain S] [Algebra R S] (H : Algebra.IsIntegral R S) (hRS : Function.Injective (algebraMap R S)) : IsField R ↔ IsField S := ⟨isField_of_isIntegral_of_isField' H, isField_of_isIntegral_of_isField H hRS⟩ -#align algebra.is_integral.is_field_iff_is_field Algebra.IsIntegral.isField_iff_isField end Algebra @@ -1187,7 +1074,6 @@ theorem integralClosure_idem {R : Type*} {A : Type*} [CommRing R] [CommRing A] [ @isIntegral_trans _ _ _ _ _ _ _ _ (integralClosure R A).algebra _ integralClosure.isIntegral x hx⟩, rfl⟩ -#align integral_closure_idem integralClosure_idem section IsDomain @@ -1199,6 +1085,5 @@ instance : IsDomain (integralClosure R S) := theorem roots_mem_integralClosure {f : R[X]} (hf : f.Monic) {a : S} (ha : a ∈ f.aroots S) : a ∈ integralClosure R S := ⟨f, hf, (eval₂_eq_eval_map _).trans <| (mem_roots <| (hf.map _).ne_zero).1 ha⟩ -#align roots_mem_integral_closure roots_mem_integralClosure end IsDomain diff --git a/Mathlib/Topology/Connected/Basic.lean b/Mathlib/Topology/Connected/Basic.lean index a90006f21a6ad..b8ae0cd7c1689 100644 --- a/Mathlib/Topology/Connected/Basic.lean +++ b/Mathlib/Topology/Connected/Basic.lean @@ -51,44 +51,34 @@ section Preconnected def IsPreconnected (s : Set α) : Prop := ∀ u v : Set α, IsOpen u → IsOpen v → s ⊆ u ∪ v → (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty -#align is_preconnected IsPreconnected /-- A connected set is one that is nonempty and where there is no non-trivial open partition. -/ def IsConnected (s : Set α) : Prop := s.Nonempty ∧ IsPreconnected s -#align is_connected IsConnected theorem IsConnected.nonempty {s : Set α} (h : IsConnected s) : s.Nonempty := h.1 -#align is_connected.nonempty IsConnected.nonempty theorem IsConnected.isPreconnected {s : Set α} (h : IsConnected s) : IsPreconnected s := h.2 -#align is_connected.is_preconnected IsConnected.isPreconnected theorem IsPreirreducible.isPreconnected {s : Set α} (H : IsPreirreducible s) : IsPreconnected s := fun _ _ hu hv _ => H _ _ hu hv -#align is_preirreducible.is_preconnected IsPreirreducible.isPreconnected theorem IsIrreducible.isConnected {s : Set α} (H : IsIrreducible s) : IsConnected s := ⟨H.nonempty, H.isPreirreducible.isPreconnected⟩ -#align is_irreducible.is_connected IsIrreducible.isConnected theorem isPreconnected_empty : IsPreconnected (∅ : Set α) := isPreirreducible_empty.isPreconnected -#align is_preconnected_empty isPreconnected_empty theorem isConnected_singleton {x} : IsConnected ({x} : Set α) := isIrreducible_singleton.isConnected -#align is_connected_singleton isConnected_singleton theorem isPreconnected_singleton {x} : IsPreconnected ({x} : Set α) := isConnected_singleton.isPreconnected -#align is_preconnected_singleton isPreconnected_singleton theorem Set.Subsingleton.isPreconnected {s : Set α} (hs : s.Subsingleton) : IsPreconnected s := hs.induction_on isPreconnected_empty fun _ => isPreconnected_singleton -#align set.subsingleton.is_preconnected Set.Subsingleton.isPreconnected /-- If any point of a set is joined to a fixed point by a preconnected subset, then the original set is preconnected as well. -/ @@ -108,7 +98,6 @@ theorem isPreconnected_of_forall {s : Set α} (x : α) rcases H z zs with ⟨t, ts, xt, zt, ht⟩ have := ht v u hv hu (ts.trans <| by rwa [union_comm]) ⟨x, xt, xv⟩ ⟨z, zt, zu⟩ exact this.imp fun _ h => ⟨ts h.1, h.2.2, h.2.1⟩ -#align is_preconnected_of_forall isPreconnected_of_forall /-- If any two points of a set are contained in a preconnected subset, then the original set is preconnected as well. -/ @@ -117,7 +106,6 @@ theorem isPreconnected_of_forall_pair {s : Set α} IsPreconnected s := by rcases eq_empty_or_nonempty s with (rfl | ⟨x, hx⟩) exacts [isPreconnected_empty, isPreconnected_of_forall x fun y => H x hx y] -#align is_preconnected_of_forall_pair isPreconnected_of_forall_pair /-- A union of a family of preconnected sets with a common point is preconnected as well. -/ theorem isPreconnected_sUnion (x : α) (c : Set (Set α)) (H1 : ∀ s ∈ c, x ∈ s) @@ -125,24 +113,20 @@ theorem isPreconnected_sUnion (x : α) (c : Set (Set α)) (H1 : ∀ s ∈ c, x apply isPreconnected_of_forall x rintro y ⟨s, sc, ys⟩ exact ⟨s, subset_sUnion_of_mem sc, H1 s sc, ys, H2 s sc⟩ -#align is_preconnected_sUnion isPreconnected_sUnion theorem isPreconnected_iUnion {ι : Sort*} {s : ι → Set α} (h₁ : (⋂ i, s i).Nonempty) (h₂ : ∀ i, IsPreconnected (s i)) : IsPreconnected (⋃ i, s i) := Exists.elim h₁ fun f hf => isPreconnected_sUnion f _ hf (forall_range_iff.2 h₂) -#align is_preconnected_Union isPreconnected_iUnion theorem IsPreconnected.union (x : α) {s t : Set α} (H1 : x ∈ s) (H2 : x ∈ t) (H3 : IsPreconnected s) (H4 : IsPreconnected t) : IsPreconnected (s ∪ t) := sUnion_pair s t ▸ isPreconnected_sUnion x {s, t} (by rintro r (rfl | rfl | h) <;> assumption) (by rintro r (rfl | rfl | h) <;> assumption) -#align is_preconnected.union IsPreconnected.union theorem IsPreconnected.union' {s t : Set α} (H : (s ∩ t).Nonempty) (hs : IsPreconnected s) (ht : IsPreconnected t) : IsPreconnected (s ∪ t) := by rcases H with ⟨x, hxs, hxt⟩ exact hs.union x hxs hxt ht -#align is_preconnected.union' IsPreconnected.union' theorem IsConnected.union {s t : Set α} (H : (s ∩ t).Nonempty) (Hs : IsConnected s) (Ht : IsConnected t) : IsConnected (s ∪ t) := by @@ -150,7 +134,6 @@ theorem IsConnected.union {s t : Set α} (H : (s ∩ t).Nonempty) (Hs : IsConnec refine' ⟨⟨x, mem_union_left t (mem_of_mem_inter_left hx)⟩, _⟩ exact Hs.isPreconnected.union x (mem_of_mem_inter_left hx) (mem_of_mem_inter_right hx) Ht.isPreconnected -#align is_connected.union IsConnected.union /-- The directed sUnion of a set S of preconnected subsets is preconnected. -/ theorem IsPreconnected.sUnion_directed {S : Set (Set α)} (K : DirectedOn (· ⊆ ·) S) @@ -161,7 +144,6 @@ theorem IsPreconnected.sUnion_directed {S : Set (Set α)} (K : DirectedOn (· H _ hrS u v hu hv ((subset_sUnion_of_mem hrS).trans Huv) ⟨a, hsr has, hau⟩ ⟨b, htr hbt, hbv⟩ have Kruv : r ∩ (u ∩ v) ⊆ ⋃₀ S ∩ (u ∩ v) := inter_subset_inter_left _ (subset_sUnion_of_mem hrS) exact Hnuv.mono Kruv -#align is_preconnected.sUnion_directed IsPreconnected.sUnion_directed /-- The biUnion of a family of preconnected sets is preconnected if the graph determined by whether two sets intersect is preconnected. -/ @@ -192,7 +174,6 @@ theorem IsPreconnected.biUnion_of_reflTransGen {ι : Type*} {t : Set ι} {s : ι obtain ⟨p, hpt, hip, hjp, hp⟩ := P i hi j hj (K i hi j hj) exact ⟨⋃ j ∈ p, s j, biUnion_subset_biUnion_left hpt, mem_biUnion hip hxi, mem_biUnion hjp hyj, hp⟩ -#align is_preconnected.bUnion_of_refl_trans_gen IsPreconnected.biUnion_of_reflTransGen /-- The biUnion of a family of preconnected sets is preconnected if the graph determined by whether two sets intersect is preconnected. -/ @@ -202,7 +183,6 @@ theorem IsConnected.biUnion_of_reflTransGen {ι : Type*} {t : Set ι} {s : ι IsConnected (⋃ n ∈ t, s n) := ⟨nonempty_biUnion.2 <| ⟨ht.some, ht.some_mem, (H _ ht.some_mem).nonempty⟩, IsPreconnected.biUnion_of_reflTransGen (fun i hi => (H i hi).isPreconnected) K⟩ -#align is_connected.bUnion_of_refl_trans_gen IsConnected.biUnion_of_reflTransGen /-- Preconnectedness of the iUnion of a family of preconnected sets indexed by the vertices of a preconnected graph, @@ -214,14 +194,12 @@ theorem IsPreconnected.iUnion_of_reflTransGen {ι : Type*} {s : ι → Set α} rw [← biUnion_univ] exact IsPreconnected.biUnion_of_reflTransGen (fun i _ => H i) fun i _ j _ => by simpa [mem_univ] using K i j -#align is_preconnected.Union_of_refl_trans_gen IsPreconnected.iUnion_of_reflTransGen theorem IsConnected.iUnion_of_reflTransGen {ι : Type*} [Nonempty ι] {s : ι → Set α} (H : ∀ i, IsConnected (s i)) (K : ∀ i j, ReflTransGen (fun i j : ι => (s i ∩ s j).Nonempty) i j) : IsConnected (⋃ n, s n) := ⟨nonempty_iUnion.2 <| Nonempty.elim ‹_› fun i : ι => ⟨i, (H _).nonempty⟩, IsPreconnected.iUnion_of_reflTransGen (fun i => (H i).isPreconnected) K⟩ -#align is_connected.Union_of_refl_trans_gen IsConnected.iUnion_of_reflTransGen section SuccOrder @@ -237,7 +215,6 @@ theorem IsPreconnected.iUnion_of_chain {s : β → Set α} (H : ∀ n, IsPreconn reflTransGen_of_succ _ (fun i _ => K i) fun i _ => by rw [inter_comm] exact K i -#align is_preconnected.Union_of_chain IsPreconnected.iUnion_of_chain /-- The iUnion of connected sets indexed by a type with an archimedean successor (like `ℕ` or `ℤ`) such that any two neighboring sets meet is connected. -/ @@ -247,7 +224,6 @@ theorem IsConnected.iUnion_of_chain [Nonempty β] {s : β → Set α} (H : ∀ n reflTransGen_of_succ _ (fun i _ => K i) fun i _ => by rw [inter_comm] exact K i -#align is_connected.Union_of_chain IsConnected.iUnion_of_chain /-- The iUnion of preconnected sets indexed by a subset of a type with an archimedean successor (like `ℕ` or `ℤ`) such that any two neighboring sets meet is preconnected. -/ @@ -264,7 +240,6 @@ theorem IsPreconnected.biUnion_of_chain {s : β → Set α} {t : Set β} (ht : O refine' IsPreconnected.biUnion_of_reflTransGen H fun i hi j hj => _ exact reflTransGen_of_succ _ (fun k hk => ⟨h3 hi hj hk, h1 hi hj hk⟩) fun k hk => ⟨by rw [inter_comm]; exact h3 hj hi hk, h2 hj hi hk⟩ -#align is_preconnected.bUnion_of_chain IsPreconnected.biUnion_of_chain /-- The iUnion of connected sets indexed by a subset of a type with an archimedean successor (like `ℕ` or `ℤ`) such that any two neighboring sets meet is preconnected. -/ @@ -273,7 +248,6 @@ theorem IsConnected.biUnion_of_chain {s : β → Set α} {t : Set β} (hnt : t.N (K : ∀ n : β, n ∈ t → succ n ∈ t → (s n ∩ s (succ n)).Nonempty) : IsConnected (⋃ n ∈ t, s n) := ⟨nonempty_biUnion.2 <| ⟨hnt.some, hnt.some_mem, (H _ hnt.some_mem).nonempty⟩, IsPreconnected.biUnion_of_chain ht (fun i hi => (H i hi).isPreconnected) K⟩ -#align is_connected.bUnion_of_chain IsConnected.biUnion_of_chain end SuccOrder @@ -286,25 +260,21 @@ protected theorem IsPreconnected.subset_closure {s : Set α} {t : Set α} (H : I let ⟨q, hqv, hqs⟩ := mem_closure_iff.1 (Ktcs hzt) v hv hzv let ⟨r, hrs, hruv⟩ := H u v hu hv (Subset.trans Kst htuv) ⟨p, hps, hpu⟩ ⟨q, hqs, hqv⟩ ⟨r, Kst hrs, hruv⟩ -#align is_preconnected.subset_closure IsPreconnected.subset_closure /-- Theorem of bark and tree: if a set is within a connected set and its closure, then it is connected as well. See also `IsPreconnected.subset_closure`. -/ protected theorem IsConnected.subset_closure {s : Set α} {t : Set α} (H : IsConnected s) (Kst : s ⊆ t) (Ktcs : t ⊆ closure s) : IsConnected t := ⟨Nonempty.mono Kst H.left, IsPreconnected.subset_closure H.right Kst Ktcs⟩ -#align is_connected.subset_closure IsConnected.subset_closure /-- The closure of a preconnected set is preconnected as well. -/ protected theorem IsPreconnected.closure {s : Set α} (H : IsPreconnected s) : IsPreconnected (closure s) := IsPreconnected.subset_closure H subset_closure Subset.rfl -#align is_preconnected.closure IsPreconnected.closure /-- The closure of a connected set is connected as well. -/ protected theorem IsConnected.closure {s : Set α} (H : IsConnected s) : IsConnected (closure s) := IsConnected.subset_closure H subset_closure <| Subset.rfl -#align is_connected.closure IsConnected.closure /-- The image of a preconnected set is preconnected as well. -/ protected theorem IsPreconnected.image [TopologicalSpace β] {s : Set α} (H : IsPreconnected s) @@ -326,13 +296,11 @@ protected theorem IsPreconnected.image [TopologicalSpace β] {s : Set α} (H : I rw [← inter_self s, inter_assoc, inter_left_comm s u', ← inter_assoc, inter_comm s, inter_comm s, ← u'_eq, ← v'_eq] at hz exact ⟨f z, ⟨z, hz.1.2, rfl⟩, hz.1.1, hz.2.1⟩ -#align is_preconnected.image IsPreconnected.image /-- The image of a connected set is connected as well. -/ protected theorem IsConnected.image [TopologicalSpace β] {s : Set α} (H : IsConnected s) (f : α → β) (hf : ContinuousOn f s) : IsConnected (f '' s) := ⟨nonempty_image_iff.mpr H.nonempty, H.isPreconnected.image f hf⟩ -#align is_connected.image IsConnected.image theorem isPreconnected_closed_iff {s : Set α} : IsPreconnected s ↔ ∀ t t', IsClosed t → IsClosed t' → @@ -355,7 +323,6 @@ theorem isPreconnected_closed_iff {s : Set α} : have := h _ _ hu.isClosed_compl hv.isClosed_compl h' ⟨y, ys, yu⟩ ⟨x, xs, xv⟩ rw [← compl_union] at this exact this.ne_empty huv.disjoint_compl_right.inter_eq⟩ -#align is_preconnected_closed_iff isPreconnected_closed_iff theorem Inducing.isPreconnected_image [TopologicalSpace β] {s : Set α} {f : α → β} (hf : Inducing f) : IsPreconnected (f '' s) ↔ IsPreconnected s := by @@ -367,7 +334,6 @@ theorem Inducing.isPreconnected_image [TopologicalSpace β] {s : Set α} {f : α rcases h u v hu hv huv ⟨f x, mem_image_of_mem _ hxs, hxu⟩ ⟨f y, mem_image_of_mem _ hys, hyv⟩ with ⟨_, ⟨z, hzs, rfl⟩, hzuv⟩ exact ⟨z, hzs, hzuv⟩ -#align inducing.is_preconnected_image Inducing.isPreconnected_image /- TODO: The following lemmas about connection of preimages hold more generally for strict maps (the quotient and subspace topologies of the image agree) whose fibers are preconnected. -/ @@ -381,7 +347,6 @@ theorem IsPreconnected.preimage_of_open_map [TopologicalSpace β] {s : Set β} ( · simpa only [image_preimage_inter] using hsu.image f · simpa only [image_preimage_inter] using hsv.image f · exact ⟨a, has, hau, hinj.mem_set_image.1 hav⟩ -#align is_preconnected.preimage_of_open_map IsPreconnected.preimage_of_open_map theorem IsPreconnected.preimage_of_closed_map [TopologicalSpace β] {s : Set β} (hs : IsPreconnected s) {f : α → β} (hinj : Function.Injective f) (hf : IsClosedMap f) @@ -394,19 +359,16 @@ theorem IsPreconnected.preimage_of_closed_map [TopologicalSpace β] {s : Set β} · simpa only [image_preimage_inter] using hsu.image f · simpa only [image_preimage_inter] using hsv.image f · exact ⟨a, has, hau, hinj.mem_set_image.1 hav⟩ -#align is_preconnected.preimage_of_closed_map IsPreconnected.preimage_of_closed_map theorem IsConnected.preimage_of_openMap [TopologicalSpace β] {s : Set β} (hs : IsConnected s) {f : α → β} (hinj : Function.Injective f) (hf : IsOpenMap f) (hsf : s ⊆ range f) : IsConnected (f ⁻¹' s) := ⟨hs.nonempty.preimage' hsf, hs.isPreconnected.preimage_of_open_map hinj hf hsf⟩ -#align is_connected.preimage_of_open_map IsConnected.preimage_of_openMap theorem IsConnected.preimage_of_closedMap [TopologicalSpace β] {s : Set β} (hs : IsConnected s) {f : α → β} (hinj : Function.Injective f) (hf : IsClosedMap f) (hsf : s ⊆ range f) : IsConnected (f ⁻¹' s) := ⟨hs.nonempty.preimage' hsf, hs.isPreconnected.preimage_of_closed_map hinj hf hsf⟩ -#align is_connected.preimage_of_closed_map IsConnected.preimage_of_closedMap theorem IsPreconnected.subset_or_subset (hu : IsOpen u) (hv : IsOpen v) (huv : Disjoint u v) (hsuv : s ⊆ u ∪ v) (hs : IsPreconnected s) : s ⊆ u ∨ s ⊆ v := by @@ -417,7 +379,6 @@ theorem IsPreconnected.subset_or_subset (hu : IsOpen u) (hv : IsOpen v) (huv : D simp_rw [Set.not_nonempty_iff_eq_empty, ← Set.disjoint_iff_inter_eq_empty, disjoint_iff_inter_eq_empty.1 huv] at hs exact Or.inl ((hs s.disjoint_empty).subset_left_of_subset_union hsuv) -#align is_preconnected.subset_or_subset IsPreconnected.subset_or_subset theorem IsPreconnected.subset_left_of_subset_union (hu : IsOpen u) (hv : IsOpen v) (huv : Disjoint u v) (hsuv : s ⊆ u ∪ v) (hsu : (s ∩ u).Nonempty) (hs : IsPreconnected s) : @@ -428,20 +389,17 @@ theorem IsPreconnected.subset_left_of_subset_union (hu : IsOpen u) (hv : IsOpen rw [not_disjoint_iff_nonempty_inter] at hsv obtain ⟨x, _, hx⟩ := hs u v hu hv hsuv hsu hsv exact Set.disjoint_iff.1 huv hx) -#align is_preconnected.subset_left_of_subset_union IsPreconnected.subset_left_of_subset_union theorem IsPreconnected.subset_right_of_subset_union (hu : IsOpen u) (hv : IsOpen v) (huv : Disjoint u v) (hsuv : s ⊆ u ∪ v) (hsv : (s ∩ v).Nonempty) (hs : IsPreconnected s) : s ⊆ v := hs.subset_left_of_subset_union hv hu huv.symm (union_comm u v ▸ hsuv) hsv -#align is_preconnected.subset_right_of_subset_union IsPreconnected.subset_right_of_subset_union -- porting note: moved up /-- Preconnected sets are either contained in or disjoint to any given clopen set. -/ theorem IsPreconnected.subset_clopen {s t : Set α} (hs : IsPreconnected s) (ht : IsClopen t) (hne : (s ∩ t).Nonempty) : s ⊆ t := hs.subset_left_of_subset_union ht.isOpen ht.compl.isOpen disjoint_compl_right (by simp) hne -#align is_preconnected.subset_clopen IsPreconnected.subset_clopen /-- If a preconnected set `s` intersects an open set `u`, and limit points of `u` inside `s` are contained in `u`, then the whole set `s` is contained in `u`. -/ @@ -456,7 +414,6 @@ theorem IsPreconnected.subset_of_closure_inter_subset (hs : IsPreconnected s) (h exact xu (h (mem_inter h'x hx)) apply hs.subset_left_of_subset_union hu isClosed_closure.isOpen_compl _ A h'u exact disjoint_compl_right.mono_right (compl_subset_compl.2 subset_closure) -#align is_preconnected.subset_of_closure_inter_subset IsPreconnected.subset_of_closure_inter_subset theorem IsPreconnected.prod [TopologicalSpace β] {s : Set α} {t : Set β} (hs : IsPreconnected s) (ht : IsPreconnected t) : IsPreconnected (s ×ˢ t) := by @@ -467,12 +424,10 @@ theorem IsPreconnected.prod [TopologicalSpace β] {s : Set α} {t : Set β} (hs exacts [⟨ha₁, hy⟩, ⟨hx, hb₂⟩] · exact (ht.image _ (Continuous.Prod.mk _).continuousOn).union (a₁, b₂) ⟨b₂, hb₂, rfl⟩ ⟨a₁, ha₁, rfl⟩ (hs.image _ (continuous_id.prod_mk continuous_const).continuousOn) -#align is_preconnected.prod IsPreconnected.prod theorem IsConnected.prod [TopologicalSpace β] {s : Set α} {t : Set β} (hs : IsConnected s) (ht : IsConnected t) : IsConnected (s ×ˢ t) := ⟨hs.1.prod ht.1, hs.2.prod ht.2⟩ -#align is_connected.prod IsConnected.prod theorem isPreconnected_univ_pi [∀ i, TopologicalSpace (π i)] {s : ∀ i, Set (π i)} (hs : ∀ i, IsPreconnected (s i)) : IsPreconnected (pi univ s) := by @@ -495,7 +450,6 @@ theorem isPreconnected_univ_pi [∀ i, TopologicalSpace (π i)] {s : ∀ i, Set have hSv : (S ∩ v).Nonempty := ⟨_, ⟨_, this _ trivial, update_eq_self _ _⟩, h⟩ refine' (hconn u v uo vo (hsub.trans hsuv) hSu hSv).mono _ exact inter_subset_inter_left _ hsub -#align is_preconnected_univ_pi isPreconnected_univ_pi @[simp] theorem isConnected_univ_pi [∀ i, TopologicalSpace (π i)] {s : ∀ i, Set (π i)} : @@ -504,7 +458,6 @@ theorem isConnected_univ_pi [∀ i, TopologicalSpace (π i)] {s : ∀ i, Set (π refine' fun hne => ⟨fun hc i => _, isPreconnected_univ_pi⟩ rw [← eval_image_univ_pi hne] exact hc.image _ (continuous_apply _).continuousOn -#align is_connected_univ_pi isConnected_univ_pi theorem Sigma.isConnected_iff [∀ i, TopologicalSpace (π i)] {s : Set (Σi, π i)} : IsConnected s ↔ ∃ i t, IsConnected t ∧ s = Sigma.mk i '' t := by @@ -516,7 +469,6 @@ theorem Sigma.isConnected_iff [∀ i, TopologicalSpace (π i)] {s : Set (Σi, π (Set.image_preimage_eq_of_subset this).symm⟩ · rintro ⟨i, t, ht, rfl⟩ exact ht.image _ continuous_sigmaMk.continuousOn -#align sigma.is_connected_iff Sigma.isConnected_iff theorem Sigma.isPreconnected_iff [hι : Nonempty ι] [∀ i, TopologicalSpace (π i)] {s : Set (Σi, π i)} : IsPreconnected s ↔ ∃ i t, IsPreconnected t ∧ s = Sigma.mk i '' t := by @@ -527,7 +479,6 @@ theorem Sigma.isPreconnected_iff [hι : Nonempty ι] [∀ i, TopologicalSpace ( refine' ⟨a, t, ht.isPreconnected, rfl⟩ · rintro ⟨a, t, ht, rfl⟩ exact ht.image _ continuous_sigmaMk.continuousOn -#align sigma.is_preconnected_iff Sigma.isPreconnected_iff theorem Sum.isConnected_iff [TopologicalSpace β] {s : Set (Sum α β)} : IsConnected s ↔ @@ -547,7 +498,6 @@ theorem Sum.isConnected_iff [TopologicalSpace β] {s : Set (Sum α β)} : · rintro (⟨t, ht, rfl⟩ | ⟨t, ht, rfl⟩) · exact ht.image _ continuous_inl.continuousOn · exact ht.image _ continuous_inr.continuousOn -#align sum.is_connected_iff Sum.isConnected_iff theorem Sum.isPreconnected_iff [TopologicalSpace β] {s : Set (Sum α β)} : IsPreconnected s ↔ @@ -561,13 +511,11 @@ theorem Sum.isPreconnected_iff [TopologicalSpace β] {s : Set (Sum α β)} : · rintro (⟨t, ht, rfl⟩ | ⟨t, ht, rfl⟩) · exact ht.image _ continuous_inl.continuousOn · exact ht.image _ continuous_inr.continuousOn -#align sum.is_preconnected_iff Sum.isPreconnected_iff /-- The connected component of a point is the maximal connected set that contains this point. -/ def connectedComponent (x : α) : Set α := ⋃₀ { s : Set α | IsPreconnected s ∧ x ∈ s } -#align connected_component connectedComponent /-- Given a set `F` in a topological space `α` and a point `x : α`, the connected component of `x` in `F` is the connected component of `x` in the subtype `F` seen as @@ -575,65 +523,52 @@ a set in `α`. This definition does not make sense if `x` is not in `F` so we re empty set in this case. -/ def connectedComponentIn (F : Set α) (x : α) : Set α := if h : x ∈ F then (↑) '' connectedComponent (⟨x, h⟩ : F) else ∅ -#align connected_component_in connectedComponentIn theorem connectedComponentIn_eq_image {F : Set α} {x : α} (h : x ∈ F) : connectedComponentIn F x = (↑) '' connectedComponent (⟨x, h⟩ : F) := dif_pos h -#align connected_component_in_eq_image connectedComponentIn_eq_image theorem connectedComponentIn_eq_empty {F : Set α} {x : α} (h : x ∉ F) : connectedComponentIn F x = ∅ := dif_neg h -#align connected_component_in_eq_empty connectedComponentIn_eq_empty theorem mem_connectedComponent {x : α} : x ∈ connectedComponent x := mem_sUnion_of_mem (mem_singleton x) ⟨isPreconnected_singleton, mem_singleton x⟩ -#align mem_connected_component mem_connectedComponent theorem mem_connectedComponentIn {x : α} {F : Set α} (hx : x ∈ F) : x ∈ connectedComponentIn F x := by simp [connectedComponentIn_eq_image hx, mem_connectedComponent, hx] -#align mem_connected_component_in mem_connectedComponentIn theorem connectedComponent_nonempty {x : α} : (connectedComponent x).Nonempty := ⟨x, mem_connectedComponent⟩ -#align connected_component_nonempty connectedComponent_nonempty theorem connectedComponentIn_nonempty_iff {x : α} {F : Set α} : (connectedComponentIn F x).Nonempty ↔ x ∈ F := by rw [connectedComponentIn] split_ifs <;> simp [connectedComponent_nonempty, *] -#align connected_component_in_nonempty_iff connectedComponentIn_nonempty_iff theorem connectedComponentIn_subset (F : Set α) (x : α) : connectedComponentIn F x ⊆ F := by rw [connectedComponentIn] split_ifs <;> simp -#align connected_component_in_subset connectedComponentIn_subset theorem isPreconnected_connectedComponent {x : α} : IsPreconnected (connectedComponent x) := isPreconnected_sUnion x _ (fun _ => And.right) fun _ => And.left -#align is_preconnected_connected_component isPreconnected_connectedComponent theorem isPreconnected_connectedComponentIn {x : α} {F : Set α} : IsPreconnected (connectedComponentIn F x) := by rw [connectedComponentIn]; split_ifs · exact inducing_subtype_val.isPreconnected_image.mpr isPreconnected_connectedComponent · exact isPreconnected_empty -#align is_preconnected_connected_component_in isPreconnected_connectedComponentIn theorem isConnected_connectedComponent {x : α} : IsConnected (connectedComponent x) := ⟨⟨x, mem_connectedComponent⟩, isPreconnected_connectedComponent⟩ -#align is_connected_connected_component isConnected_connectedComponent theorem isConnected_connectedComponentIn_iff {x : α} {F : Set α} : IsConnected (connectedComponentIn F x) ↔ x ∈ F := by simp_rw [← connectedComponentIn_nonempty_iff, IsConnected, isPreconnected_connectedComponentIn, and_true_iff] -#align is_connected_connected_component_in_iff isConnected_connectedComponentIn_iff theorem IsPreconnected.subset_connectedComponent {x : α} {s : Set α} (H1 : IsPreconnected s) (H2 : x ∈ s) : s ⊆ connectedComponent x := fun _z hz => mem_sUnion_of_mem hz ⟨H1, H2⟩ -#align is_preconnected.subset_connected_component IsPreconnected.subset_connectedComponent theorem IsPreconnected.subset_connectedComponentIn {x : α} {F : Set α} (hs : IsPreconnected s) (hxs : x ∈ s) (hsF : s ⊆ F) : s ⊆ connectedComponentIn F x := by @@ -647,17 +582,14 @@ theorem IsPreconnected.subset_connectedComponentIn {x : α} {F : Set α} (hs : I rw [connectedComponentIn_eq_image (hsF hxs)] refine' Subset.trans _ (image_subset _ this) rw [Subtype.image_preimage_coe, inter_eq_left.mpr hsF] -#align is_preconnected.subset_connected_component_in IsPreconnected.subset_connectedComponentIn theorem IsConnected.subset_connectedComponent {x : α} {s : Set α} (H1 : IsConnected s) (H2 : x ∈ s) : s ⊆ connectedComponent x := H1.2.subset_connectedComponent H2 -#align is_connected.subset_connected_component IsConnected.subset_connectedComponent theorem IsPreconnected.connectedComponentIn {x : α} {F : Set α} (h : IsPreconnected F) (hx : x ∈ F) : connectedComponentIn F x = F := (connectedComponentIn_subset F x).antisymm (h.subset_connectedComponentIn hx subset_rfl) -#align is_preconnected.connected_component_in IsPreconnected.connectedComponentIn theorem connectedComponent_eq {x y : α} (h : y ∈ connectedComponent x) : connectedComponent x = connectedComponent y := @@ -665,12 +597,10 @@ theorem connectedComponent_eq {x y : α} (h : y ∈ connectedComponent x) : (isConnected_connectedComponent.subset_connectedComponent (Set.mem_of_mem_of_subset mem_connectedComponent (isConnected_connectedComponent.subset_connectedComponent h))) -#align connected_component_eq connectedComponent_eq theorem connectedComponent_eq_iff_mem {x y : α} : connectedComponent x = connectedComponent y ↔ x ∈ connectedComponent y := ⟨fun h => h ▸ mem_connectedComponent, fun h => (connectedComponent_eq h).symm⟩ -#align connected_component_eq_iff_mem connectedComponent_eq_iff_mem theorem connectedComponentIn_eq {x y : α} {F : Set α} (h : y ∈ connectedComponentIn F x) : connectedComponentIn F x = connectedComponentIn F y := by @@ -678,7 +608,6 @@ theorem connectedComponentIn_eq {x y : α} {F : Set α} (h : y ∈ connectedComp simp_rw [connectedComponentIn_eq_image hx] at h ⊢ obtain ⟨⟨y, hy⟩, h2y, rfl⟩ := h simp_rw [connectedComponentIn_eq_image hy, connectedComponent_eq h2y] -#align connected_component_in_eq connectedComponentIn_eq theorem connectedComponentIn_univ (x : α) : connectedComponentIn univ x = connectedComponent x := subset_antisymm @@ -686,35 +615,29 @@ theorem connectedComponentIn_univ (x : α) : connectedComponentIn univ x = conne mem_connectedComponentIn trivial) (isPreconnected_connectedComponent.subset_connectedComponentIn mem_connectedComponent <| subset_univ _) -#align connected_component_in_univ connectedComponentIn_univ theorem connectedComponent_disjoint {x y : α} (h : connectedComponent x ≠ connectedComponent y) : Disjoint (connectedComponent x) (connectedComponent y) := Set.disjoint_left.2 fun _ h1 h2 => h ((connectedComponent_eq h1).trans (connectedComponent_eq h2).symm) -#align connected_component_disjoint connectedComponent_disjoint theorem isClosed_connectedComponent {x : α} : IsClosed (connectedComponent x) := closure_subset_iff_isClosed.1 <| isConnected_connectedComponent.closure.subset_connectedComponent <| subset_closure mem_connectedComponent -#align is_closed_connected_component isClosed_connectedComponent theorem Continuous.image_connectedComponent_subset [TopologicalSpace β] {f : α → β} (h : Continuous f) (a : α) : f '' connectedComponent a ⊆ connectedComponent (f a) := (isConnected_connectedComponent.image f h.continuousOn).subset_connectedComponent ((mem_image f (connectedComponent a) (f a)).2 ⟨a, mem_connectedComponent, rfl⟩) -#align continuous.image_connected_component_subset Continuous.image_connectedComponent_subset theorem Continuous.mapsTo_connectedComponent [TopologicalSpace β] {f : α → β} (h : Continuous f) (a : α) : MapsTo f (connectedComponent a) (connectedComponent (f a)) := mapsTo'.2 <| h.image_connectedComponent_subset a -#align continuous.maps_to_connected_component Continuous.mapsTo_connectedComponent theorem irreducibleComponent_subset_connectedComponent {x : α} : irreducibleComponent x ⊆ connectedComponent x := isIrreducible_irreducibleComponent.isConnected.subset_connectedComponent mem_irreducibleComponent -#align irreducible_component_subset_connected_component irreducibleComponent_subset_connectedComponent @[mono] theorem connectedComponentIn_mono (x : α) {F G : Set α} (h : F ⊆ G) : @@ -725,13 +648,11 @@ theorem connectedComponentIn_mono (x : α) {F G : Set α} (h : F ⊆ G) : exact image_subset _ ((continuous_inclusion h).image_connectedComponent_subset ⟨x, hx⟩) · rw [connectedComponentIn_eq_empty hx] exact Set.empty_subset _ -#align connected_component_in_mono connectedComponentIn_mono /-- A preconnected space is one where there is no non-trivial open partition. -/ class PreconnectedSpace (α : Type u) [TopologicalSpace α] : Prop where /-- The universal set `Set.univ` in a preconnected space is a preconnected set. -/ isPreconnected_univ : IsPreconnected (univ : Set α) -#align preconnected_space PreconnectedSpace export PreconnectedSpace (isPreconnected_univ) @@ -739,14 +660,12 @@ export PreconnectedSpace (isPreconnected_univ) class ConnectedSpace (α : Type u) [TopologicalSpace α] extends PreconnectedSpace α : Prop where /-- A connected space is nonempty. -/ toNonempty : Nonempty α -#align connected_space ConnectedSpace attribute [instance 50] ConnectedSpace.toNonempty -- see Note [lower instance priority] -- see Note [lower instance priority] theorem isConnected_univ [ConnectedSpace α] : IsConnected (univ : Set α) := ⟨univ_nonempty, isPreconnected_univ⟩ -#align is_connected_univ isConnected_univ lemma preconnectedSpace_iff_univ : PreconnectedSpace α ↔ IsPreconnected (univ : Set α) := ⟨fun h ↦ h.1, fun h ↦ ⟨h⟩⟩ @@ -758,12 +677,10 @@ lemma connectedSpace_iff_univ : ConnectedSpace α ↔ IsConnected (univ : Set α theorem isPreconnected_range [TopologicalSpace β] [PreconnectedSpace α] {f : α → β} (h : Continuous f) : IsPreconnected (range f) := @image_univ _ _ f ▸ isPreconnected_univ.image _ h.continuousOn -#align is_preconnected_range isPreconnected_range theorem isConnected_range [TopologicalSpace β] [ConnectedSpace α] {f : α → β} (h : Continuous f) : IsConnected (range f) := ⟨range_nonempty f, isPreconnected_range h⟩ -#align is_connected_range isConnected_range theorem Function.Surjective.connectedSpace [ConnectedSpace α] [TopologicalSpace β] {f : α → β} (hf : Surjective f) (hf' : Continuous f) : ConnectedSpace β := by @@ -777,7 +694,6 @@ instance Quotient.instConnectedSpace {s : Setoid α} [ConnectedSpace α] : theorem DenseRange.preconnectedSpace [TopologicalSpace β] [PreconnectedSpace α] {f : α → β} (hf : DenseRange f) (hc : Continuous f) : PreconnectedSpace β := ⟨hf.closure_eq ▸ (isPreconnected_range hc).closure⟩ -#align dense_range.preconnected_space DenseRange.preconnectedSpace theorem connectedSpace_iff_connectedComponent : ConnectedSpace α ↔ ∃ x : α, connectedComponent x = univ := by @@ -789,7 +705,6 @@ theorem connectedSpace_iff_connectedComponent : haveI : PreconnectedSpace α := ⟨by rw [← h]; exact isPreconnected_connectedComponent⟩ exact ⟨⟨x⟩⟩ -#align connected_space_iff_connected_component connectedSpace_iff_connectedComponent theorem preconnectedSpace_iff_connectedComponent : PreconnectedSpace α ↔ ∀ x : α, connectedComponent x = univ := by @@ -800,13 +715,11 @@ theorem preconnectedSpace_iff_connectedComponent : cases' isEmpty_or_nonempty α with hα hα · exact ⟨by rw [univ_eq_empty_iff.mpr hα]; exact isPreconnected_empty⟩ · exact ⟨by rw [← h (Classical.choice hα)]; exact isPreconnected_connectedComponent⟩ -#align preconnected_space_iff_connected_component preconnectedSpace_iff_connectedComponent @[simp] theorem PreconnectedSpace.connectedComponent_eq_univ {X : Type*} [TopologicalSpace X] [h : PreconnectedSpace X] (x : X) : connectedComponent x = univ := preconnectedSpace_iff_connectedComponent.mp h x -#align preconnected_space.connected_component_eq_univ PreconnectedSpace.connectedComponent_eq_univ instance [TopologicalSpace β] [PreconnectedSpace α] [PreconnectedSpace β] : PreconnectedSpace (α × β) := @@ -828,12 +741,10 @@ instance [∀ i, TopologicalSpace (π i)] [∀ i, ConnectedSpace (π i)] : Conne instance (priority := 100) PreirreducibleSpace.preconnectedSpace (α : Type u) [TopologicalSpace α] [PreirreducibleSpace α] : PreconnectedSpace α := ⟨isPreirreducible_univ.isPreconnected⟩ -#align preirreducible_space.preconnected_space PreirreducibleSpace.preconnectedSpace -- see Note [lower instance priority] instance (priority := 100) IrreducibleSpace.connectedSpace (α : Type u) [TopologicalSpace α] [IrreducibleSpace α] : ConnectedSpace α where toNonempty := IrreducibleSpace.toNonempty -#align irreducible_space.connected_space IrreducibleSpace.connectedSpace /-- A continuous map from a connected space to a disjoint union `Σ i, π i` can be lifted to one of the components `π i`. See also `ContinuousMap.exists_lift_sigma` for a version with bundled @@ -851,7 +762,6 @@ theorem Continuous.exists_lift_sigma [ConnectedSpace α] [∀ i, TopologicalSpac theorem nonempty_inter [PreconnectedSpace α] {s t : Set α} : IsOpen s → IsOpen t → s ∪ t = univ → s.Nonempty → t.Nonempty → (s ∩ t).Nonempty := by simpa only [univ_inter, univ_subset_iff] using @PreconnectedSpace.isPreconnected_univ α _ _ s t -#align nonempty_inter nonempty_inter theorem isClopen_iff [PreconnectedSpace α] {s : Set α} : IsClopen s ↔ s = ∅ ∨ s = univ := ⟨fun hs => @@ -864,12 +774,10 @@ theorem isClopen_iff [PreconnectedSpace α] {s : Set α} : IsClopen s ↔ s = (nonempty_iff_ne_empty.2 h1.2) h3 h2, by rintro (rfl | rfl) <;> [exact isClopen_empty; exact isClopen_univ]⟩ -#align is_clopen_iff isClopen_iff theorem IsClopen.eq_univ [PreconnectedSpace α] {s : Set α} (h' : IsClopen s) (h : s.Nonempty) : s = univ := (isClopen_iff.mp h').resolve_left h.ne_empty -#align is_clopen.eq_univ IsClopen.eq_univ section disjoint_subsets @@ -921,32 +829,26 @@ end disjoint_subsets theorem frontier_eq_empty_iff [PreconnectedSpace α] {s : Set α} : frontier s = ∅ ↔ s = ∅ ∨ s = univ := isClopen_iff_frontier_eq_empty.symm.trans isClopen_iff -#align frontier_eq_empty_iff frontier_eq_empty_iff theorem nonempty_frontier_iff [PreconnectedSpace α] {s : Set α} : (frontier s).Nonempty ↔ s.Nonempty ∧ s ≠ univ := by simp only [nonempty_iff_ne_empty, Ne.def, frontier_eq_empty_iff, not_or] -#align nonempty_frontier_iff nonempty_frontier_iff theorem Subtype.preconnectedSpace {s : Set α} (h : IsPreconnected s) : PreconnectedSpace s where isPreconnected_univ := by rwa [← inducing_subtype_val.isPreconnected_image, image_univ, Subtype.range_val] -#align subtype.preconnected_space Subtype.preconnectedSpace theorem Subtype.connectedSpace {s : Set α} (h : IsConnected s) : ConnectedSpace s where toPreconnectedSpace := Subtype.preconnectedSpace h.isPreconnected toNonempty := h.nonempty.to_subtype -#align subtype.connected_space Subtype.connectedSpace theorem isPreconnected_iff_preconnectedSpace {s : Set α} : IsPreconnected s ↔ PreconnectedSpace s := ⟨Subtype.preconnectedSpace, fun h => by simpa using isPreconnected_univ.image ((↑) : s → α) continuous_subtype_val.continuousOn⟩ -#align is_preconnected_iff_preconnected_space isPreconnected_iff_preconnectedSpace theorem isConnected_iff_connectedSpace {s : Set α} : IsConnected s ↔ ConnectedSpace s := ⟨Subtype.connectedSpace, fun h => ⟨nonempty_subtype.mp h.2, isPreconnected_iff_preconnectedSpace.mpr h.1⟩⟩ -#align is_connected_iff_connected_space isConnected_iff_connectedSpace /-- In a preconnected space, given a transitive relation `P`, if `P x y` and `P y x` are true for `y` close enough to `x`, then `P x y` holds for all `x, y`. This is a version of the fact @@ -1032,7 +934,6 @@ theorem isPreconnected_iff_subset_of_disjoint {s : Set α} : exact ⟨x, hxs, ⟨h hxs, hxv⟩⟩ · rcases hsu with ⟨x, hxs, hxu⟩ exact ⟨x, hxs, ⟨hxu, h hxs⟩⟩ -#align is_preconnected_iff_subset_of_disjoint isPreconnected_iff_subset_of_disjoint /-- A set `s` is connected if and only if for every cover by a finite collection of open sets that are pairwise disjoint on `s`, @@ -1056,7 +957,6 @@ theorem isConnected_iff_sUnion_disjoint_open {s : Set α} : · rw [← not_nonempty_iff_eq_empty] at hsuv have := hsuv; rw [inter_comm u] at this simpa [*, or_imp, forall_and] using h {u, v} -#align is_connected_iff_sUnion_disjoint_open isConnected_iff_sUnion_disjoint_open -- porting note: `IsPreconnected.subset_clopen` moved up from here @@ -1064,7 +964,6 @@ theorem isConnected_iff_sUnion_disjoint_open {s : Set α} : theorem disjoint_or_subset_of_clopen {s t : Set α} (hs : IsPreconnected s) (ht : IsClopen t) : Disjoint s t ∨ s ⊆ t := (disjoint_or_nonempty_inter s t).imp_right <| hs.subset_clopen ht -#align disjoint_or_subset_of_clopen disjoint_or_subset_of_clopen /-- A set `s` is preconnected if and only if for every cover by two closed sets that are disjoint on `s`, @@ -1094,7 +993,6 @@ theorem isPreconnected_iff_subset_of_disjoint_closed : exact ⟨x, hxs, ⟨h hxs, hxv⟩⟩ · rcases hsu with ⟨x, hxs, hxu⟩ exact ⟨x, hxs, ⟨hxu, h hxs⟩⟩ -#align is_preconnected_iff_subset_of_disjoint_closed isPreconnected_iff_subset_of_disjoint_closed /-- A closed set `s` is preconnected if and only if for every cover by two closed sets that are disjoint, it is contained in one of the two covering sets. -/ @@ -1111,26 +1009,22 @@ theorem isPreconnected_iff_subset_of_fully_disjoint_closed {s : Set α} (hs : Is · rw [← inter_distrib_right] exact subset_inter hss Subset.rfl · rwa [disjoint_iff_inter_eq_empty, ← inter_inter_distrib_right, inter_comm] -#align is_preconnected_iff_subset_of_fully_disjoint_closed isPreconnected_iff_subset_of_fully_disjoint_closed theorem IsClopen.connectedComponent_subset {x} (hs : IsClopen s) (hx : x ∈ s) : connectedComponent x ⊆ s := isPreconnected_connectedComponent.subset_clopen hs ⟨x, mem_connectedComponent, hx⟩ -#align is_clopen.connected_component_subset IsClopen.connectedComponent_subset /-- The connected component of a point is always a subset of the intersection of all its clopen neighbourhoods. -/ theorem connectedComponent_subset_iInter_clopen {x : α} : connectedComponent x ⊆ ⋂ Z : { Z : Set α // IsClopen Z ∧ x ∈ Z }, Z := subset_iInter fun Z => Z.2.1.connectedComponent_subset Z.2.2 -#align connected_component_subset_Inter_clopen connectedComponent_subset_iInter_clopen /-- A clopen set is the union of its connected components. -/ theorem IsClopen.biUnion_connectedComponent_eq {Z : Set α} (h : IsClopen Z) : ⋃ x ∈ Z, connectedComponent x = Z := Subset.antisymm (iUnion₂_subset fun _ => h.connectedComponent_subset) fun _ h => mem_iUnion₂_of_mem h mem_connectedComponent -#align is_clopen.bUnion_connected_component_eq IsClopen.biUnion_connectedComponent_eq /-- The preimage of a connected component is preconnected if the function has connected fibers and a subset is closed iff the preimage is. -/ @@ -1209,7 +1103,6 @@ theorem preimage_connectedComponent_connected [TopologicalSpace β] {f : α → suffices f ⁻¹' connectedComponent t ⊆ f ⁻¹' T₂ from (this.trans T₂_v.1).trans (inter_subset_right _ _) exact preimage_mono h -#align preimage_connected_component_connected preimage_connectedComponent_connected theorem QuotientMap.preimage_connectedComponent [TopologicalSpace β] {f : α → β} (hf : QuotientMap f) (h_fibers : ∀ y : β, IsConnected (f ⁻¹' {y})) (a : α) : @@ -1217,13 +1110,11 @@ theorem QuotientMap.preimage_connectedComponent [TopologicalSpace β] {f : α ((preimage_connectedComponent_connected h_fibers (fun _ => hf.isClosed_preimage.symm) _).subset_connectedComponent mem_connectedComponent).antisymm (hf.continuous.mapsTo_connectedComponent a) -#align quotient_map.preimage_connected_component QuotientMap.preimage_connectedComponent theorem QuotientMap.image_connectedComponent [TopologicalSpace β] {f : α → β} (hf : QuotientMap f) (h_fibers : ∀ y : β, IsConnected (f ⁻¹' {y})) (a : α) : f '' connectedComponent a = connectedComponent (f a) := by rw [← hf.preimage_connectedComponent h_fibers, image_preimage_eq _ hf.surjective] -#align quotient_map.image_connected_component QuotientMap.image_connectedComponent end Preconnected @@ -1232,12 +1123,10 @@ section connectedComponentSetoid def connectedComponentSetoid (α : Type*) [TopologicalSpace α] : Setoid α := ⟨fun x y => connectedComponent x = connectedComponent y, ⟨fun x => by trivial, fun h1 => h1.symm, fun h1 h2 => h1.trans h2⟩⟩ -#align connected_component_setoid connectedComponentSetoid /-- The quotient of a space by its connected components -/ def ConnectedComponents (α : Type u) [TopologicalSpace α] := Quotient (connectedComponentSetoid α) -#align connected_components ConnectedComponents namespace ConnectedComponents @@ -1250,16 +1139,13 @@ instance : CoeTC α (ConnectedComponents α) := ⟨mk⟩ theorem coe_eq_coe {x y : α} : (x : ConnectedComponents α) = y ↔ connectedComponent x = connectedComponent y := Quotient.eq'' -#align connected_components.coe_eq_coe ConnectedComponents.coe_eq_coe theorem coe_ne_coe {x y : α} : (x : ConnectedComponents α) ≠ y ↔ connectedComponent x ≠ connectedComponent y := coe_eq_coe.not -#align connected_components.coe_ne_coe ConnectedComponents.coe_ne_coe theorem coe_eq_coe' {x y : α} : (x : ConnectedComponents α) = y ↔ x ∈ connectedComponent y := coe_eq_coe.trans connectedComponent_eq_iff_mem -#align connected_components.coe_eq_coe' ConnectedComponents.coe_eq_coe' instance [Inhabited α] : Inhabited (ConnectedComponents α) := ⟨mk default⟩ @@ -1269,21 +1155,17 @@ instance : TopologicalSpace (ConnectedComponents α) := theorem surjective_coe : Surjective (mk : α → ConnectedComponents α) := surjective_quot_mk _ -#align connected_components.surjective_coe ConnectedComponents.surjective_coe theorem quotientMap_coe : QuotientMap (mk : α → ConnectedComponents α) := quotientMap_quot_mk -#align connected_components.quotient_map_coe ConnectedComponents.quotientMap_coe @[continuity] theorem continuous_coe : Continuous (mk : α → ConnectedComponents α) := quotientMap_coe.continuous -#align connected_components.continuous_coe ConnectedComponents.continuous_coe @[simp] theorem range_coe : range (mk : α → ConnectedComponents α) = univ := surjective_coe.range_eq -#align connected_components.range_coe ConnectedComponents.range_coe end ConnectedComponents @@ -1293,14 +1175,12 @@ theorem connectedComponents_preimage_singleton {x : α} : (↑) ⁻¹' ({↑x} : Set (ConnectedComponents α)) = connectedComponent x := by ext y rw [mem_preimage, mem_singleton_iff, ConnectedComponents.coe_eq_coe'] -#align connected_components_preimage_singleton connectedComponents_preimage_singleton /-- The preimage of the image of a set under the quotient map to `connectedComponents α` is the union of the connected components of the elements in it. -/ theorem connectedComponents_preimage_image (U : Set α) : (↑) ⁻¹' ((↑) '' U : Set (ConnectedComponents α)) = ⋃ x ∈ U, connectedComponent x := by simp only [connectedComponents_preimage_singleton, preimage_iUnion₂, image_eq_iUnion] -#align connected_components_preimage_image connectedComponents_preimage_image @@ -1321,11 +1201,9 @@ theorem isPreconnected_of_forall_constant {s : Set α} exact (v_op.preimage continuous_subtype_val).isClosed_compl simpa [(u.mem_iff_boolIndicator _).mp x_in_u, (u.not_mem_iff_boolIndicator _).mp hy] using hs _ this x x_in_s y y_in_s -#align is_preconnected_of_forall_constant isPreconnected_of_forall_constant /-- A `PreconnectedSpace` version of `isPreconnected_of_forall_constant` -/ theorem preconnectedSpace_of_forall_constant (hs : ∀ f : α → Bool, Continuous f → ∀ x y, f x = f y) : PreconnectedSpace α := ⟨isPreconnected_of_forall_constant fun f hf x _ y _ => hs f (continuous_iff_continuousOn_univ.mpr hf) x y⟩ -#align preconnected_space_of_forall_constant preconnectedSpace_of_forall_constant diff --git a/Mathlib/Topology/Connected/LocallyConnected.lean b/Mathlib/Topology/Connected/LocallyConnected.lean index 40f3ce3ad7111..48c4a15878fab 100644 --- a/Mathlib/Topology/Connected/LocallyConnected.lean +++ b/Mathlib/Topology/Connected/LocallyConnected.lean @@ -30,13 +30,11 @@ equivalence later in `locallyConnectedSpace_iff_connected_basis`. -/ class LocallyConnectedSpace (α : Type*) [TopologicalSpace α] : Prop where /-- Open connected neighborhoods form a basis of the neighborhoods filter. -/ open_connected_basis : ∀ x, (𝓝 x).HasBasis (fun s : Set α => IsOpen s ∧ x ∈ s ∧ IsConnected s) id -#align locally_connected_space LocallyConnectedSpace theorem locallyConnectedSpace_iff_open_connected_basis : LocallyConnectedSpace α ↔ ∀ x, (𝓝 x).HasBasis (fun s : Set α => IsOpen s ∧ x ∈ s ∧ IsConnected s) id := ⟨@LocallyConnectedSpace.open_connected_basis _ _, LocallyConnectedSpace.mk⟩ -#align locally_connected_space_iff_open_connected_basis locallyConnectedSpace_iff_open_connected_basis theorem locallyConnectedSpace_iff_open_connected_subsets : LocallyConnectedSpace α ↔ @@ -50,7 +48,6 @@ theorem locallyConnectedSpace_iff_open_connected_subsets : · exact fun h => ⟨fun U => ⟨fun hU => let ⟨V, hVU, hV⟩ := h U hU ⟨V, hV, hVU⟩, fun ⟨V, ⟨hV, hxV, _⟩, hVU⟩ => mem_nhds_iff.mpr ⟨V, hVU, hV, hxV⟩⟩⟩ -#align locally_connected_space_iff_open_connected_subsets locallyConnectedSpace_iff_open_connected_subsets /-- A space with discrete topology is a locally connected space. -/ instance (priority := 100) DiscreteTopology.toLocallyConnectedSpace (α) [TopologicalSpace α] @@ -58,14 +55,12 @@ instance (priority := 100) DiscreteTopology.toLocallyConnectedSpace (α) [Topolo locallyConnectedSpace_iff_open_connected_subsets.2 fun x _U hU => ⟨{x}, singleton_subset_iff.2 <| mem_of_mem_nhds hU, isOpen_discrete _, rfl, isConnected_singleton⟩ -#align discrete_topology.to_locally_connected_space DiscreteTopology.toLocallyConnectedSpace theorem connectedComponentIn_mem_nhds [LocallyConnectedSpace α] {F : Set α} {x : α} (h : F ∈ 𝓝 x) : connectedComponentIn F x ∈ 𝓝 x := by rw [(LocallyConnectedSpace.open_connected_basis x).mem_iff] at h rcases h with ⟨s, ⟨h1s, hxs, h2s⟩, hsF⟩ exact mem_nhds_iff.mpr ⟨s, h2s.isPreconnected.subset_connectedComponentIn hxs hsF, h1s, hxs⟩ -#align connected_component_in_mem_nhds connectedComponentIn_mem_nhds protected theorem IsOpen.connectedComponentIn [LocallyConnectedSpace α] {F : Set α} {x : α} (hF : IsOpen F) : IsOpen (connectedComponentIn F x) := by @@ -73,18 +68,15 @@ protected theorem IsOpen.connectedComponentIn [LocallyConnectedSpace α] {F : Se intro y hy rw [connectedComponentIn_eq hy] exact connectedComponentIn_mem_nhds (hF.mem_nhds <| connectedComponentIn_subset F x hy) -#align is_open.connected_component_in IsOpen.connectedComponentIn theorem isOpen_connectedComponent [LocallyConnectedSpace α] {x : α} : IsOpen (connectedComponent x) := by rw [← connectedComponentIn_univ] exact isOpen_univ.connectedComponentIn -#align is_open_connected_component isOpen_connectedComponent theorem isClopen_connectedComponent [LocallyConnectedSpace α] {x : α} : IsClopen (connectedComponent x) := ⟨isOpen_connectedComponent, isClosed_connectedComponent⟩ -#align is_clopen_connected_component isClopen_connectedComponent theorem locallyConnectedSpace_iff_connectedComponentIn_open : LocallyConnectedSpace α ↔ @@ -99,7 +91,6 @@ theorem locallyConnectedSpace_iff_connectedComponentIn_open : (connectedComponentIn_subset _ _).trans interior_subset, h _ isOpen_interior x _, mem_connectedComponentIn _, isConnected_connectedComponentIn_iff.mpr _⟩ <;> exact mem_interior_iff_mem_nhds.mpr hU -#align locally_connected_space_iff_connected_component_in_open locallyConnectedSpace_iff_connectedComponentIn_open theorem locallyConnectedSpace_iff_connected_subsets : LocallyConnectedSpace α ↔ ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U := by @@ -113,14 +104,12 @@ theorem locallyConnectedSpace_iff_connected_subsets : rw [connectedComponentIn_eq hy] rcases h y U (hU.mem_nhds <| (connectedComponentIn_subset _ _) hy) with ⟨V, hVy, hV, hVU⟩ exact Filter.mem_of_superset hVy (hV.subset_connectedComponentIn (mem_of_mem_nhds hVy) hVU) -#align locally_connected_space_iff_connected_subsets locallyConnectedSpace_iff_connected_subsets theorem locallyConnectedSpace_iff_connected_basis : LocallyConnectedSpace α ↔ ∀ x, (𝓝 x).HasBasis (fun s : Set α => s ∈ 𝓝 x ∧ IsPreconnected s) id := by rw [locallyConnectedSpace_iff_connected_subsets] exact forall_congr' <| fun x => Filter.hasBasis_self.symm -#align locally_connected_space_iff_connected_basis locallyConnectedSpace_iff_connected_basis theorem locallyConnectedSpace_of_connected_bases {ι : Type*} (b : α → ι → Set α) (p : α → ι → Prop) (hbasis : ∀ x, (𝓝 x).HasBasis (p x) (b x)) @@ -130,7 +119,6 @@ theorem locallyConnectedSpace_of_connected_bases {ι : Type*} (b : α → ι → (hbasis x).to_hasBasis (fun i hi => ⟨b x i, ⟨(hbasis x).mem_of_mem hi, hconnected x i hi⟩, subset_rfl⟩) fun s hs => ⟨(hbasis x).index s hs.1, ⟨(hbasis x).property_index hs.1, (hbasis x).set_index_subset hs.1⟩⟩ -#align locally_connected_space_of_connected_bases locallyConnectedSpace_of_connected_bases theorem OpenEmbedding.locallyConnectedSpace [LocallyConnectedSpace α] [TopologicalSpace β] {f : β → α} (h : OpenEmbedding f) : LocallyConnectedSpace β := by diff --git a/Mathlib/Topology/Connected/TotallyDisconnected.lean b/Mathlib/Topology/Connected/TotallyDisconnected.lean index cfa0b6a03b780..fbb36fa13caad 100644 --- a/Mathlib/Topology/Connected/TotallyDisconnected.lean +++ b/Mathlib/Topology/Connected/TotallyDisconnected.lean @@ -31,27 +31,22 @@ section TotallyDisconnected a subsingleton, ie either empty or a singleton.-/ def IsTotallyDisconnected (s : Set α) : Prop := ∀ t, t ⊆ s → IsPreconnected t → t.Subsingleton -#align is_totally_disconnected IsTotallyDisconnected theorem isTotallyDisconnected_empty : IsTotallyDisconnected (∅ : Set α) := fun _ ht _ _ x_in _ _ => (ht x_in).elim -#align is_totally_disconnected_empty isTotallyDisconnected_empty theorem isTotallyDisconnected_singleton {x} : IsTotallyDisconnected ({x} : Set α) := fun _ ht _ => subsingleton_singleton.anti ht -#align is_totally_disconnected_singleton isTotallyDisconnected_singleton /-- A space is totally disconnected if all of its connected components are singletons. -/ @[mk_iff] class TotallyDisconnectedSpace (α : Type u) [TopologicalSpace α] : Prop where /-- The universal set `Set.univ` in a totally disconnected space is totally disconnected. -/ isTotallyDisconnected_univ : IsTotallyDisconnected (univ : Set α) -#align totally_disconnected_space TotallyDisconnectedSpace theorem IsPreconnected.subsingleton [TotallyDisconnectedSpace α] {s : Set α} (h : IsPreconnected s) : s.Subsingleton := TotallyDisconnectedSpace.isTotallyDisconnected_univ s (subset_univ s) h -#align is_preconnected.subsingleton IsPreconnected.subsingleton instance Pi.totallyDisconnectedSpace {α : Type*} {β : α → Type*} [∀ a, TopologicalSpace (β a)] [∀ a, TotallyDisconnectedSpace (β a)] : @@ -60,7 +55,6 @@ instance Pi.totallyDisconnectedSpace {α : Type*} {β : α → Type*} have this : ∀ a, IsPreconnected ((fun x : ∀ a, β a => x a) '' t) := fun a => h2.image (fun x => x a) (continuous_apply a).continuousOn fun x x_in y y_in => funext fun a => (this a).subsingleton ⟨x, x_in, rfl⟩ ⟨y, y_in, rfl⟩⟩ -#align pi.totally_disconnected_space Pi.totallyDisconnectedSpace instance Prod.totallyDisconnectedSpace [TopologicalSpace β] [TotallyDisconnectedSpace α] [TotallyDisconnectedSpace β] : TotallyDisconnectedSpace (α × β) := @@ -70,7 +64,6 @@ instance Prod.totallyDisconnectedSpace [TopologicalSpace β] [TotallyDisconnecte fun x hx y hy => Prod.ext (H1.subsingleton ⟨x, hx, rfl⟩ ⟨y, hy, rfl⟩) (H2.subsingleton ⟨x, hx, rfl⟩ ⟨y, hy, rfl⟩)⟩ -#align prod.totally_disconnected_space Prod.totallyDisconnectedSpace instance [TopologicalSpace β] [TotallyDisconnectedSpace α] [TotallyDisconnectedSpace β] : TotallyDisconnectedSpace (Sum α β) := by @@ -102,7 +95,6 @@ theorem isTotallyDisconnected_of_clopen_set {X : Type*} [TopologicalSpace X] hS U Uᶜ h_clopen.1 h_clopen.compl.1 (fun a _ => em (a ∈ U)) ⟨x, hx, hxU⟩ ⟨y, hy, hyU⟩ rw [inter_compl_self, Set.inter_empty] at hS exact Set.not_nonempty_empty hS -#align is_totally_disconnected_of_clopen_set isTotallyDisconnected_of_clopen_set /-- A space is totally disconnected iff its connected components are subsingletons. -/ theorem totallyDisconnectedSpace_iff_connectedComponent_subsingleton : @@ -117,7 +109,6 @@ theorem totallyDisconnectedSpace_iff_connectedComponent_subsingleton : rcases eq_empty_or_nonempty s with (rfl | ⟨x, x_in⟩) · exact subsingleton_empty · exact (h x).anti (hs.subset_connectedComponent x_in) -#align totally_disconnected_space_iff_connected_component_subsingleton totallyDisconnectedSpace_iff_connectedComponent_subsingleton /-- A space is totally disconnected iff its connected components are singletons. -/ theorem totallyDisconnectedSpace_iff_connectedComponent_singleton : @@ -126,12 +117,10 @@ theorem totallyDisconnectedSpace_iff_connectedComponent_singleton : refine forall_congr' fun x => ?_ rw [subsingleton_iff_singleton] exact mem_connectedComponent -#align totally_disconnected_space_iff_connected_component_singleton totallyDisconnectedSpace_iff_connectedComponent_singleton @[simp] theorem connectedComponent_eq_singleton [TotallyDisconnectedSpace α] (x : α) : connectedComponent x = {x} := totallyDisconnectedSpace_iff_connectedComponent_singleton.1 ‹_› x -#align connected_component_eq_singleton connectedComponent_eq_singleton /-- The image of a connected component in a totally disconnected space is a singleton. -/ @[simp] @@ -140,12 +129,10 @@ theorem Continuous.image_connectedComponent_eq_singleton {β : Type*} [Topologic f '' connectedComponent a = {f a} := (Set.subsingleton_iff_singleton <| mem_image_of_mem f mem_connectedComponent).mp (isPreconnected_connectedComponent.image f h.continuousOn).subsingleton -#align continuous.image_connected_component_eq_singleton Continuous.image_connectedComponent_eq_singleton theorem isTotallyDisconnected_of_totallyDisconnectedSpace [TotallyDisconnectedSpace α] (s : Set α) : IsTotallyDisconnected s := fun t _ ht => TotallyDisconnectedSpace.isTotallyDisconnected_univ _ t.subset_univ ht -#align is_totally_disconnected_of_totally_disconnected_space isTotallyDisconnected_of_totallyDisconnectedSpace theorem isTotallyDisconnected_of_image [TopologicalSpace β] {f : α → β} (hf : ContinuousOn f s) (hf' : Injective f) (h : IsTotallyDisconnected (f '' s)) : IsTotallyDisconnected s := @@ -153,12 +140,10 @@ theorem isTotallyDisconnected_of_image [TopologicalSpace β] {f : α → β} (hf hf' <| h _ (image_subset f hts) (ht.image f <| hf.mono hts) (mem_image_of_mem f x_in) (mem_image_of_mem f y_in) -#align is_totally_disconnected_of_image isTotallyDisconnected_of_image theorem Embedding.isTotallyDisconnected [TopologicalSpace β] {f : α → β} (hf : Embedding f) {s : Set α} (h : IsTotallyDisconnected (f '' s)) : IsTotallyDisconnected s := isTotallyDisconnected_of_image hf.continuous.continuousOn hf.inj h -#align embedding.is_totally_disconnected Embedding.isTotallyDisconnected lemma Embedding.isTotallyDisconnected_image [TopologicalSpace β] {f : α → β} (hf : Embedding f) {s : Set α} : IsTotallyDisconnected (f '' s) ↔ IsTotallyDisconnected s := by @@ -179,7 +164,6 @@ lemma totallyDisconnectedSpace_subtype_iff {s : Set α} : instance Subtype.totallyDisconnectedSpace {α : Type*} {p : α → Prop} [TopologicalSpace α] [TotallyDisconnectedSpace α] : TotallyDisconnectedSpace (Subtype p) := totallyDisconnectedSpace_subtype_iff.2 (isTotallyDisconnected_of_totallyDisconnectedSpace _) -#align subtype.totally_disconnected_space Subtype.totallyDisconnectedSpace end TotallyDisconnected @@ -191,14 +175,11 @@ by two disjoint open sets covering `s`. -/ def IsTotallySeparated (s : Set α) : Prop := ∀ x ∈ s, ∀ y ∈ s, x ≠ y → ∃ u v : Set α, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ s ⊆ u ∪ v ∧ Disjoint u v -#align is_totally_separated IsTotallySeparated theorem isTotallySeparated_empty : IsTotallySeparated (∅ : Set α) := fun _ => False.elim -#align is_totally_separated_empty isTotallySeparated_empty theorem isTotallySeparated_singleton {x} : IsTotallySeparated ({x} : Set α) := fun _ hp _ hq hpq => (hpq <| (eq_of_mem_singleton hp).symm ▸ (eq_of_mem_singleton hq).symm).elim -#align is_totally_separated_singleton isTotallySeparated_singleton theorem isTotallyDisconnected_of_isTotallySeparated {s : Set α} (H : IsTotallySeparated s) : IsTotallyDisconnected s := by @@ -210,30 +191,25 @@ theorem isTotallyDisconnected_of_isTotallySeparated {s : Set α} (H : IsTotallyS H x (hts x_in) y (hts y_in) h refine' (ht _ _ hu hv (hts.trans hs) ⟨x, x_in, hxu⟩ ⟨y, y_in, hyv⟩).ne_empty _ rw [huv.inter_eq, inter_empty] -#align is_totally_disconnected_of_is_totally_separated isTotallyDisconnected_of_isTotallySeparated alias IsTotallySeparated.isTotallyDisconnected := isTotallyDisconnected_of_isTotallySeparated -#align is_totally_separated.is_totally_disconnected IsTotallySeparated.isTotallyDisconnected /-- A space is totally separated if any two points can be separated by two disjoint open sets covering the whole space. -/ class TotallySeparatedSpace (α : Type u) [TopologicalSpace α] : Prop where /-- The universal set `Set.univ` in a totally separated space is totally separated. -/ isTotallySeparated_univ : IsTotallySeparated (univ : Set α) -#align totally_separated_space TotallySeparatedSpace -- see Note [lower instance priority] instance (priority := 100) TotallySeparatedSpace.totallyDisconnectedSpace (α : Type u) [TopologicalSpace α] [TotallySeparatedSpace α] : TotallyDisconnectedSpace α := ⟨TotallySeparatedSpace.isTotallySeparated_univ.isTotallyDisconnected⟩ -#align totally_separated_space.totally_disconnected_space TotallySeparatedSpace.totallyDisconnectedSpace -- see Note [lower instance priority] instance (priority := 100) TotallySeparatedSpace.of_discrete (α : Type*) [TopologicalSpace α] [DiscreteTopology α] : TotallySeparatedSpace α := ⟨fun _ _ b _ h => ⟨{b}ᶜ, {b}, isOpen_discrete _, isOpen_discrete _, h, rfl, (compl_union_self _).symm.subset, disjoint_compl_left⟩⟩ -#align totally_separated_space.of_discrete TotallySeparatedSpace.of_discrete theorem exists_clopen_of_totally_separated {α : Type*} [TopologicalSpace α] [TotallySeparatedSpace α] {x y : α} (hxy : x ≠ y) : @@ -244,7 +220,6 @@ theorem exists_clopen_of_totally_separated {α : Type*} [TopologicalSpace α] rw [univ_inter _] at clopen_U rw [← Set.subset_compl_iff_disjoint_right, subset_compl_comm] at disj exact ⟨U, clopen_U, Ux, disj Vy⟩ -#align exists_clopen_of_totally_separated exists_clopen_of_totally_separated end TotallySeparated @@ -256,42 +231,35 @@ theorem Continuous.image_eq_of_connectedComponent_eq (h : Continuous f) (a b : singleton_eq_singleton_iff.1 <| h.image_connectedComponent_eq_singleton a ▸ h.image_connectedComponent_eq_singleton b ▸ hab ▸ rfl -#align continuous.image_eq_of_connected_component_eq Continuous.image_eq_of_connectedComponent_eq /-- The lift to `connectedComponents α` of a continuous map from `α` to a totally disconnected space -/ def Continuous.connectedComponentsLift (h : Continuous f) : ConnectedComponents α → β := fun x => Quotient.liftOn' x f h.image_eq_of_connectedComponent_eq -#align continuous.connected_components_lift Continuous.connectedComponentsLift @[continuity] theorem Continuous.connectedComponentsLift_continuous (h : Continuous f) : Continuous h.connectedComponentsLift := h.quotient_liftOn' <| by convert h.image_eq_of_connectedComponent_eq -#align continuous.connected_components_lift_continuous Continuous.connectedComponentsLift_continuous @[simp] theorem Continuous.connectedComponentsLift_apply_coe (h : Continuous f) (x : α) : h.connectedComponentsLift x = f x := rfl -#align continuous.connected_components_lift_apply_coe Continuous.connectedComponentsLift_apply_coe @[simp] theorem Continuous.connectedComponentsLift_comp_coe (h : Continuous f) : h.connectedComponentsLift ∘ (↑) = f := rfl -#align continuous.connected_components_lift_comp_coe Continuous.connectedComponentsLift_comp_coe theorem connectedComponents_lift_unique' {β : Sort*} {g₁ g₂ : ConnectedComponents α → β} (hg : g₁ ∘ ((↑) : α → ConnectedComponents α) = g₂ ∘ (↑)) : g₁ = g₂ := ConnectedComponents.surjective_coe.injective_comp_right hg -#align connected_components_lift_unique' connectedComponents_lift_unique' theorem Continuous.connectedComponentsLift_unique (h : Continuous f) (g : ConnectedComponents α → β) (hg : g ∘ (↑) = f) : g = h.connectedComponentsLift := connectedComponents_lift_unique' <| hg.trans h.connectedComponentsLift_comp_coe.symm -#align continuous.connected_components_lift_unique Continuous.connectedComponentsLift_unique instance ConnectedComponents.totallyDisconnectedSpace : @@ -303,18 +271,15 @@ instance ConnectedComponents.totallyDisconnectedSpace : refine' ConnectedComponents.surjective_coe.forall.2 fun y => _ rw [connectedComponents_preimage_singleton] exact isConnected_connectedComponent -#align connected_components.totally_disconnected_space ConnectedComponents.totallyDisconnectedSpace /-- Functoriality of `connectedComponents` -/ def Continuous.connectedComponentsMap {β : Type*} [TopologicalSpace β] {f : α → β} (h : Continuous f) : ConnectedComponents α → ConnectedComponents β := Continuous.connectedComponentsLift (ConnectedComponents.continuous_coe.comp h) -#align continuous.connected_components_map Continuous.connectedComponentsMap theorem Continuous.connectedComponentsMap_continuous {β : Type*} [TopologicalSpace β] {f : α → β} (h : Continuous f) : Continuous h.connectedComponentsMap := Continuous.connectedComponentsLift_continuous (ConnectedComponents.continuous_coe.comp h) -#align continuous.connected_components_map_continuous Continuous.connectedComponentsMap_continuous /-- A preconnected set `s` has the property that every map to a discrete space that is continuous on `s` is constant on `s` -/ @@ -322,13 +287,11 @@ theorem IsPreconnected.constant {Y : Type*} [TopologicalSpace Y] [DiscreteTopolo (hs : IsPreconnected s) {f : α → Y} (hf : ContinuousOn f s) {x y : α} (hx : x ∈ s) (hy : y ∈ s) : f x = f y := (hs.image f hf).subsingleton (mem_image_of_mem f hx) (mem_image_of_mem f hy) -#align is_preconnected.constant IsPreconnected.constant /-- A `PreconnectedSpace` version of `isPreconnected.constant` -/ theorem PreconnectedSpace.constant {Y : Type*} [TopologicalSpace Y] [DiscreteTopology Y] (hp : PreconnectedSpace α) {f : α → Y} (hf : Continuous f) {x y : α} : f x = f y := IsPreconnected.constant hp.isPreconnected_univ (Continuous.continuousOn hf) trivial trivial -#align preconnected_space.constant PreconnectedSpace.constant /-- Refinement of `IsPreconnected.constant` only assuming the map factors through a discrete subset of the target. -/ @@ -338,7 +301,6 @@ theorem IsPreconnected.constant_of_mapsTo [TopologicalSpace β] {S : Set α} (hS let F : S → T := hTm.restrict f S T suffices F ⟨x, hx⟩ = F ⟨y, hy⟩ by rwa [← Subtype.coe_inj] at this exact (isPreconnected_iff_preconnectedSpace.mp hS).constant (hc.restrict_mapsTo _) -#align is_preconnected.constant_of_maps_to IsPreconnected.constant_of_mapsTo /-- A version of `IsPreconnected.constant_of_mapsTo` that assumes that the codomain is nonempty and proves that `f` is equal to `const α y` on `S` for some `y ∈ T`. -/