diff --git a/Mathlib.lean b/Mathlib.lean index f2911594599ca..6d47e1ee52f14 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -2197,6 +2197,7 @@ import Mathlib.GroupTheory.GroupAction.Option import Mathlib.GroupTheory.GroupAction.Pi import Mathlib.GroupTheory.GroupAction.Prod import Mathlib.GroupTheory.GroupAction.Quotient +import Mathlib.GroupTheory.GroupAction.Ring import Mathlib.GroupTheory.GroupAction.Sigma import Mathlib.GroupTheory.GroupAction.SubMulAction import Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise @@ -2974,6 +2975,7 @@ import Mathlib.Probability.ConditionalExpectation import Mathlib.Probability.ConditionalProbability import Mathlib.Probability.Density import Mathlib.Probability.Distributions.Exponential +import Mathlib.Probability.Distributions.Gamma import Mathlib.Probability.Distributions.Gaussian import Mathlib.Probability.IdentDistrib import Mathlib.Probability.Independence.Basic diff --git a/Mathlib/Algebra/Algebra/Subalgebra/Unitization.lean b/Mathlib/Algebra/Algebra/Subalgebra/Unitization.lean index 36397a3317628..be9a753c379de 100644 --- a/Mathlib/Algebra/Algebra/Subalgebra/Unitization.lean +++ b/Mathlib/Algebra/Algebra/Subalgebra/Unitization.lean @@ -3,11 +3,10 @@ Copyright (c) 2023 Jireh Loreaux. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Jireh Loreaux -/ - -import Mathlib.Algebra.Algebra.NonUnitalSubalgebra -import Mathlib.Algebra.Star.Subalgebra import Mathlib.Algebra.Algebra.Unitization import Mathlib.Algebra.Star.NonUnitalSubalgebra +import Mathlib.Algebra.Star.Subalgebra +import Mathlib.GroupTheory.GroupAction.Ring /-! # Relating unital and non-unital substructures diff --git a/Mathlib/Algebra/Associated.lean b/Mathlib/Algebra/Associated.lean index 680c895bef388..1c909dcee25d0 100644 --- a/Mathlib/Algebra/Associated.lean +++ b/Mathlib/Algebra/Associated.lean @@ -3,8 +3,6 @@ Copyright (c) 2018 Johannes Hölzl. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Johannes Hölzl, Jens Wagemaker -/ -import Mathlib.Algebra.Divisibility.Basic -import Mathlib.Algebra.GroupPower.Lemmas import Mathlib.Algebra.Parity #align_import algebra.associated from "leanprover-community/mathlib"@"2f3994e1b117b1e1da49bcfb67334f33460c3ce4" @@ -306,7 +304,7 @@ variable [CommMonoid α] {a : α} theorem Irreducible.not_square (ha : Irreducible a) : ¬IsSquare a := by rw [isSquare_iff_exists_sq] rintro ⟨b, rfl⟩ - exact not_irreducible_pow one_lt_two.ne' ha + exact not_irreducible_pow (by decide) ha #align irreducible.not_square Irreducible.not_square theorem IsSquare.not_irreducible (ha : IsSquare a) : ¬Irreducible a := fun h => h.not_square ha diff --git a/Mathlib/Algebra/Group/Commute/Basic.lean b/Mathlib/Algebra/Group/Commute/Basic.lean index 52526a31626af..ec86249c341d1 100644 --- a/Mathlib/Algebra/Group/Commute/Basic.lean +++ b/Mathlib/Algebra/Group/Commute/Basic.lean @@ -58,4 +58,38 @@ protected theorem div_div_div_comm (hbc : Commute b c) (hbd : Commute b⁻¹ d) end DivisionMonoid +section Group +variable [Group G] {a b : G} + +@[to_additive (attr := simp)] +lemma inv_left_iff : Commute a⁻¹ b ↔ Commute a b := SemiconjBy.inv_symm_left_iff +#align commute.inv_left_iff Commute.inv_left_iff +#align add_commute.neg_left_iff AddCommute.neg_left_iff + +@[to_additive] alias ⟨_, inv_left⟩ := inv_left_iff +#align commute.inv_left Commute.inv_left +#align add_commute.neg_left AddCommute.neg_left + +@[to_additive (attr := simp)] +lemma inv_right_iff : Commute a b⁻¹ ↔ Commute a b := SemiconjBy.inv_right_iff +#align commute.inv_right_iff Commute.inv_right_iff +#align add_commute.neg_right_iff AddCommute.neg_right_iff + +@[to_additive] alias ⟨_, inv_right⟩ := inv_right_iff +#align commute.inv_right Commute.inv_right +#align add_commute.neg_right AddCommute.neg_right + +@[to_additive] +protected lemma inv_mul_cancel (h : Commute a b) : a⁻¹ * b * a = b := by + rw [h.inv_left.eq, inv_mul_cancel_right] +#align commute.inv_mul_cancel Commute.inv_mul_cancel +#align add_commute.neg_add_cancel AddCommute.neg_add_cancel + +@[to_additive] +lemma inv_mul_cancel_assoc (h : Commute a b) : a⁻¹ * (b * a) = b := by + rw [← mul_assoc, h.inv_mul_cancel] +#align commute.inv_mul_cancel_assoc Commute.inv_mul_cancel_assoc +#align add_commute.neg_add_cancel_assoc AddCommute.neg_add_cancel_assoc + +end Group end Commute diff --git a/Mathlib/Algebra/Group/Commute/Units.lean b/Mathlib/Algebra/Group/Commute/Units.lean index ab88e7de6d631..e047ec8da22da 100644 --- a/Mathlib/Algebra/Group/Commute/Units.lean +++ b/Mathlib/Algebra/Group/Commute/Units.lean @@ -99,65 +99,4 @@ theorem _root_.isUnit_mul_self_iff : IsUnit (a * a) ↔ IsUnit a := #align is_add_unit_add_self_iff isAddUnit_add_self_iff end Monoid - -section Group - -variable [Group G] {a b : G} - -@[to_additive] -theorem inv_right : Commute a b → Commute a b⁻¹ := - SemiconjBy.inv_right -#align commute.inv_right Commute.inv_right -#align add_commute.neg_right AddCommute.neg_right - -@[to_additive (attr := simp)] -theorem inv_right_iff : Commute a b⁻¹ ↔ Commute a b := - SemiconjBy.inv_right_iff -#align commute.inv_right_iff Commute.inv_right_iff -#align add_commute.neg_right_iff AddCommute.neg_right_iff - -@[to_additive] -theorem inv_left : Commute a b → Commute a⁻¹ b := - SemiconjBy.inv_symm_left -#align commute.inv_left Commute.inv_left -#align add_commute.neg_left AddCommute.neg_left - -@[to_additive (attr := simp)] -theorem inv_left_iff : Commute a⁻¹ b ↔ Commute a b := - SemiconjBy.inv_symm_left_iff -#align commute.inv_left_iff Commute.inv_left_iff -#align add_commute.neg_left_iff AddCommute.neg_left_iff - -@[to_additive] -protected theorem inv_mul_cancel (h : Commute a b) : a⁻¹ * b * a = b := by - rw [h.inv_left.eq, inv_mul_cancel_right] -#align commute.inv_mul_cancel Commute.inv_mul_cancel -#align add_commute.neg_add_cancel AddCommute.neg_add_cancel - -@[to_additive] -theorem inv_mul_cancel_assoc (h : Commute a b) : a⁻¹ * (b * a) = b := by - rw [← mul_assoc, h.inv_mul_cancel] -#align commute.inv_mul_cancel_assoc Commute.inv_mul_cancel_assoc -#align add_commute.neg_add_cancel_assoc AddCommute.neg_add_cancel_assoc - -end Group - end Commute - -section CommGroup - -variable [CommGroup G] (a b : G) - -@[to_additive (attr := simp)] -theorem inv_mul_cancel_comm : a⁻¹ * b * a = b := - (Commute.all a b).inv_mul_cancel -#align inv_mul_cancel_comm inv_mul_cancel_comm -#align neg_add_cancel_comm neg_add_cancel_comm - -@[to_additive (attr := simp)] -theorem inv_mul_cancel_comm_assoc : a⁻¹ * (b * a) = b := - (Commute.all a b).inv_mul_cancel_assoc -#align inv_mul_cancel_comm_assoc inv_mul_cancel_comm_assoc -#align neg_add_cancel_comm_assoc neg_add_cancel_comm_assoc - -end CommGroup diff --git a/Mathlib/Algebra/Group/Defs.lean b/Mathlib/Algebra/Group/Defs.lean index 96578316890a6..5871222cc782d 100644 --- a/Mathlib/Algebra/Group/Defs.lean +++ b/Mathlib/Algebra/Group/Defs.lean @@ -998,6 +998,10 @@ theorem zpow_ofNat (a : G) : ∀ n : ℕ, a ^ (n : ℤ) = a ^ n #align zpow_of_nat zpow_ofNat #align of_nat_zsmul ofNat_zsmul +@[to_additive (attr := simp, norm_cast) coe_nat_zsmul] +lemma zpow_coe_nat (a : G) (n : ℕ) : a ^ (Nat.cast n : ℤ) = a ^ n := zpow_ofNat .. +#align coe_nat_zsmul coe_nat_zsmul + theorem zpow_negSucc (a : G) (n : ℕ) : a ^ (Int.negSucc n) = (a ^ (n + 1))⁻¹ := by rw [← zpow_ofNat] exact DivInvMonoid.zpow_neg' n a @@ -1263,6 +1267,16 @@ instance (priority := 100) CommGroup.toCancelCommMonoid : CancelCommMonoid G := instance (priority := 100) CommGroup.toDivisionCommMonoid : DivisionCommMonoid G := { ‹CommGroup G›, Group.toDivisionMonoid with } +@[to_additive (attr := simp)] lemma inv_mul_cancel_comm (a b : G) : a⁻¹ * b * a = b := by + rw [mul_comm, mul_inv_cancel_left] +#align inv_mul_cancel_comm inv_mul_cancel_comm +#align neg_add_cancel_comm neg_add_cancel_comm + +@[to_additive (attr := simp)] lemma inv_mul_cancel_comm_assoc (a b : G) : a⁻¹ * (b * a) = b := by + rw [mul_comm, mul_inv_cancel_right] +#align inv_mul_cancel_comm_assoc inv_mul_cancel_comm_assoc +#align neg_add_cancel_comm_assoc neg_add_cancel_comm_assoc + end CommGroup /-! We initialize all projections for `@[simps]` here, so that we don't have to do it in later diff --git a/Mathlib/Algebra/Group/Semiconj/Basic.lean b/Mathlib/Algebra/Group/Semiconj/Basic.lean index 05a807fabfd96..b3ff872fd9cf9 100644 --- a/Mathlib/Algebra/Group/Semiconj/Basic.lean +++ b/Mathlib/Algebra/Group/Semiconj/Basic.lean @@ -9,29 +9,47 @@ import Mathlib.Algebra.Group.Basic #align_import algebra.group.semiconj from "leanprover-community/mathlib"@"a148d797a1094ab554ad4183a4ad6f130358ef64" /-! -# Lemmas about semiconjugate elements of a semigroup +# Lemmas about semiconjugate elements of a group -/ namespace SemiconjBy +variable {G : Type*} section DivisionMonoid - -variable {G : Type*} [DivisionMonoid G] {a x y : G} +variable [DivisionMonoid G] {a x y : G} @[to_additive (attr := simp)] -theorem inv_inv_symm_iff : SemiconjBy a⁻¹ x⁻¹ y⁻¹ ↔ SemiconjBy a y x := - inv_involutive.injective.eq_iff.symm.trans <| by - rw [mul_inv_rev, mul_inv_rev, inv_inv, inv_inv, inv_inv, eq_comm, SemiconjBy] +theorem inv_inv_symm_iff : SemiconjBy a⁻¹ x⁻¹ y⁻¹ ↔ SemiconjBy a y x := by + simp_rw [SemiconjBy, ← mul_inv_rev, inv_inj, eq_comm] #align semiconj_by.inv_inv_symm_iff SemiconjBy.inv_inv_symm_iff #align add_semiconj_by.neg_neg_symm_iff AddSemiconjBy.neg_neg_symm_iff -@[to_additive] -theorem inv_inv_symm : SemiconjBy a x y → SemiconjBy a⁻¹ y⁻¹ x⁻¹ := - inv_inv_symm_iff.2 +@[to_additive] alias ⟨_, inv_inv_symm⟩ := inv_inv_symm_iff #align semiconj_by.inv_inv_symm SemiconjBy.inv_inv_symm #align add_semiconj_by.neg_neg_symm AddSemiconjBy.neg_neg_symm end DivisionMonoid +section Group +variable [Group G] {a x y : G} + +@[to_additive (attr := simp)] lemma inv_symm_left_iff : SemiconjBy a⁻¹ y x ↔ SemiconjBy a x y := by + simp_rw [SemiconjBy, eq_mul_inv_iff_mul_eq, mul_assoc, inv_mul_eq_iff_eq_mul, eq_comm] +#align semiconj_by.inv_symm_left_iff SemiconjBy.inv_symm_left_iff +#align add_semiconj_by.neg_symm_left_iff AddSemiconjBy.neg_symm_left_iff + +@[to_additive] alias ⟨_, inv_symm_left⟩ := inv_symm_left_iff +#align semiconj_by.inv_symm_left SemiconjBy.inv_symm_left +#align add_semiconj_by.neg_symm_left AddSemiconjBy.neg_symm_left + +@[to_additive (attr := simp)] lemma inv_right_iff : SemiconjBy a x⁻¹ y⁻¹ ↔ SemiconjBy a x y := by + rw [← inv_symm_left_iff, inv_inv_symm_iff] +#align add_semiconj_by.neg_right_iff AddSemiconjBy.neg_right_iff + +@[to_additive] alias ⟨_, inv_right⟩ := inv_right_iff +#align semiconj_by.inv_right SemiconjBy.inv_right +#align add_semiconj_by.neg_right AddSemiconjBy.neg_right + +end Group end SemiconjBy diff --git a/Mathlib/Algebra/Group/Semiconj/Units.lean b/Mathlib/Algebra/Group/Semiconj/Units.lean index 065963366ee40..b2a42301446fa 100644 --- a/Mathlib/Algebra/Group/Semiconj/Units.lean +++ b/Mathlib/Algebra/Group/Semiconj/Units.lean @@ -88,38 +88,6 @@ theorem units_val_iff {a x y : Mˣ} : SemiconjBy (a : M) x y ↔ SemiconjBy a x #align add_semiconj_by.add_units_coe_iff AddSemiconjBy.addUnits_val_iff end Monoid - -section Group - -variable [Group G] {a x y : G} - -@[to_additive (attr := simp)] -theorem inv_right_iff : SemiconjBy a x⁻¹ y⁻¹ ↔ SemiconjBy a x y := - @units_inv_right_iff G _ a ⟨x, x⁻¹, mul_inv_self x, inv_mul_self x⟩ - ⟨y, y⁻¹, mul_inv_self y, inv_mul_self y⟩ -#align semiconj_by.inv_right_iff SemiconjBy.inv_right_iff -#align add_semiconj_by.neg_right_iff AddSemiconjBy.neg_right_iff - -@[to_additive] -theorem inv_right : SemiconjBy a x y → SemiconjBy a x⁻¹ y⁻¹ := - inv_right_iff.2 -#align semiconj_by.inv_right SemiconjBy.inv_right -#align add_semiconj_by.neg_right AddSemiconjBy.neg_right - -@[to_additive (attr := simp)] -theorem inv_symm_left_iff : SemiconjBy a⁻¹ y x ↔ SemiconjBy a x y := - @units_inv_symm_left_iff G _ ⟨a, a⁻¹, mul_inv_self a, inv_mul_self a⟩ _ _ -#align semiconj_by.inv_symm_left_iff SemiconjBy.inv_symm_left_iff -#align add_semiconj_by.neg_symm_left_iff AddSemiconjBy.neg_symm_left_iff - -@[to_additive] -theorem inv_symm_left : SemiconjBy a x y → SemiconjBy a⁻¹ y x := - inv_symm_left_iff.2 -#align semiconj_by.inv_symm_left SemiconjBy.inv_symm_left -#align add_semiconj_by.neg_symm_left AddSemiconjBy.neg_symm_left - -end Group - end SemiconjBy /-- `a` semiconjugates `x` to `a * x * a⁻¹`. -/ diff --git a/Mathlib/Algebra/GroupPower/Basic.lean b/Mathlib/Algebra/GroupPower/Basic.lean index 7987521fafe72..71c1aff51bd68 100644 --- a/Mathlib/Algebra/GroupPower/Basic.lean +++ b/Mathlib/Algebra/GroupPower/Basic.lean @@ -3,9 +3,9 @@ Copyright (c) 2015 Jeremy Avigad. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Jeremy Avigad, Robert Y. Lewis -/ -import Mathlib.Algebra.Group.Commute.Units +import Mathlib.Algebra.Group.Commute.Basic import Mathlib.Algebra.GroupWithZero.Defs -import Mathlib.Tactic.Convert +import Mathlib.Tactic.Common #align_import algebra.group_power.basic from "leanprover-community/mathlib"@"9b2660e1b25419042c8da10bf411aa3c67f14383" diff --git a/Mathlib/Algebra/GroupPower/Lemmas.lean b/Mathlib/Algebra/GroupPower/Lemmas.lean index 32a1e07074ae7..d70f19479e54c 100644 --- a/Mathlib/Algebra/GroupPower/Lemmas.lean +++ b/Mathlib/Algebra/GroupPower/Lemmas.lean @@ -10,6 +10,7 @@ import Mathlib.Algebra.Order.Monoid.WithTop import Mathlib.Data.Nat.Pow import Mathlib.Data.Int.Cast.Lemmas import Mathlib.Algebra.Group.Opposite +import Mathlib.GroupTheory.GroupAction.Ring #align_import algebra.group_power.lemmas from "leanprover-community/mathlib"@"a07d750983b94c530ab69a726862c2ab6802b38c" @@ -511,24 +512,6 @@ theorem nsmul_eq_mul [NonAssocSemiring R] (n : ℕ) (a : R) : n • a = n * a := #align nsmul_eq_mul nsmul_eq_mulₓ -- typeclasses do not match up exactly. -/-- Note that `AddCommMonoid.nat_smulCommClass` requires stronger assumptions on `R`. -/ -instance NonUnitalNonAssocSemiring.nat_smulCommClass [NonUnitalNonAssocSemiring R] : - SMulCommClass ℕ R R := - ⟨fun n x y => by - induction' n with n ih - · simp [zero_nsmul] - · simp_rw [succ_nsmul, smul_eq_mul, mul_add, ← smul_eq_mul, ih]⟩ -#align non_unital_non_assoc_semiring.nat_smul_comm_class NonUnitalNonAssocSemiring.nat_smulCommClass - -/-- Note that `AddCommMonoid.nat_isScalarTower` requires stronger assumptions on `R`. -/ -instance NonUnitalNonAssocSemiring.nat_isScalarTower [NonUnitalNonAssocSemiring R] : - IsScalarTower ℕ R R := - ⟨fun n x y => by - induction' n with n ih - · simp [zero_nsmul] - · simp_rw [succ_nsmul, ← ih, smul_eq_mul, add_mul]⟩ -#align non_unital_non_assoc_semiring.nat_is_scalar_tower NonUnitalNonAssocSemiring.nat_isScalarTower - @[simp, norm_cast] theorem Nat.cast_pow [Semiring R] (n m : ℕ) : (↑(n ^ m) : R) = (↑n : R) ^ m := by induction' m with m ih @@ -596,24 +579,6 @@ theorem zsmul_eq_mul' [Ring R] (a : R) (n : ℤ) : n • a = a * n := by rw [zsmul_eq_mul, (n.cast_commute a).eq] #align zsmul_eq_mul' zsmul_eq_mul' -/-- Note that `AddCommGroup.int_smulCommClass` requires stronger assumptions on `R`. -/ -instance NonUnitalNonAssocRing.int_smulCommClass [NonUnitalNonAssocRing R] : - SMulCommClass ℤ R R := - ⟨fun n x y => - match n with - | (n : ℕ) => by simp_rw [coe_nat_zsmul, smul_comm] - | -[n+1] => by simp_rw [negSucc_zsmul, smul_eq_mul, mul_neg, mul_smul_comm]⟩ -#align non_unital_non_assoc_ring.int_smul_comm_class NonUnitalNonAssocRing.int_smulCommClass - -/-- Note that `AddCommGroup.int_isScalarTower` requires stronger assumptions on `R`. -/ -instance NonUnitalNonAssocRing.int_isScalarTower [NonUnitalNonAssocRing R] : - IsScalarTower ℤ R R := - ⟨fun n x y => - match n with - | (n : ℕ) => by simp_rw [coe_nat_zsmul, smul_assoc] - | -[n+1] => by simp_rw [negSucc_zsmul, smul_eq_mul, neg_mul, smul_mul_assoc]⟩ -#align non_unital_non_assoc_ring.int_is_scalar_tower NonUnitalNonAssocRing.int_isScalarTower - theorem zsmul_int_int (a b : ℤ) : a • b = a * b := by simp #align zsmul_int_int zsmul_int_int diff --git a/Mathlib/Algebra/GroupPower/NegOnePow.lean b/Mathlib/Algebra/GroupPower/NegOnePow.lean index e3de679ff6df6..fbc302478a720 100644 --- a/Mathlib/Algebra/GroupPower/NegOnePow.lean +++ b/Mathlib/Algebra/GroupPower/NegOnePow.lean @@ -86,4 +86,13 @@ lemma negOnePow_eq_iff (n₁ n₂ : ℤ) : Int.even_iff_not_odd, Int.even_iff_not_odd] tauto +@[simp] +lemma negOnePow_mul_self (n : ℤ) : (n * n).negOnePow = n.negOnePow := by + suffices Even (n * (n - 1)) by + simpa [mul_sub, mul_one, negOnePow_eq_iff] using this + rw [even_mul] + by_cases h : Even (n - 1) + · exact Or.inr h + · exact Or.inl (by simpa using Int.even_add_one.2 h) + end Int diff --git a/Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean b/Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean index 12d6df70373be..d0103b2dbd1c4 100644 --- a/Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean +++ b/Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean @@ -15,10 +15,11 @@ study how these cochains behave with respect to the shift on the complexes `K` and `L`. When `n`, `a`, `n'` are integers such that `h : n' + a = n`, -we obtain `rightShiftAddEquiv K L n a n' h : Cochain K L n ≃+ Cochain K L⟦a⟧ n'`. -This definition does not involve signs, but the analogous definition for -the shift on the first variable `K` shall involve signs (TODO), as we follow the -conventions appearing in the introduction of +we obtain `rightShiftAddEquiv K L n a n' h : Cochain K L n ≃+ Cochain K (L⟦a⟧) n'`. +This definition does not involve signs, but the analogous definition +of `leftShiftAddEquiv K L n a n' h' : Cochain K L n ≃+ Cochain (K⟦a⟧) L n'` +when `h' : n + a = n'` does involve signs, as we follow the conventions +appearing in the introduction of [Brian Conrad's book *Grothendieck duality and base change*][conrad2000]. ## References @@ -52,6 +53,20 @@ lemma rightShift_v (a n' : ℤ) (hn' : n' + a = n) (p q : ℤ) (hpq : p + n' = q dsimp only [rightShift] simp only [mk_v] +/-- The map `Cochain K L n → Cochain (K⟦a⟧) L n'` when `n + a = n'`. -/ +def leftShift (a n' : ℤ) (hn' : n + a = n') : Cochain (K⟦a⟧) L n' := + Cochain.mk (fun p q hpq => (a * n' + ((a * (a-1))/2)).negOnePow • + (K.shiftFunctorObjXIso a p (p + a) rfl).hom ≫ γ.v (p+a) q (by linarith)) + +lemma leftShift_v (a n' : ℤ) (hn' : n + a = n') (p q : ℤ) (hpq : p + n' = q) + (p' : ℤ) (hp' : p' + n = q) : + (γ.leftShift a n' hn').v p q hpq = (a * n' + ((a * (a - 1))/2)).negOnePow • + (K.shiftFunctorObjXIso a p p' + (by rw [← add_left_inj n, hp', add_assoc, add_comm a, hn', hpq])).hom ≫ γ.v p' q hp' := by + obtain rfl : p' = p + a := by linarith + dsimp only [leftShift] + simp only [mk_v] + /-- The map `Cochain K (L⟦a⟧) n' → Cochain K L n` when `n' + a = n`. -/ def rightUnshift {n' a : ℤ} (γ : Cochain K (L⟦a⟧) n') (n : ℤ) (hn : n' + a = n) : Cochain K L n := @@ -66,6 +81,37 @@ lemma rightUnshift_v {n' a : ℤ} (γ : Cochain K (L⟦a⟧) n') (n : ℤ) (hn : dsimp only [rightUnshift] simp only [mk_v] +/-- The map `Cochain (K⟦a⟧) L n' → Cochain K L n` when `n + a = n'`. -/ +def leftUnshift {n' a : ℤ} (γ : Cochain (K⟦a⟧) L n') (n : ℤ) (hn : n + a = n') : + Cochain K L n := + Cochain.mk (fun p q hpq => (a * n' + ((a * (a-1))/2)).negOnePow • + (K.shiftFunctorObjXIso a (p - a) p (by linarith)).inv ≫ γ.v (p-a) q (by linarith)) + +lemma leftUnshift_v {n' a : ℤ} (γ : Cochain (K⟦a⟧) L n') (n : ℤ) (hn : n + a = n') + (p q : ℤ) (hpq : p + n = q) (p' : ℤ) (hp' : p' + n' = q) : + (γ.leftUnshift n hn).v p q hpq = (a * n' + ((a * (a-1))/2)).negOnePow • + (K.shiftFunctorObjXIso a p' p (by linarith)).inv ≫ γ.v p' q (by linarith) := by + obtain rfl : p' = p - a := by linarith + rfl + +/-- The map `Cochain K L n → Cochain (K⟦a⟧) (L⟦a⟧) n`. -/ +def shift (a : ℤ) : Cochain (K⟦a⟧) (L⟦a⟧) n := + Cochain.mk (fun p q hpq => (K.shiftFunctorObjXIso a p _ rfl).hom ≫ + γ.v (p + a) (q + a) (by linarith) ≫ (L.shiftFunctorObjXIso a q _ rfl).inv) + +lemma shift_v (a : ℤ) (p q : ℤ) (hpq : p + n = q) (p' q' : ℤ) + (hp' : p' = p + a) (hq' : q' = q + a) : + (γ.shift a).v p q hpq = (K.shiftFunctorObjXIso a p p' hp').hom ≫ + γ.v p' q' (by rw [hp', hq', ← hpq, add_assoc, add_comm a, add_assoc]) ≫ + (L.shiftFunctorObjXIso a q q' hq').inv := by + subst hp' hq' + rfl + +lemma shift_v' (a : ℤ) (p q : ℤ) (hpq : p + n = q) : + (γ.shift a).v p q hpq = γ.v (p + a) (q + a) (by linarith) := by + simp only [shift_v γ a p q hpq _ _ rfl rfl, shiftFunctor_obj_X, shiftFunctorObjXIso, + HomologicalComplex.XIsoOfEq_rfl, Iso.refl_hom, Iso.refl_inv, comp_id, id_comp] + @[simp] lemma rightUnshift_rightShift (a n' : ℤ) (hn' : n' + a = n) : (γ.rightShift a n' hn').rightUnshift n hn' = γ := by @@ -82,6 +128,22 @@ lemma rightShift_rightUnshift {a n' : ℤ} (γ : Cochain K (L⟦a⟧) n') (n : γ.rightUnshift_v n hn' p (p + n) rfl q hpq, shiftFunctorObjXIso, assoc, Iso.hom_inv_id, comp_id] +@[simp] +lemma leftUnshift_leftShift (a n' : ℤ) (hn' : n + a = n') : + (γ.leftShift a n' hn').leftUnshift n hn' = γ := by + ext p q hpq + rw [(γ.leftShift a n' hn').leftUnshift_v n hn' p q hpq (q-n') (by linarith), + γ.leftShift_v a n' hn' (q-n') q (by linarith) p hpq, Linear.comp_units_smul, + Iso.inv_hom_id_assoc, smul_smul, Int.units_mul_self, one_smul] + +@[simp] +lemma leftShift_leftUnshift {a n' : ℤ} (γ : Cochain (K⟦a⟧) L n') (n : ℤ) (hn' : n + a = n') : + (γ.leftUnshift n hn').leftShift a n' hn' = γ := by + ext p q hpq + rw [(γ.leftUnshift n hn').leftShift_v a n' hn' p q hpq (q-n) (by linarith), + γ.leftUnshift_v n hn' (q-n) q (by linarith) p hpq, Linear.comp_units_smul, smul_smul, + Iso.hom_inv_id_assoc, Int.units_mul_self, one_smul] + @[simp] lemma rightShift_add (a n' : ℤ) (hn' : n' + a = n) : (γ₁ + γ₂).rightShift a n' hn' = γ₁.rightShift a n' hn' + γ₂.rightShift a n' hn' := by @@ -89,6 +151,19 @@ lemma rightShift_add (a n' : ℤ) (hn' : n' + a = n) : dsimp simp only [rightShift_v _ a n' hn' p q hpq _ rfl, add_v, add_comp] +@[simp] +lemma leftShift_add (a n' : ℤ) (hn' : n + a = n') : + (γ₁ + γ₂).leftShift a n' hn' = γ₁.leftShift a n' hn' + γ₂.leftShift a n' hn' := by + ext p q hpq + dsimp + simp only [leftShift_v _ a n' hn' p q hpq (p + a) (by linarith), add_v, comp_add, smul_add] + +@[simp] +lemma shift_add (a : ℤ) : + (γ₁ + γ₂).shift a = γ₁.shift a + γ₂.shift a:= by + ext p q hpq + simp [shift_v'] + variable (K L) /-- The additive equivalence `Cochain K L n ≃+ Cochain K L⟦a⟧ n'` when `n' + a = n`. -/ @@ -101,7 +176,22 @@ def rightShiftAddEquiv (n a n' : ℤ) (hn' : n' + a = n) : right_inv γ := by simp map_add' γ γ' := by simp -variable {K L} +/-- The additive equivalence `Cochain K L n ≃+ Cochain (K⟦a⟧) L n'` when `n + a = n'`. -/ +@[simps] +def leftShiftAddEquiv (n a n' : ℤ) (hn' : n + a = n') : + Cochain K L n ≃+ Cochain (K⟦a⟧) L n' where + toFun γ := γ.leftShift a n' hn' + invFun γ := γ.leftUnshift n hn' + left_inv γ := by simp + right_inv γ := by simp + map_add' γ γ' := by simp + +/-- The additive map `Cochain K L n →+ Cochain (K⟦a⟧) (L⟦a⟧) n`. -/ +@[simps!] +def shiftAddHom (n a : ℤ) : Cochain K L n →+ Cochain (K⟦a⟧) (L⟦a⟧) n := + AddMonoidHom.mk' (fun γ => γ.shift a) (by simp) + +variable (n) @[simp] lemma rightShift_zero (a n' : ℤ) (hn' : n' + a = n) : @@ -115,6 +205,26 @@ lemma rightUnshift_zero (a n' : ℤ) (hn' : n' + a = n) : change (rightShiftAddEquiv K L n a n' hn').symm 0 = 0 apply _root_.map_zero +@[simp] +lemma leftShift_zero (a n' : ℤ) (hn' : n + a = n') : + (0 : Cochain K L n).leftShift a n' hn' = 0 := by + change leftShiftAddEquiv K L n a n' hn' 0 = 0 + apply _root_.map_zero + +@[simp] +lemma leftUnshift_zero (a n' : ℤ) (hn' : n + a = n') : + (0 : Cochain (K⟦a⟧) L n').leftUnshift n hn' = 0 := by + change (leftShiftAddEquiv K L n a n' hn').symm 0 = 0 + apply _root_.map_zero + +@[simp] +lemma shift_zero (a : ℤ) : + (0 : Cochain K L n).shift a = 0 := by + change shiftAddHom K L n a 0 = 0 + apply _root_.map_zero + +variable {K L n} + @[simp] lemma rightShift_neg (a n' : ℤ) (hn' : n' + a = n) : (-γ).rightShift a n' hn' = -γ.rightShift a n' hn' := by @@ -127,12 +237,36 @@ lemma rightUnshift_neg {n' a : ℤ} (γ : Cochain K (L⟦a⟧) n') (n : ℤ) (hn change (rightShiftAddEquiv K L n a n' hn).symm (-γ) = _ apply _root_.map_neg +@[simp] +lemma leftShift_neg (a n' : ℤ) (hn' : n + a = n') : + (-γ).leftShift a n' hn' = -γ.leftShift a n' hn' := by + change leftShiftAddEquiv K L n a n' hn' (-γ) = _ + apply _root_.map_neg + +@[simp] +lemma leftUnshift_neg {n' a : ℤ} (γ : Cochain (K⟦a⟧) L n') (n : ℤ) (hn : n + a = n') : + (-γ).leftUnshift n hn = -γ.leftUnshift n hn := by + change (leftShiftAddEquiv K L n a n' hn).symm (-γ) = _ + apply _root_.map_neg + +@[simp] +lemma shift_neg (a : ℤ) : + (-γ).shift a = -γ.shift a := by + change shiftAddHom K L n a (-γ) = _ + apply _root_.map_neg + @[simp] lemma rightUnshift_add {n' a : ℤ} (γ₁ γ₂ : Cochain K (L⟦a⟧) n') (n : ℤ) (hn : n' + a = n) : (γ₁ + γ₂).rightUnshift n hn = γ₁.rightUnshift n hn + γ₂.rightUnshift n hn := by change (rightShiftAddEquiv K L n a n' hn).symm (γ₁ + γ₂) = _ apply _root_.map_add +@[simp] +lemma leftUnshift_add {n' a : ℤ} (γ₁ γ₂ : Cochain (K⟦a⟧) L n') (n : ℤ) (hn : n + a = n') : + (γ₁ + γ₂).leftUnshift n hn = γ₁.leftUnshift n hn + γ₂.leftUnshift n hn := by + change (leftShiftAddEquiv K L n a n' hn).symm (γ₁ + γ₂) = _ + apply _root_.map_add + @[simp] lemma rightShift_smul (a n' : ℤ) (hn' : n' + a = n) (x : R) : (x • γ).rightShift a n' hn' = x • γ.rightShift a n' hn' := by @@ -140,6 +274,20 @@ lemma rightShift_smul (a n' : ℤ) (hn' : n' + a = n) (x : R) : dsimp simp only [rightShift_v _ a n' hn' p q hpq _ rfl, smul_v, Linear.smul_comp] +@[simp] +lemma leftShift_smul (a n' : ℤ) (hn' : n + a = n') (x : R) : + (x • γ).leftShift a n' hn' = x • γ.leftShift a n' hn' := by + ext p q hpq + dsimp + simp only [leftShift_v _ a n' hn' p q hpq (p + a) (by linarith), smul_v, Linear.comp_smul, + smul_comm x] + +@[simp] +lemma shift_smul (a : ℤ) (x : R) : + (x • γ).shift a = x • (γ.shift a) := by + ext p q hpq + simp [shift_v'] + variable (K L R) /-- The linear equivalence `Cochain K L n ≃+ Cochain K L⟦a⟧ n'` when `n' + a = n` and @@ -149,6 +297,20 @@ def rightShiftLinearEquiv (n a n' : ℤ) (hn' : n' + a = n) : Cochain K L n ≃ₗ[R] Cochain K (L⟦a⟧) n' := (rightShiftAddEquiv K L n a n' hn').toLinearEquiv (fun x γ => by simp) +/-- The additive equivalence `Cochain K L n ≃+ Cochain (K⟦a⟧) L n'` when `n + a = n'` and +the category is `R`-linear. -/ +@[simps!] +def leftShiftLinearEquiv (n a n' : ℤ) (hn : n + a = n') : + Cochain K L n ≃ₗ[R] Cochain (K⟦a⟧) L n' := + (leftShiftAddEquiv K L n a n' hn).toLinearEquiv (fun x γ => by simp) + +/-- The linear map `Cochain K L n ≃+ Cochain (K⟦a⟧) (L⟦a⟧) n` when the category is `R`-linear. -/ +@[simps!] +def shiftLinearMap (n a : ℤ) : + Cochain K L n →ₗ[R] Cochain (K⟦a⟧) (L⟦a⟧) n where + toAddHom := shiftAddHom K L n a + map_smul' _ _ := by simp + variable {K L R} @[simp] @@ -156,6 +318,17 @@ lemma rightShift_units_smul (a n' : ℤ) (hn' : n' + a = n) (x : Rˣ) : (x • γ).rightShift a n' hn' = x • γ.rightShift a n' hn' := by apply rightShift_smul +@[simp] +lemma leftShift_units_smul (a n' : ℤ) (hn' : n + a = n') (x : Rˣ) : + (x • γ).leftShift a n' hn' = x • γ.leftShift a n' hn' := by + apply leftShift_smul + +@[simp] +lemma shift_units_smul (a : ℤ) (x : Rˣ) : + (x • γ).shift a = x • (γ.shift a) := by + ext p q hpq + simp [shift_v'] + @[simp] lemma rightUnshift_smul {n' a : ℤ} (γ : Cochain K (L⟦a⟧) n') (n : ℤ) (hn : n' + a = n) (x : R) : (x • γ).rightUnshift n hn = x • γ.rightUnshift n hn := by @@ -168,6 +341,18 @@ lemma rightUnshift_units_smul {n' a : ℤ} (γ : Cochain K (L⟦a⟧) n') (n : (x • γ).rightUnshift n hn = x • γ.rightUnshift n hn := by apply rightUnshift_smul +@[simp] +lemma leftUnshift_smul {n' a : ℤ} (γ : Cochain (K⟦a⟧) L n') (n : ℤ) (hn : n + a = n') (x : R) : + (x • γ).leftUnshift n hn = x • γ.leftUnshift n hn := by + change (leftShiftLinearEquiv R K L n a n' hn).symm (x • γ) = _ + apply map_smul + +@[simp] +lemma leftUnshift_units_smul {n' a : ℤ} (γ : Cochain (K⟦a⟧) L n') (n : ℤ) + (hn : n + a = n') (x : Rˣ) : + (x • γ).leftUnshift n hn = x • γ.leftUnshift n hn := by + apply leftUnshift_smul + lemma rightUnshift_comp {m : ℤ} {a : ℤ} (γ' : Cochain L (M⟦a⟧) m) {nm : ℤ} (hnm : n + m = nm) (nm' : ℤ) (hnm' : nm + a = nm') (m' : ℤ) (hm' : m + a = m') : (γ.comp γ' hnm).rightUnshift nm' hnm' = @@ -178,6 +363,27 @@ lemma rightUnshift_comp {m : ℤ} {a : ℤ} (γ' : Cochain L (M⟦a⟧) m) {nm : comp_v _ _ (show n + m' = nm' by linarith) p (p + n) q (by linarith) (by linarith), γ'.rightUnshift_v m' hm' (p + n) q (by linarith) (p + n + m) rfl, assoc] +lemma leftShift_comp (a n' : ℤ) (hn' : n + a = n') {m t t' : ℤ} (γ' : Cochain L M m) + (h : n + m = t) (ht' : t + a = t') : + (γ.comp γ' h).leftShift a t' ht' = (a * m).negOnePow • (γ.leftShift a n' hn').comp γ' + (by rw [← ht', ← h, ← hn', add_assoc, add_comm a, add_assoc]) := by + ext p q hpq + have h' : n' + m = t' := by linarith + dsimp + simp only [Cochain.comp_v _ _ h' p (p + n') q rfl (by linarith), + γ.leftShift_v a n' hn' p (p + n') rfl (p + a) (by linarith), + (γ.comp γ' h).leftShift_v a t' (by linarith) p q hpq (p + a) (by linarith), + smul_smul, Linear.units_smul_comp, assoc, Int.negOnePow_add, ← mul_assoc, ← h', + comp_v _ _ h (p + a) (p + n') q (by linarith) (by linarith)] + congr 2 + rw [add_comm n', mul_add, Int.negOnePow_add] + +@[simp] +lemma leftShift_comp_zero_cochain (a n' : ℤ) (hn' : n + a = n') (γ' : Cochain L M 0) : + (γ.comp γ' (add_zero n)).leftShift a n' hn' = + (γ.leftShift a n' hn').comp γ' (add_zero n') := by + rw [leftShift_comp γ a n' hn' γ' (add_zero _) hn', mul_zero, Int.negOnePow_zero, one_smul] + lemma δ_rightShift (a n' m' : ℤ) (hn' : n' + a = n) (m : ℤ) (hm' : m' + a = m) : δ n' m' (γ.rightShift a n' hn') = a.negOnePow • (δ n m γ).rightShift a m' hm' := by by_cases hnm : n + 1 = m @@ -207,6 +413,78 @@ lemma δ_rightUnshift {a n' : ℤ} (γ : Cochain K (L⟦a⟧) n') (n : ℤ) (hn simp only [rightUnshift_rightShift, γ'.δ_rightShift a n' m' hn m hm', rightUnshift_units_smul, smul_smul, Int.units_mul_self, one_smul] +lemma δ_leftShift (a n' m' : ℤ) (hn' : n + a = n') (m : ℤ) (hm' : m + a = m') : + δ n' m' (γ.leftShift a n' hn') = a.negOnePow • (δ n m γ).leftShift a m' hm' := by + by_cases hnm : n + 1 = m + · have hnm' : n' + 1 = m' := by linarith + ext p q hpq + dsimp + rw [(δ n m γ).leftShift_v a m' hm' p q hpq (p+a) (by linarith), + δ_v n m hnm _ (p+a) q (by linarith) (p+n') (p+1+a) (by linarith) (by linarith), + δ_v n' m' hnm' _ p q hpq (p+n') (p+1) (by linarith) rfl, + γ.leftShift_v a n' hn' p (p+n') rfl (p+a) (by linarith), + γ.leftShift_v a n' hn' (p+1) q (by linarith) (p+1+a) (by linarith)] + simp only [shiftFunctor_obj_X, shiftFunctorObjXIso, HomologicalComplex.XIsoOfEq_rfl, + Iso.refl_hom, id_comp, Linear.units_smul_comp, shiftFunctor_obj_d', + Linear.comp_units_smul, smul_add, smul_smul] + congr 2 + · rw [← hnm', add_comm n', mul_add, mul_one] + simp only [Int.negOnePow_add, ← mul_assoc, Int.units_mul_self, one_mul] + · simp only [← Int.negOnePow_add, ← hn', ← hm', ← hnm] + congr 1 + linarith + · have hnm' : ¬ n' + 1 = m' := fun _ => hnm (by linarith) + rw [δ_shape _ _ hnm', δ_shape _ _ hnm, leftShift_zero, smul_zero] + +lemma δ_leftUnshift {a n' : ℤ} (γ : Cochain (K⟦a⟧) L n') (n : ℤ) (hn : n + a = n') + (m m' : ℤ) (hm' : m + a = m') : + δ n m (γ.leftUnshift n hn) = a.negOnePow • (δ n' m' γ).leftUnshift m hm' := by + obtain ⟨γ', rfl⟩ := (leftShiftAddEquiv K L n a n' hn).surjective γ + dsimp + simp only [leftUnshift_leftShift, γ'.δ_leftShift a n' m' hn m hm', leftUnshift_units_smul, + smul_smul, Int.units_mul_self, one_smul] + +@[simp] +lemma δ_shift (a m : ℤ) : + δ n m (γ.shift a) = a.negOnePow • (δ n m γ).shift a := by + by_cases hnm : n + 1 = m + · ext p q hpq + dsimp + simp only [shift_v', sub_add_cancel, shiftFunctor_obj_d', + δ_v n m hnm _ p q hpq (q - 1) (p + 1) rfl rfl, + δ_v n m hnm _ (p + a) (q + a) (by linarith) (q - 1 + a) (p + 1 + a) + (by linarith) (by linarith), + smul_add, Linear.units_smul_comp, Linear.comp_units_smul, add_right_inj] + rw [smul_comm] + · rw [δ_shape _ _ hnm, δ_shape _ _ hnm, shift_zero, smul_zero] + +lemma leftShift_rightShift (a n' : ℤ) (hn' : n' + a = n) : + (γ.rightShift a n' hn').leftShift a n hn' = + (a * n + (a * (a - 1)) / 2).negOnePow • γ.shift a := by + ext p q hpq + simp only [leftShift_v _ a n hn' p q hpq (p + a) (by linarith), + rightShift_v _ a n' hn' (p + a) q (by linarith) (q + a) (by linarith), units_smul_v, shift_v'] + dsimp + rw [id_comp, comp_id] + +lemma rightShift_leftShift (a n' : ℤ) (hn' : n + a = n') : + (γ.leftShift a n' hn').rightShift a n hn' = + (a * n' + (a * (a - 1)) / 2).negOnePow • γ.shift a := by + ext p q hpq + simp only [rightShift_v _ a n hn' p q hpq (q + a) (by linarith), + leftShift_v _ a n' hn' p (q + a) (by linarith) (p + a) (by linarith), units_smul_v, shift_v'] + dsimp + rw [id_comp, comp_id] + +/-- The left and right shift of cochains commute only up to a sign. -/ +lemma leftShift_rightShift_eq_negOnePow_rightShift_leftShift + (a n' n'' : ℤ) (hn' : n' + a = n) (hn'' : n + a = n'') : + (γ.rightShift a n' hn').leftShift a n hn' = + a.negOnePow • (γ.leftShift a n'' hn'').rightShift a n hn'' := by + rw [leftShift_rightShift, rightShift_leftShift, smul_smul, ← hn'', add_comm n a, mul_add, + Int.negOnePow_add, Int.negOnePow_add, Int.negOnePow_add, Int.negOnePow_mul_self, + ← mul_assoc, ← mul_assoc, Int.units_mul_self, one_mul] + end Cochain namespace Cocycle @@ -227,6 +505,28 @@ def rightUnshift {n' a : ℤ} (γ : Cocycle K (L⟦a⟧) n') (n : ℤ) (hn : n' rw [Cochain.δ_rightUnshift _ n hn (n + 1) (n + 1 - a) (by linarith), δ_eq_zero, Cochain.rightUnshift_zero, smul_zero]) +/-- The map `Cocycle K L n → Cocycle (K⟦a⟧) L n'` when `n + a = n'`. -/ +@[simps!] +def leftShift (γ : Cocycle K L n) (a n' : ℤ) (hn' : n + a = n') : + Cocycle (K⟦a⟧) L n' := + Cocycle.mk (γ.1.leftShift a n' hn') _ rfl (by + simp only [Cochain.δ_leftShift _ a n' (n' + 1) hn' (n + 1) (by linarith), + δ_eq_zero, Cochain.leftShift_zero, smul_zero]) + +/-- The map `Cocycle (K⟦a⟧) L n' → Cocycle K L n` when `n + a = n'`. -/ +@[simps!] +def leftUnshift {n' a : ℤ} (γ : Cocycle (K⟦a⟧) L n') (n : ℤ) (hn : n + a = n') : + Cocycle K L n := + Cocycle.mk (γ.1.leftUnshift n hn) _ rfl (by + rw [Cochain.δ_leftUnshift _ n hn (n + 1) (n + 1 + a) rfl, + δ_eq_zero, Cochain.leftUnshift_zero, smul_zero]) + +/-- The map `Cocycle K L n → Cocycle (K⟦a⟧) (L⟦a⟧) n`. -/ +@[simps!] +def shift (γ : Cocycle K L n) (a : ℤ) : + Cocycle (K⟦a⟧) (L⟦a⟧) n := + Cocycle.mk (γ.1.shift a) _ rfl (by simp) + end Cocycle end CochainComplex.HomComplex diff --git a/Mathlib/Algebra/Homology/HomotopyCofiber.lean b/Mathlib/Algebra/Homology/HomotopyCofiber.lean index 3c4e3799651b4..c40dcc9bdef3f 100644 --- a/Mathlib/Algebra/Homology/HomotopyCofiber.lean +++ b/Mathlib/Algebra/Homology/HomotopyCofiber.lean @@ -18,7 +18,7 @@ When we assume `hc : ∀ j, ∃ i, c.Rel i j` (which holds in the case of chain or cochain complexes indexed by `ℤ`), then for any homological complex `K`, there is a bijection `HomologicalComplex.homotopyCofiber.descEquiv φ K hc` between `homotopyCofiber φ ⟶ K` and the tuples `(α, hα)` with -`α : G ⟶ K` and `hα : Homotopy (φ ≫ α) 0` (TODO). +`α : G ⟶ K` and `hα : Homotopy (φ ≫ α) 0`. We shall also study the cylinder of a homological complex `K`: this is the homotopy cofiber of the morphism `biprod.lift (𝟙 K) (-𝟙 K) : K ⟶ K ⊞ K`. @@ -229,4 +229,142 @@ noncomputable def homotopyCofiber : HomologicalComplex C c where · simp [homotopyCofiber.inlX_d' φ j k hjk hk] · simp + +namespace homotopyCofiber + +/-- The right inclusion `G ⟶ homotopyCofiber φ`. -/ +@[simps!] +noncomputable def inr : G ⟶ homotopyCofiber φ where + f i := inrX φ i + +section + +variable (hc : ∀ j, ∃ i, c.Rel i j) + +/-- The composition `φ ≫ mappingCone.inr φ` is homotopic to `0`. -/ +noncomputable def inrCompHomotopy : + Homotopy (φ ≫ inr φ) 0 where + hom i j := + if hij : c.Rel j i then inlX φ i j hij else 0 + zero i j hij := dif_neg hij + comm j := by + obtain ⟨i, hij⟩ := hc j + rw [prevD_eq _ hij, dif_pos hij] + by_cases hj : c.Rel j (c.next j) + · simp only [comp_f, homotopyCofiber_d, zero_f, add_zero, + inlX_d φ i j _ hij hj, dNext_eq _ hj, dif_pos hj, + add_neg_cancel_left, inr_f] + · rw [dNext_eq_zero _ _ hj, zero_add, zero_f, add_zero, homotopyCofiber_d, + inlX_d' _ _ _ _ hj, comp_f, inr_f] + +lemma inrCompHomotopy_hom (i j : ι) (hij : c.Rel j i) : + (inrCompHomotopy φ hc).hom i j = inlX φ i j hij := dif_pos hij + +lemma inrCompHomotopy_hom_eq_zero (i j : ι) (hij : ¬ c.Rel j i) : + (inrCompHomotopy φ hc).hom i j = 0 := dif_neg hij + +end + +section + +variable (α : G ⟶ K) (hα : Homotopy (φ ≫ α) 0) + +/-- The morphism `homotopyCofiber φ ⟶ K` that is induced by a morphism `α : G ⟶ K` +and a homotopy `hα : Homotopy (φ ≫ α) 0`. -/ +noncomputable def desc : + homotopyCofiber φ ⟶ K where + f j := + if hj : c.Rel j (c.next j) + then fstX φ j _ hj ≫ hα.hom _ j + sndX φ j ≫ α.f j + else sndX φ j ≫ α.f j + comm' j k hjk := by + obtain rfl := c.next_eq' hjk + dsimp + simp [dif_pos hjk] + have H := hα.comm (c.next j) + simp only [comp_f, zero_f, add_zero, prevD_eq _ hjk] at H + split_ifs with hj + · simp only [comp_add, d_sndX_assoc _ _ _ hjk, add_comp, assoc, H, + d_fstX_assoc _ _ _ _ hjk, neg_comp, dNext, AddMonoidHom.mk'_apply] + abel + · simp only [d_sndX_assoc _ _ _ hjk, add_comp, assoc, add_left_inj, H, + dNext_eq_zero _ _ hj, zero_add] + +lemma desc_f (j k : ι) (hjk : c.Rel j k) : + (desc φ α hα).f j = fstX φ j _ hjk ≫ hα.hom _ j + sndX φ j ≫ α.f j := by + obtain rfl := c.next_eq' hjk + apply dif_pos hjk + +lemma desc_f' (j : ι) (hj : ¬ c.Rel j (c.next j)) : + (desc φ α hα).f j = sndX φ j ≫ α.f j := by + apply dif_neg hj + +@[reassoc (attr := simp)] +lemma inlX_desc_f (i j : ι) (hjk : c.Rel j i) : + inlX φ i j hjk ≫ (desc φ α hα).f j = hα.hom i j := by + obtain rfl := c.next_eq' hjk + dsimp [desc] + rw [dif_pos hjk, comp_add, inlX_fstX_assoc, inlX_sndX_assoc, zero_comp, add_zero] + +@[reassoc (attr := simp)] +lemma inrX_desc_f (i : ι) : + inrX φ i ≫ (desc φ α hα).f i = α.f i := by + dsimp [desc] + split_ifs <;> simp + +@[reassoc (attr := simp)] +lemma inr_desc : + inr φ ≫ desc φ α hα = α := by aesop_cat + +@[reassoc (attr := simp)] +lemma inrCompHomotopy_hom_desc_hom (hc : ∀ j, ∃ i, c.Rel i j) (i j : ι) : + (inrCompHomotopy φ hc).hom i j ≫ (desc φ α hα).f j = hα.hom i j := by + by_cases hij : c.Rel j i + · dsimp + simp only [inrCompHomotopy_hom φ hc i j hij, desc_f φ α hα _ _ hij, + comp_add, inlX_fstX_assoc, inlX_sndX_assoc, zero_comp, add_zero] + · simp only [Homotopy.zero _ _ _ hij, zero_comp] + +lemma eq_desc (f : homotopyCofiber φ ⟶ K) (hc : ∀ j, ∃ i, c.Rel i j) : + f = desc φ (inr φ ≫ f) (Homotopy.trans (Homotopy.ofEq (by simp)) + (((inrCompHomotopy φ hc).compRight f).trans (Homotopy.ofEq (by simp)))) := by + ext j + by_cases hj : c.Rel j (c.next j) + · apply ext_from_X φ _ _ hj + · simp [inrCompHomotopy_hom _ _ _ _ hj] + · simp + · apply ext_from_X' φ _ hj + simp + +end + +lemma descSigma_ext_iff {K : HomologicalComplex C c} + (x y : Σ (α : G ⟶ K), Homotopy (φ ≫ α) 0) : + x = y ↔ x.1 = y.1 ∧ (∀ (i j : ι) (_ : c.Rel j i), x.2.hom i j = y.2.hom i j) := by + constructor + · rintro rfl + tauto + · obtain ⟨x₁, x₂⟩ := x + obtain ⟨y₁, y₂⟩ := y + rintro ⟨rfl, h⟩ + simp only [Sigma.mk.inj_iff, heq_eq_eq, true_and] + ext i j + by_cases hij : c.Rel j i + · exact h _ _ hij + · simp only [Homotopy.zero _ _ _ hij] + +/-- Morphisms `homotopyCofiber φ ⟶ K` are uniquely determined by +a morphism `α : G ⟶ K` and a homotopy from `φ ≫ α` to `0`. -/ +noncomputable def descEquiv (K : HomologicalComplex C c) (hc : ∀ j, ∃ i, c.Rel i j) : + (Σ (α : G ⟶ K), Homotopy (φ ≫ α) 0) ≃ (homotopyCofiber φ ⟶ K) where + toFun := fun ⟨α, hα⟩ => desc φ α hα + invFun f := ⟨inr φ ≫ f, Homotopy.trans (Homotopy.ofEq (by simp)) + (((inrCompHomotopy φ hc).compRight f).trans (Homotopy.ofEq (by simp)))⟩ + right_inv f := (eq_desc φ f hc).symm + left_inv := fun ⟨α, hα⟩ => by + rw [descSigma_ext_iff] + aesop_cat + +end homotopyCofiber + end HomologicalComplex diff --git a/Mathlib/Algebra/Lie/Free.lean b/Mathlib/Algebra/Lie/Free.lean index ed701c023455d..b2c5bfcc93ae9 100644 --- a/Mathlib/Algebra/Lie/Free.lean +++ b/Mathlib/Algebra/Lie/Free.lean @@ -3,10 +3,10 @@ Copyright (c) 2021 Oliver Nash. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Oliver Nash -/ -import Mathlib.Algebra.Lie.OfAssociative +import Mathlib.Algebra.FreeNonUnitalNonAssocAlgebra import Mathlib.Algebra.Lie.NonUnitalNonAssocAlgebra import Mathlib.Algebra.Lie.UniversalEnveloping -import Mathlib.Algebra.FreeNonUnitalNonAssocAlgebra +import Mathlib.GroupTheory.GroupAction.Ring #align_import algebra.lie.free from "leanprover-community/mathlib"@"841ac1a3d9162bf51c6327812ecb6e5e71883ac4" diff --git a/Mathlib/Algebra/Lie/Killing.lean b/Mathlib/Algebra/Lie/Killing.lean index b735f497dc472..e1fbb04f34613 100644 --- a/Mathlib/Algebra/Lie/Killing.lean +++ b/Mathlib/Algebra/Lie/Killing.lean @@ -473,10 +473,13 @@ end LieAlgebra section Field open LieModule FiniteDimensional -open Submodule (span) +open Submodule (span subset_span) -lemma LieModule.traceForm_eq_sum_finrank_nsmul_mul [LieAlgebra.IsNilpotent K L] - [LinearWeights K L M] [IsTriangularizable K L M] (x y : L) : +namespace LieModule + +variable [LieAlgebra.IsNilpotent K L] [LinearWeights K L M] [IsTriangularizable K L M] + +lemma traceForm_eq_sum_finrank_nsmul_mul (x y : L) : traceForm K L M x y = ∑ χ in weight K L M, finrank K (weightSpace M χ) • (χ x * χ y) := by have hxy : ∀ χ : L → K, MapsTo (toEndomorphism K L M x ∘ₗ toEndomorphism K L M y) (weightSpace M χ) (weightSpace M χ) := @@ -492,26 +495,24 @@ lemma LieModule.traceForm_eq_sum_finrank_nsmul_mul [LieAlgebra.IsNilpotent K L] LinearMap.trace_eq_sum_trace_restrict' hds hfin hxy] exact Finset.sum_congr (by simp) (fun χ _ ↦ traceForm_weightSpace_eq K L M χ x y) +lemma traceForm_eq_sum_finrank_nsmul : + traceForm K L M = ∑ χ : weight K L M, finrank K (weightSpace M (χ : L → K)) • + (weight.toLinear K L M χ).smulRight (weight.toLinear K L M χ) := by + ext + rw [traceForm_eq_sum_finrank_nsmul_mul, ← Finset.sum_attach] + simp + -- The reverse inclusion should also hold: TODO prove this! -lemma LieModule.dualAnnihilator_ker_traceForm_le_span_weight [LieAlgebra.IsNilpotent K L] - [LinearWeights K L M] [IsTriangularizable K L M] [FiniteDimensional K L] : - (LinearMap.ker (traceForm K L M)).dualAnnihilator ≤ span K (range (weight.toLinear K L M)) := by - intro g hg - simp only [Submodule.mem_dualAnnihilator, LinearMap.mem_ker] at hg - by_contra contra - obtain ⟨f : Module.Dual K (Module.Dual K L), hf, hf'⟩ := - Submodule.exists_dual_map_eq_bot_of_nmem contra inferInstance - let x : L := (Module.evalEquiv K L).symm f - replace hf' : ∀ χ ∈ weight K L M, χ x = 0 := by - intro χ hχ - change weight.toLinear K L M ⟨χ, hχ⟩ x = 0 - rw [Module.apply_evalEquiv_symm_apply, ← Submodule.mem_bot (R := K), ← hf', Submodule.mem_map] - exact ⟨weight.toLinear K L M ⟨χ, hχ⟩, Submodule.subset_span (mem_range_self _), rfl⟩ - have hx : g x ≠ 0 := by simpa - refine hx (hg _ ?_) - ext y - rw [LieModule.traceForm_eq_sum_finrank_nsmul_mul, LinearMap.zero_apply] - exact Finset.sum_eq_zero fun χ hχ ↦ by simp [hf' χ hχ] +lemma range_traceForm_le_span_weight : + LinearMap.range (traceForm K L M) ≤ span K (range (weight.toLinear K L M)) := by + rintro - ⟨x, rfl⟩ + rw [LieModule.traceForm_eq_sum_finrank_nsmul, LinearMap.coeFn_sum, Finset.sum_apply] + refine Submodule.sum_mem _ fun χ _ ↦ ?_ + simp_rw [LinearMap.smul_apply, LinearMap.coe_smulRight, weight.toLinear_apply, + nsmul_eq_smul_cast (R := K)] + exact Submodule.smul_mem _ _ <| Submodule.smul_mem _ _ <| subset_span <| mem_range_self χ + +end LieModule /-- Given a splitting Cartan subalgebra `H` of a finite-dimensional Lie algebra with non-singular Killing form, the corresponding roots span the dual space of `H`. -/ @@ -519,6 +520,8 @@ Killing form, the corresponding roots span the dual space of `H`. -/ lemma LieAlgebra.IsKilling.span_weight_eq_top [FiniteDimensional K L] [IsKilling K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] [IsTriangularizable K H L] : span K (range (weight.toLinear K H L)) = ⊤ := by - simpa using LieModule.dualAnnihilator_ker_traceForm_le_span_weight K H L + refine eq_top_iff.mpr (le_trans ?_ (LieModule.range_traceForm_le_span_weight K H L)) + rw [← traceForm_flip K H L, ← LinearMap.dualAnnihilator_ker_eq_range_flip, + ker_traceForm_eq_bot_of_isCartanSubalgebra, Submodule.dualAnnihilator_bot] end Field diff --git a/Mathlib/Algebra/QuaternionBasis.lean b/Mathlib/Algebra/QuaternionBasis.lean index d1509010654ed..082d1e7a57343 100644 --- a/Mathlib/Algebra/QuaternionBasis.lean +++ b/Mathlib/Algebra/QuaternionBasis.lean @@ -180,4 +180,25 @@ def lift : Basis A c₁ c₂ ≃ (ℍ[R,c₁,c₂] →ₐ[R] A) where congr <;> simp #align quaternion_algebra.lift QuaternionAlgebra.lift +/-- Two `R`-algebra morphisms from a quaternion algebra are equal if they agree on `i` and `j`. -/ +@[ext] +theorem hom_ext ⦃f g : ℍ[R,c₁,c₂] →ₐ[R] A⦄ + (hi : f (Basis.self R).i = g (Basis.self R).i) (hj : f (Basis.self R).j = g (Basis.self R).j) : + f = g := + lift.symm.injective <| Basis.ext hi hj + end QuaternionAlgebra + +namespace Quaternion +variable {R A : Type*} [CommRing R] [Ring A] [Algebra R A] + +open QuaternionAlgebra (Basis) + +/-- Two `R`-algebra morphisms from the quaternions are equal if they agree on `i` and `j`. -/ +@[ext] +theorem hom_ext ⦃f g : ℍ[R] →ₐ[R] A⦄ + (hi : f (Basis.self R).i = g (Basis.self R).i) (hj : f (Basis.self R).j = g (Basis.self R).j) : + f = g := + QuaternionAlgebra.hom_ext hi hj + +end Quaternion diff --git a/Mathlib/Algebra/Regular/Basic.lean b/Mathlib/Algebra/Regular/Basic.lean index 56ec13a6f3950..1d72eeaac3c6e 100644 --- a/Mathlib/Algebra/Regular/Basic.lean +++ b/Mathlib/Algebra/Regular/Basic.lean @@ -88,6 +88,15 @@ theorem IsLeftRegular.right_of_commute {a : R} fun x y xy => h <| (ca x).trans <| xy.trans <| (ca y).symm #align is_left_regular.right_of_commute IsLeftRegular.right_of_commute +theorem IsRightRegular.left_of_commute {a : R} + (ca : ∀ b, Commute a b) (h : IsRightRegular a) : IsLeftRegular a := by + simp_rw [@Commute.symm_iff R _ a] at ca + exact fun x y xy => h <| (ca x).trans <| xy.trans <| (ca y).symm + +theorem Commute.isRightRegular_iff {a : R} (ca : ∀ b, Commute a b) : + IsRightRegular a ↔ IsLeftRegular a := + ⟨IsRightRegular.left_of_commute ca, IsLeftRegular.right_of_commute ca⟩ + theorem Commute.isRegular_iff {a : R} (ca : ∀ b, Commute a b) : IsRegular a ↔ IsLeftRegular a := ⟨fun h => h.left, fun h => ⟨h, h.right_of_commute ca⟩⟩ #align commute.is_regular_iff Commute.isRegular_iff diff --git a/Mathlib/Algebra/Ring/Basic.lean b/Mathlib/Algebra/Ring/Basic.lean index bfd8bfba3da46..42bf56eebf1bb 100644 --- a/Mathlib/Algebra/Ring/Basic.lean +++ b/Mathlib/Algebra/Ring/Basic.lean @@ -188,6 +188,11 @@ instance (priority := 100) NoZeroDivisors.to_isCancelMulZero [Ring α] [NoZeroDi exact sub_eq_zero.1 ((eq_zero_or_eq_zero_of_mul_eq_zero h).resolve_right hb) } #align no_zero_divisors.to_is_cancel_mul_zero NoZeroDivisors.to_isCancelMulZero +/-- In a ring, `IsCancelMulZero` and `NoZeroDivisors` are equivalent. -/ +lemma isCancelMulZero_iff_noZeroDivisors [Ring α] : + IsCancelMulZero α ↔ NoZeroDivisors α := + ⟨fun _ => IsRightCancelMulZero.to_noZeroDivisors _, fun _ => inferInstance⟩ + lemma NoZeroDivisors.to_isDomain [Ring α] [h : Nontrivial α] [NoZeroDivisors α] : IsDomain α := { NoZeroDivisors.to_isCancelMulZero α, h with .. } @@ -198,4 +203,29 @@ instance (priority := 100) IsDomain.to_noZeroDivisors [Ring α] [IsDomain α] : IsRightCancelMulZero.to_noZeroDivisors α #align is_domain.to_no_zero_divisors IsDomain.to_noZeroDivisors +instance Subsingleton.to_isCancelMulZero [Mul α] [Zero α] [Subsingleton α] : IsCancelMulZero α where + mul_right_cancel_of_ne_zero hb := (hb <| Subsingleton.eq_zero _).elim + mul_left_cancel_of_ne_zero hb := (hb <| Subsingleton.eq_zero _).elim + +instance Subsingleton.to_noZeroDivisors [Mul α] [Zero α] [Subsingleton α] : NoZeroDivisors α where + eq_zero_or_eq_zero_of_mul_eq_zero _ := .inl (Subsingleton.eq_zero _) + +lemma isDomain_iff_cancelMulZero_and_nontrivial [Semiring α] : + IsDomain α ↔ IsCancelMulZero α ∧ Nontrivial α := + ⟨fun _ => ⟨inferInstance, inferInstance⟩, fun ⟨_, _⟩ => {}⟩ + +lemma isCancelMulZero_iff_isDomain_or_subsingleton [Semiring α] : + IsCancelMulZero α ↔ IsDomain α ∨ Subsingleton α := by + refine ⟨fun t ↦ ?_, fun h ↦ h.elim (fun _ ↦ inferInstance) (fun _ ↦ inferInstance)⟩ + rw [or_iff_not_imp_right, not_subsingleton_iff_nontrivial] + exact fun _ ↦ {} + +lemma isDomain_iff_noZeroDivisors_and_nontrivial [Ring α] : + IsDomain α ↔ NoZeroDivisors α ∧ Nontrivial α := by + rw [← isCancelMulZero_iff_noZeroDivisors, isDomain_iff_cancelMulZero_and_nontrivial] + +lemma noZeroDivisors_iff_isDomain_or_subsingleton [Ring α] : + NoZeroDivisors α ↔ IsDomain α ∨ Subsingleton α := by + rw [← isCancelMulZero_iff_noZeroDivisors, isCancelMulZero_iff_isDomain_or_subsingleton] + end NoZeroDivisors diff --git a/Mathlib/Algebra/Ring/CentroidHom.lean b/Mathlib/Algebra/Ring/CentroidHom.lean index 6000aaaefccb1..5fe0f91ff3ab4 100644 --- a/Mathlib/Algebra/Ring/CentroidHom.lean +++ b/Mathlib/Algebra/Ring/CentroidHom.lean @@ -5,6 +5,7 @@ Authors: Yaël Dillies, Christopher Hoskin -/ import Mathlib.Algebra.Algebra.Basic import Mathlib.Algebra.Module.Hom +import Mathlib.GroupTheory.GroupAction.Ring import Mathlib.RingTheory.NonUnitalSubsemiring.Basic import Mathlib.RingTheory.Subsemiring.Basic diff --git a/Mathlib/Algebra/Ring/Divisibility/Lemmas.lean b/Mathlib/Algebra/Ring/Divisibility/Lemmas.lean index c5bb9b1c9172d..65559b3b984b2 100644 --- a/Mathlib/Algebra/Ring/Divisibility/Lemmas.lean +++ b/Mathlib/Algebra/Ring/Divisibility/Lemmas.lean @@ -5,6 +5,7 @@ Authors: Oliver Nash -/ import Mathlib.Algebra.Ring.Divisibility.Basic import Mathlib.Data.Nat.Choose.Sum +import Mathlib.GroupTheory.GroupAction.Ring /-! # Lemmas about divisibility in rings diff --git a/Mathlib/Analysis/NormedSpace/OperatorNorm.lean b/Mathlib/Analysis/NormedSpace/OperatorNorm.lean index 8a2d176302e92..72eae739234a7 100644 --- a/Mathlib/Analysis/NormedSpace/OperatorNorm.lean +++ b/Mathlib/Analysis/NormedSpace/OperatorNorm.lean @@ -370,7 +370,7 @@ theorem op_nnnorm_le_of_lipschitz {f : E →SL[σ₁₂] F} {K : ℝ≥0} (hf : op_norm_le_of_lipschitz hf #align continuous_linear_map.op_nnnorm_le_of_lipschitz ContinuousLinearMap.op_nnnorm_le_of_lipschitz -theorem op_nnnorm_eq_of_bounds {φ : E →SL[σ₁₂] F} (M : ℝ≥0) (h_above : ∀ x, ‖φ x‖ ≤ M * ‖x‖) +theorem op_nnnorm_eq_of_bounds {φ : E →SL[σ₁₂] F} (M : ℝ≥0) (h_above : ∀ x, ‖φ x‖₊ ≤ M * ‖x‖₊) (h_below : ∀ N, (∀ x, ‖φ x‖₊ ≤ N * ‖x‖₊) → M ≤ N) : ‖φ‖₊ = M := Subtype.ext <| op_norm_eq_of_bounds (zero_le M) h_above <| Subtype.forall'.mpr h_below #align continuous_linear_map.op_nnnorm_eq_of_bounds ContinuousLinearMap.op_nnnorm_eq_of_bounds diff --git a/Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean b/Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean index e000d4540f824..7a72ab6af7875 100644 --- a/Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean +++ b/Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean @@ -389,6 +389,33 @@ theorem Gamma_conj (s : ℂ) : Gamma (conj s) = conj (Gamma s) := by rw [RingHom.map_add, RingHom.map_one] #align complex.Gamma_conj Complex.Gamma_conj +/-- Expresses the integral over `Ioi 0` of `t ^ (a - 1) * exp (-(r * t))` in terms of the Gamma +function, for complex `a`. -/ +lemma integral_cpow_mul_exp_neg_mul_Ioi {a : ℂ} {r : ℝ} (ha : 0 < a.re) (hr : 0 < r) : + ∫ (t : ℝ) in Ioi 0, t ^ (a - 1) * exp (-(r * t)) = (1 / r) ^ a * Gamma a := by + have aux : (1 / r : ℂ) ^ a = 1 / r * (1 / r) ^ (a - 1) := by + nth_rewrite 2 [← cpow_one (1 / r : ℂ)] + rw [← cpow_add _ _ (one_div_ne_zero <| ofReal_ne_zero.mpr hr.ne'), add_sub_cancel'_right] + calc + _ = ∫ (t : ℝ) in Ioi 0, (1 / r) ^ (a - 1) * (r * t) ^ (a - 1) * exp (-(r * t)) := by + refine MeasureTheory.set_integral_congr measurableSet_Ioi (fun x (hx : 0 < x) ↦ ?_) + rw [mul_cpow_ofReal_nonneg hr.le hx.le, ← mul_assoc, one_div, ← ofReal_inv, + ← mul_cpow_ofReal_nonneg (inv_pos.mpr hr).le hr.le, ← ofReal_mul r⁻¹, inv_mul_cancel hr.ne', + ofReal_one, one_cpow, one_mul] + _ = |1 / r| * ∫ (t : ℝ) in Ioi (r * 0), (1 / r) ^ (a - 1) * t ^ (a - 1) * exp (-t) := by + simp_rw [← ofReal_mul] + rw [integral_comp_mul_left_Ioi (fun x ↦ _ * x ^ (a - 1) * exp (-x)) _ hr, mul_zero, + real_smul, ← one_div] + _ = 1 / r * ∫ (t : ℝ) in Ioi 0, (1 / r) ^ (a - 1) * t ^ (a - 1) * exp (-t) := by + rw [congr_arg Ioi (mul_zero r), _root_.abs_of_nonneg (one_div_pos.mpr hr).le, ofReal_div, + ofReal_one] + _ = 1 / r * (1 / r : ℂ) ^ (a - 1) * (∫ (t : ℝ) in Ioi 0, t ^ (a - 1) * exp (-t)) := by + simp_rw [← integral_mul_left, mul_assoc] + _ = (1 / r) ^ a * Gamma a := by + rw [aux, Gamma_eq_integral ha] + congr 2 with x + rw [ofReal_exp, ofReal_neg, mul_comm] + end GammaDef /-! Now check that the `Γ` function is differentiable, wherever this makes sense. -/ @@ -554,6 +581,18 @@ theorem Gamma_nonneg_of_nonneg {s : ℝ} (hs : 0 ≤ s) : 0 ≤ Gamma s := by · rw [Gamma_zero] · exact (Gamma_pos_of_pos h).le +open Complex in +/-- Expresses the integral over `Ioi 0` of `t ^ (a - 1) * exp (-(r * t))`, for positive real `r`, +in terms of the Gamma function. -/ +lemma integral_rpow_mul_exp_neg_mul_Ioi {a r : ℝ} (ha : 0 < a) (hr : 0 < r) : + ∫ t : ℝ in Ioi 0, t ^ (a - 1) * exp (-(r * t)) = (1 / r) ^ a * Gamma a := by + rw [← ofReal_inj, ofReal_mul, ← Gamma_ofReal, ofReal_cpow (by positivity), ofReal_div] + convert integral_cpow_mul_exp_neg_mul_Ioi (by rwa [ofReal_re] : 0 < (a : ℂ).re) hr + refine _root_.integral_ofReal.symm.trans <| set_integral_congr measurableSet_Ioi (fun t ht ↦ ?_) + norm_cast + rw [← ofReal_cpow (le_of_lt ht), IsROrC.ofReal_mul] + rfl + open Lean.Meta Qq in /-- The `positivity` extension which identifies expressions of the form `Gamma a`. -/ @[positivity Gamma (_ : ℝ)] diff --git a/Mathlib/Data/Countable/Basic.lean b/Mathlib/Data/Countable/Basic.lean index 314c39a308ab5..3c8c3f02ba7b5 100644 --- a/Mathlib/Data/Countable/Basic.lean +++ b/Mathlib/Data/Countable/Basic.lean @@ -35,6 +35,9 @@ theorem countable_iff_nonempty_embedding : Countable α ↔ Nonempty (α ↪ ℕ ⟨fun ⟨⟨f, hf⟩⟩ => ⟨⟨f, hf⟩⟩, fun ⟨f⟩ => ⟨⟨f, f.2⟩⟩⟩ #align countable_iff_nonempty_embedding countable_iff_nonempty_embedding +theorem uncountable_iff_isEmpty_embedding : Uncountable α ↔ IsEmpty (α ↪ ℕ) := by + rw [← not_countable_iff, countable_iff_nonempty_embedding, not_nonempty_iff] + theorem nonempty_embedding_nat (α) [Countable α] : Nonempty (α ↪ ℕ) := countable_iff_nonempty_embedding.1 ‹_› #align nonempty_embedding_nat nonempty_embedding_nat @@ -43,6 +46,9 @@ protected theorem Function.Embedding.countable [Countable β] (f : α ↪ β) : f.injective.countable #align function.embedding.countable Function.Embedding.countable +protected lemma Function.Embedding.uncountable [Uncountable α] (f : α ↪ β) : Uncountable β := + f.injective.uncountable + end Embedding /-! @@ -53,24 +59,51 @@ section type variable {α : Type u} {β : Type v} {π : α → Type w} -instance [Countable α] [Countable β] : Countable (Sum α β) := by +instance [Countable α] [Countable β] : Countable (α ⊕ β) := by rcases exists_injective_nat α with ⟨f, hf⟩ rcases exists_injective_nat β with ⟨g, hg⟩ exact (Equiv.natSumNatEquivNat.injective.comp <| hf.sum_map hg).countable +instance Sum.uncountable_inl [Uncountable α] : Uncountable (α ⊕ β) := + inl_injective.uncountable + +instance Sum.uncountable_inr [Uncountable β] : Uncountable (α ⊕ β) := + inr_injective.uncountable + instance [Countable α] : Countable (Option α) := Countable.of_equiv _ (Equiv.optionEquivSumPUnit.{_, 0} α).symm +instance Option.instUncountable [Uncountable α] : Uncountable (Option α) := + Injective.uncountable fun _ _ ↦ Option.some_inj.1 + instance [Countable α] [Countable β] : Countable (α × β) := by rcases exists_injective_nat α with ⟨f, hf⟩ rcases exists_injective_nat β with ⟨g, hg⟩ exact (Nat.pairEquiv.injective.comp <| hf.Prod_map hg).countable +instance [Uncountable α] [Nonempty β] : Uncountable (α × β) := by + inhabit β + exact (Prod.mk.inj_right default).uncountable + +instance [Nonempty α] [Uncountable β] : Uncountable (α × β) := by + inhabit α + exact (Prod.mk.inj_left default).uncountable + instance [Countable α] [∀ a, Countable (π a)] : Countable (Sigma π) := by rcases exists_injective_nat α with ⟨f, hf⟩ choose g hg using fun a => exists_injective_nat (π a) exact ((Equiv.sigmaEquivProd ℕ ℕ).injective.comp <| hf.sigma_map hg).countable +lemma Sigma.uncountable (a : α) [Uncountable (π a)] : Uncountable (Sigma π) := + (sigma_mk_injective (i := a)).uncountable + +instance [Nonempty α] [∀ a, Uncountable (π a)] : Uncountable (Sigma π) := by + inhabit α; exact Sigma.uncountable default + +instance (priority := 500) SetCoe.countable [Countable α] (s : Set α) : Countable s := + Subtype.countable +#align set_coe.countable SetCoe.countable + end type section sort @@ -81,12 +114,8 @@ variable {α : Sort u} {β : Sort v} {π : α → Sort w} ### Operations on `Sort*`s -/ -instance (priority := 500) SetCoe.countable {α} [Countable α] (s : Set α) : Countable s := - Subtype.countable -#align set_coe.countable SetCoe.countable - -instance [Countable α] [Countable β] : Countable (PSum α β) := - Countable.of_equiv (Sum (PLift α) (PLift β)) (Equiv.plift.sumPSum Equiv.plift) +instance [Countable α] [Countable β] : Countable (α ⊕' β) := + Countable.of_equiv (PLift α ⊕ PLift β) (Equiv.plift.sumPSum Equiv.plift) instance [Countable α] [Countable β] : Countable (PProd α β) := Countable.of_equiv (PLift α × PLift β) (Equiv.plift.prodPProd Equiv.plift) diff --git a/Mathlib/Data/Countable/Defs.lean b/Mathlib/Data/Countable/Defs.lean index 78b60d323f3fc..7bec5e9fd701d 100644 --- a/Mathlib/Data/Countable/Defs.lean +++ b/Mathlib/Data/Countable/Defs.lean @@ -10,15 +10,17 @@ import Mathlib.Tactic.Common #align_import data.countable.defs from "leanprover-community/mathlib"@"70d50ecfd4900dd6d328da39ab7ebd516abe4025" /-! -# Countable types +# Countable and uncountable types -In this file we define a typeclass saying that a given `Sort*` is countable. See also `Encodable` -for a version that singles out a specific encoding of elements of `α` by natural numbers. +In this file we define a typeclass `Countable` saying that a given `Sort*` is countable +and a typeclass `Uncountable` saying that a given `Type*` is uncountable. -This file also provides a few instances of this typeclass. More instances can be found in other -files. --/ +See also `Encodable` for a version that singles out +a specific encoding of elements of `α` by natural numbers. +This file also provides a few instances of these typeclasses. +More instances can be found in other files. +-/ open Function @@ -117,3 +119,57 @@ instance (priority := 500) Quotient.countable [Countable α] {r : α → α → instance (priority := 500) [Countable α] {s : Setoid α} : Countable (Quotient s) := (inferInstance : Countable (@Quot α _)) + +/-! +### Uncountable types +-/ + +/-- A type `α` is uncountable if it is not countable. -/ +@[mk_iff uncountable_iff_not_countable] +class Uncountable (α : Sort*) : Prop where + /-- A type `α` is uncountable if it is not countable. -/ + not_countable : ¬Countable α + +lemma not_uncountable_iff : ¬Uncountable α ↔ Countable α := by + rw [uncountable_iff_not_countable, not_not] + +lemma not_countable_iff : ¬Countable α ↔ Uncountable α := (uncountable_iff_not_countable α).symm + +@[simp] +lemma not_uncountable [Countable α] : ¬Uncountable α := not_uncountable_iff.2 ‹_› + +@[simp] +lemma not_countable [Uncountable α] : ¬Countable α := Uncountable.not_countable + +protected theorem Function.Injective.uncountable [Uncountable α] {f : α → β} (hf : Injective f) : + Uncountable β := + ⟨fun _ ↦ not_countable hf.countable⟩ + +protected theorem Function.Surjective.uncountable [Uncountable β] {f : α → β} (hf : Surjective f) : + Uncountable α := (injective_surjInv hf).uncountable + +lemma not_injective_uncountable_countable [Uncountable α] [Countable β] (f : α → β) : + ¬Injective f := fun hf ↦ not_countable hf.countable + +lemma not_surjective_countable_uncountable [Countable α] [Uncountable β] (f : α → β) : + ¬Surjective f := fun hf ↦ + not_countable hf.countable + +theorem uncountable_iff_forall_not_surjective [Nonempty α] : + Uncountable α ↔ ∀ f : ℕ → α, ¬Surjective f := by + rw [← not_countable_iff, countable_iff_exists_surjective, not_exists] + +theorem Uncountable.of_equiv (α : Sort*) [Uncountable α] (e : α ≃ β) : Uncountable β := + e.injective.uncountable + +theorem Equiv.uncountable_iff (e : α ≃ β) : Uncountable α ↔ Uncountable β := + ⟨fun h => @Uncountable.of_equiv _ _ h e, fun h => @Uncountable.of_equiv _ _ h e.symm⟩ + +instance {β : Type v} [Uncountable β] : Uncountable (ULift.{u} β) := + .of_equiv _ Equiv.ulift.symm + +instance [Uncountable α] : Uncountable (PLift α) := + .of_equiv _ Equiv.plift.symm + +instance (priority := 100) [Uncountable α] : Infinite α := + ⟨fun _ ↦ not_countable (α := α) inferInstance⟩ diff --git a/Mathlib/Data/Int/Basic.lean b/Mathlib/Data/Int/Basic.lean index be0dd2169bc10..d608336210a56 100644 --- a/Mathlib/Data/Int/Basic.lean +++ b/Mathlib/Data/Int/Basic.lean @@ -88,11 +88,6 @@ lemma natAbs_cast (n : ℕ) : natAbs ↑n = n := rfl @[norm_cast] protected lemma coe_nat_sub {n m : ℕ} : n ≤ m → (↑(m - n) : ℤ) = ↑m - ↑n := ofNat_sub -@[to_additive (attr := simp, norm_cast) coe_nat_zsmul] -theorem _root_.zpow_coe_nat [DivInvMonoid G] (a : G) (n : ℕ) : a ^ (Nat.cast n : ℤ) = a ^ n := - zpow_ofNat .. -#align coe_nat_zsmul coe_nat_zsmul - /-! ### Extra instances to short-circuit type class resolution These also prevent non-computable instances like `Int.normedCommRing` being used to construct diff --git a/Mathlib/Data/Nat/Choose/Sum.lean b/Mathlib/Data/Nat/Choose/Sum.lean index 4fc5443a4c328..061ac12398ff5 100644 --- a/Mathlib/Data/Nat/Choose/Sum.lean +++ b/Mathlib/Data/Nat/Choose/Sum.lean @@ -132,6 +132,14 @@ theorem four_pow_le_two_mul_add_one_mul_central_binom (n : ℕ) : _ = (2 * n + 1) * choose (2 * n) n := by simp #align nat.four_pow_le_two_mul_add_one_mul_central_binom Nat.four_pow_le_two_mul_add_one_mul_central_binom +/-- **Zhu Shijie's identity** aka hockey-stick identity. -/ +theorem sum_Icc_choose (n k : ℕ) : ∑ m in Icc k n, m.choose k = (n + 1).choose (k + 1) := by + cases' le_or_gt k n with h h + · induction' n, h using le_induction with n _ ih; · simp + rw [← Ico_insert_right (by linarith), sum_insert (by simp), + show Ico k (n + 1) = Icc k n by rfl, ih, choose_succ_succ' (n + 1)] + · rw [choose_eq_zero_of_lt (by linarith), Icc_eq_empty_of_lt h, sum_empty] + end Nat theorem Int.alternating_sum_range_choose {n : ℕ} : diff --git a/Mathlib/Data/Real/CauSeq.lean b/Mathlib/Data/Real/CauSeq.lean index 6af31e21f5021..956f052341e18 100644 --- a/Mathlib/Data/Real/CauSeq.lean +++ b/Mathlib/Data/Real/CauSeq.lean @@ -9,6 +9,7 @@ import Mathlib.Algebra.Order.Group.MinMax import Mathlib.Algebra.Order.Field.Basic import Mathlib.Algebra.Ring.Pi import Mathlib.GroupTheory.GroupAction.Pi +import Mathlib.GroupTheory.GroupAction.Ring import Mathlib.Init.Align import Mathlib.Tactic.GCongr import Mathlib.Tactic.Ring diff --git a/Mathlib/Geometry/Manifold/ChartedSpace.lean b/Mathlib/Geometry/Manifold/ChartedSpace.lean index e519a641f3a3e..2ad848a4620ec 100644 --- a/Mathlib/Geometry/Manifold/ChartedSpace.lean +++ b/Mathlib/Geometry/Manifold/ChartedSpace.lean @@ -1030,7 +1030,7 @@ theorem StructureGroupoid.compatible_of_mem_maximalAtlas {e e' : PartialHomeomor have D : (e.symm ≫ₕ f) ≫ₕ f.symm ≫ₕ e' ≈ (e.symm ≫ₕ e').restr s := calc (e.symm ≫ₕ f) ≫ₕ f.symm ≫ₕ e' = e.symm ≫ₕ (f ≫ₕ f.symm) ≫ₕ e' := by simp only [trans_assoc] _ ≈ e.symm ≫ₕ ofSet f.source f.open_source ≫ₕ e' := - EqOnSource.trans' (refl _) (EqOnSource.trans' (trans_self_symm _) (refl _)) + EqOnSource.trans' (refl _) (EqOnSource.trans' (self_trans_symm _) (refl _)) _ ≈ (e.symm ≫ₕ ofSet f.source f.open_source) ≫ₕ e' := by rw [trans_assoc] _ ≈ e.symm.restr s ≫ₕ e' := by rw [trans_of_set']; apply refl _ ≈ (e.symm ≫ₕ e').restr s := by rw [restr_trans] @@ -1098,7 +1098,7 @@ theorem singleton_hasGroupoid (h : e.source = Set.univ) (G : StructureGroupoid H intro e' e'' he' he'' rw [e.singletonChartedSpace_mem_atlas_eq h e' he', e.singletonChartedSpace_mem_atlas_eq h e'' he''] - refine' G.eq_on_source _ e.trans_symm_self + refine' G.eq_on_source _ e.symm_trans_self have hle : idRestrGroupoid ≤ G := (closedUnderRestriction_iff_id_le G).mp (by assumption) exact StructureGroupoid.le_iff.mp hle _ (idRestrGroupoid_mem _) } #align local_homeomorph.singleton_has_groupoid PartialHomeomorph.singleton_hasGroupoid @@ -1262,7 +1262,7 @@ def Structomorph.trans (e : Structomorph G M M') (e' : Structomorph G M' M'') : F₁ ≈ c.symm ≫ₕ f₁ ≫ₕ (g ≫ₕ g.symm) ≫ₕ f₂ ≫ₕ c' := by simp only [trans_assoc, _root_.refl] _ ≈ c.symm ≫ₕ f₁ ≫ₕ ofSet g.source g.open_source ≫ₕ f₂ ≫ₕ c' := EqOnSource.trans' (_root_.refl _) (EqOnSource.trans' (_root_.refl _) - (EqOnSource.trans' (trans_self_symm g) (_root_.refl _))) + (EqOnSource.trans' (self_trans_symm g) (_root_.refl _))) _ ≈ ((c.symm ≫ₕ f₁) ≫ₕ ofSet g.source g.open_source) ≫ₕ f₂ ≫ₕ c' := by simp only [trans_assoc, _root_.refl] _ ≈ (c.symm ≫ₕ f₁).restr s ≫ₕ f₂ ≫ₕ c' := by rw [trans_of_set'] diff --git a/Mathlib/Geometry/Manifold/Diffeomorph.lean b/Mathlib/Geometry/Manifold/Diffeomorph.lean index 38875a608ffa6..995a04d616bf6 100644 --- a/Mathlib/Geometry/Manifold/Diffeomorph.lean +++ b/Mathlib/Geometry/Manifold/Diffeomorph.lean @@ -195,6 +195,7 @@ theorem coe_refl : ⇑(Diffeomorph.refl I M n) = id := end /-- Composition of two diffeomorphisms. -/ +@[trans] protected def trans (h₁ : M ≃ₘ^n⟮I, I'⟯ M') (h₂ : M' ≃ₘ^n⟮I', J⟯ N) : M ≃ₘ^n⟮I, J⟯ N where contMDiff_toFun := h₂.contMDiff.comp h₁.contMDiff contMDiff_invFun := h₁.contMDiff_invFun.comp h₂.contMDiff_invFun @@ -217,7 +218,7 @@ theorem coe_trans (h₁ : M ≃ₘ^n⟮I, I'⟯ M') (h₂ : M' ≃ₘ^n⟮I', J #align diffeomorph.coe_trans Diffeomorph.coe_trans /-- Inverse of a diffeomorphism. -/ -@[pp_dot] +@[symm] protected def symm (h : M ≃ₘ^n⟮I, J⟯ N) : N ≃ₘ^n⟮J, I⟯ M where contMDiff_toFun := h.contMDiff_invFun contMDiff_invFun := h.contMDiff_toFun diff --git a/Mathlib/Geometry/Manifold/InteriorBoundary.lean b/Mathlib/Geometry/Manifold/InteriorBoundary.lean index e8f1d22de97be..970413b2edd42 100644 --- a/Mathlib/Geometry/Manifold/InteriorBoundary.lean +++ b/Mathlib/Geometry/Manifold/InteriorBoundary.lean @@ -103,25 +103,42 @@ lemma _root_.range_mem_nhds_isInteriorPoint {x : M} (h : I.IsInteriorPoint x) : rw [mem_nhds_iff] exact ⟨interior (range I), interior_subset, isOpen_interior, h⟩ -section boundaryless +/-- Type class for manifold without boundary. This differs from `ModelWithCorners.Boundaryless`, + which states that the `ModelWithCorners` maps to the whole model vector space. -/ +class _root_.BoundarylessManifold {𝕜 : Type*} [NontriviallyNormedField 𝕜] + {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] + {H : Type*} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) + (M : Type*) [TopologicalSpace M] [ChartedSpace H M] : Prop where + isInteriorPoint' : ∀ x : M, IsInteriorPoint I x + +section Boundaryless variable [I.Boundaryless] -/-- If `I` is boundaryless, every point of `M` is an interior point. -/ -lemma isInteriorPoint {x : M} : I.IsInteriorPoint x := by - let r := ((chartAt H x).isOpen_extend_target I).interior_eq - have : extChartAt I x = (chartAt H x).extend I := rfl - rw [← this] at r - rw [ModelWithCorners.isInteriorPoint_iff, r] - exact PartialEquiv.map_source _ (mem_extChartAt_source _ _) +/-- Boundaryless `ModelWithCorners` implies boundaryless manifold. -/ +instance : BoundarylessManifold I M where + isInteriorPoint' x := by + let r := ((chartAt H x).isOpen_extend_target I).interior_eq + have : extChartAt I x = (chartAt H x).extend I := rfl + rw [← this] at r + rw [ModelWithCorners.isInteriorPoint_iff, r] + exact PartialEquiv.map_source _ (mem_extChartAt_source _ _) -/-- If `I` is boundaryless, `M` has full interior. -/ +end Boundaryless + +section BoundarylessManifold +variable [BoundarylessManifold I M] + +lemma _root_.BoundarylessManifold.isInteriorPoint {x : M} : + IsInteriorPoint I x := BoundarylessManifold.isInteriorPoint' x + +/-- Boundaryless manifolds have full interior. -/ lemma interior_eq_univ : I.interior M = univ := by ext - refine ⟨fun _ ↦ trivial, fun _ ↦ I.isInteriorPoint⟩ + refine ⟨fun _ ↦ trivial, fun _ ↦ BoundarylessManifold.isInteriorPoint I⟩ -/-- If `I` is boundaryless, `M` has empty boundary. -/ +/-- Boundaryless manifolds have empty boundary. -/ lemma Boundaryless.boundary_eq_empty : I.boundary M = ∅ := by rw [I.boundary_eq_complement_interior, I.interior_eq_univ, compl_empty_iff] -end boundaryless +end BoundarylessManifold end ModelWithCorners diff --git a/Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean b/Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean index 7612e907c11ae..be615f8a99e15 100644 --- a/Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean +++ b/Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean @@ -478,7 +478,9 @@ end ModelWithCornersProd section Boundaryless -/-- Property ensuring that the model with corners `I` defines manifolds without boundary. -/ +/-- Property ensuring that the model with corners `I` defines manifolds without boundary. This + differs from the more general `BoundarylessManifold`, which requires every point on the manifold + to be an interior point. -/ class ModelWithCorners.Boundaryless {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type*} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) : Prop where @@ -617,7 +619,7 @@ the `C^n` groupoid. -/ theorem symm_trans_mem_contDiffGroupoid (e : PartialHomeomorph M H) : e.symm.trans e ∈ contDiffGroupoid n I := haveI : e.symm.trans e ≈ PartialHomeomorph.ofSet e.target e.open_target := - PartialHomeomorph.trans_symm_self _ + PartialHomeomorph.symm_trans_self _ StructureGroupoid.eq_on_source _ (ofSet_mem_contDiffGroupoid n I e.open_target) this #align symm_trans_mem_cont_diff_groupoid symm_trans_mem_contDiffGroupoid @@ -776,7 +778,7 @@ the analytic groupoid. -/ theorem symm_trans_mem_analyticGroupoid (e : PartialHomeomorph M H) : e.symm.trans e ∈ analyticGroupoid I := haveI : e.symm.trans e ≈ PartialHomeomorph.ofSet e.target e.open_target := - PartialHomeomorph.trans_symm_self _ + PartialHomeomorph.symm_trans_self _ StructureGroupoid.eq_on_source _ (ofSet_mem_analyticGroupoid I e.open_target) this /-- The analytic groupoid is closed under restriction. -/ diff --git a/Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean b/Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean index bce81054d2c41..8df736fa3019c 100644 --- a/Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean +++ b/Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean @@ -124,6 +124,51 @@ theorem tangentBundleCore_coordChange_achart (x x' z : M) : rfl #align tangent_bundle_core_coord_change_achart tangentBundleCore_coordChange_achart +section tangentCoordChange + +/-- In a manifold `M`, given two preferred charts indexed by `x y : M`, `tangentCoordChange I x y` +is the family of derivatives of the corresponding change-of-coordinates map. It takes junk values +outside the intersection of the sources of the two charts. + +Note that this definition takes advantage of the fact that `tangentBundleCore` has the same base +sets as the preferred charts of the base manifold. -/ +abbrev tangentCoordChange (x y : M) : M → E →L[𝕜] E := + (tangentBundleCore I M).coordChange (achart H x) (achart H y) + +variable {I} + +lemma tangentCoordChange_def {x y z : M} : tangentCoordChange I x y z = + fderivWithin 𝕜 (extChartAt I y ∘ (extChartAt I x).symm) (range I) (extChartAt I x z) := rfl + +lemma tangentCoordChange_self {x z : M} {v : E} (h : z ∈ (extChartAt I x).source) : + tangentCoordChange I x x z v = v := by + apply (tangentBundleCore I M).coordChange_self + rw [tangentBundleCore_baseSet, coe_achart, ← extChartAt_source I] + exact h + +lemma tangentCoordChange_comp {w x y z : M} {v : E} + (h : z ∈ (extChartAt I w).source ∩ (extChartAt I x).source ∩ (extChartAt I y).source) : + tangentCoordChange I x y z (tangentCoordChange I w x z v) = tangentCoordChange I w y z v := by + apply (tangentBundleCore I M).coordChange_comp + simp only [tangentBundleCore_baseSet, coe_achart, ← extChartAt_source I] + exact h + +lemma hasFDerivWithinAt_tangentCoordChange {x y z : M} + (h : z ∈ (extChartAt I x).source ∩ (extChartAt I y).source) : + HasFDerivWithinAt ((extChartAt I y) ∘ (extChartAt I x).symm) (tangentCoordChange I x y z) + (range I) (extChartAt I x z) := + have h' : extChartAt I x z ∈ ((extChartAt I x).symm ≫ (extChartAt I y)).source := by + rw [PartialEquiv.trans_source'', PartialEquiv.symm_symm, PartialEquiv.symm_target] + exact mem_image_of_mem _ h + ((contDiffWithinAt_ext_coord_change I y x h').differentiableWithinAt (by simp)).hasFDerivWithinAt + +lemma continuousOn_tangentCoordChange (x y : M) : ContinuousOn (tangentCoordChange I x y) + ((extChartAt I x).source ∩ (extChartAt I y).source) := by + convert (tangentBundleCore I M).continuousOn_coordChange (achart H x) (achart H y) <;> + simp only [tangentBundleCore_baseSet, coe_achart, ← extChartAt_source I] + +end tangentCoordChange + /-- The tangent space at a point of the manifold `M`. It is just `E`. We could use instead `(tangentBundleCore I M).to_topological_vector_bundle_core.fiber x`, but we use `E` to help the kernel. diff --git a/Mathlib/GroupTheory/GroupAction/Ring.lean b/Mathlib/GroupTheory/GroupAction/Ring.lean new file mode 100644 index 0000000000000..c99e4cf635df7 --- /dev/null +++ b/Mathlib/GroupTheory/GroupAction/Ring.lean @@ -0,0 +1,58 @@ +/- +Copyright (c) 2022 Eric Wieser. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Eric Wieser +-/ +import Mathlib.Algebra.Ring.Defs +import Mathlib.GroupTheory.GroupAction.Defs + +/-! +# Commutativity and associativity of action of integers on rings + +This file proves that `ℕ` and `ℤ` act commutatively and associatively on (semi)rings. + +## TODO + +Those instances are in their own file only because they require much less imports than any existing +file they could go to. This is unfortunate and should be fixed by reorganising files. +-/ + +open scoped Int + +variable {α : Type*} + +/-- Note that `AddMonoid.nat_smulCommClass` requires stronger assumptions on `α`. -/ +instance NonUnitalNonAssocSemiring.nat_smulCommClass [NonUnitalNonAssocSemiring α] : + SMulCommClass ℕ α α where + smul_comm n x y := by + induction' n with n ih + · simp [zero_nsmul] + · simp_rw [succ_nsmul, smul_eq_mul, mul_add, ← smul_eq_mul, ih] +#align non_unital_non_assoc_semiring.nat_smul_comm_class NonUnitalNonAssocSemiring.nat_smulCommClass + +/-- Note that `AddCommMonoid.nat_isScalarTower` requires stronger assumptions on `α`. -/ +instance NonUnitalNonAssocSemiring.nat_isScalarTower [NonUnitalNonAssocSemiring α] : + IsScalarTower ℕ α α where + smul_assoc n x y := by + induction' n with n ih + · simp [zero_nsmul] + · simp_rw [succ_nsmul, ← ih, smul_eq_mul, add_mul] +#align non_unital_non_assoc_semiring.nat_is_scalar_tower NonUnitalNonAssocSemiring.nat_isScalarTower + +/-- Note that `AddGroup.int_smulCommClass` requires stronger assumptions on `α`. -/ +instance NonUnitalNonAssocRing.int_smulCommClass [NonUnitalNonAssocRing α] : + SMulCommClass ℤ α α where + smul_comm n x y := + match n with + | (n : ℕ) => by simp_rw [coe_nat_zsmul, smul_comm] + | -[n+1] => by simp_rw [negSucc_zsmul, smul_eq_mul, mul_neg, mul_smul_comm] +#align non_unital_non_assoc_ring.int_smul_comm_class NonUnitalNonAssocRing.int_smulCommClass + +/-- Note that `AddCommGroup.int_isScalarTower` requires stronger assumptions on `α`. -/ +instance NonUnitalNonAssocRing.int_isScalarTower [NonUnitalNonAssocRing α] : + IsScalarTower ℤ α α where + smul_assoc n x y := + match n with + | (n : ℕ) => by simp_rw [coe_nat_zsmul, smul_assoc] + | -[n+1] => by simp_rw [negSucc_zsmul, smul_eq_mul, neg_mul, smul_mul_assoc] +#align non_unital_non_assoc_ring.int_is_scalar_tower NonUnitalNonAssocRing.int_isScalarTower diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean index 278eb81150964..0ddab49db907a 100644 --- a/Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean +++ b/Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean @@ -357,8 +357,7 @@ theorem ofQuaternion_toQuaternion (c : CliffordAlgebra (Q c₁ c₂)) : @[simp] theorem toQuaternion_comp_ofQuaternion : toQuaternion.comp ofQuaternion = AlgHom.id R ℍ[R,c₁,c₂] := by - apply QuaternionAlgebra.lift.symm.injective - ext1 <;> dsimp [QuaternionAlgebra.Basis.lift] <;> simp + ext : 1 <;> simp #align clifford_algebra_quaternion.to_quaternion_comp_of_quaternion CliffordAlgebraQuaternion.toQuaternion_comp_ofQuaternion @[simp] diff --git a/Mathlib/LinearAlgebra/Dual.lean b/Mathlib/LinearAlgebra/Dual.lean index 0753e9517e6c9..b83dcc91a128d 100644 --- a/Mathlib/LinearAlgebra/Dual.lean +++ b/Mathlib/LinearAlgebra/Dual.lean @@ -912,6 +912,7 @@ def dualCoannihilator (Φ : Submodule R (Module.Dual R M)) : Submodule R M := Φ.dualAnnihilator.comap (Module.Dual.eval R M) #align submodule.dual_coannihilator Submodule.dualCoannihilator +@[simp] theorem mem_dualCoannihilator {Φ : Submodule R (Module.Dual R M)} (x : M) : x ∈ Φ.dualCoannihilator ↔ ∀ φ ∈ Φ, (φ x : R) = 0 := by simp_rw [dualCoannihilator, mem_comap, mem_dualAnnihilator, Module.Dual.eval_apply] @@ -1428,6 +1429,15 @@ theorem range_dualMap_eq_dualAnnihilator_ker_of_subtype_range_surjective (f : M exact (ker_rangeRestrict f).symm #align linear_map.range_dual_map_eq_dual_annihilator_ker_of_subtype_range_surjective LinearMap.range_dualMap_eq_dualAnnihilator_ker_of_subtype_range_surjective +theorem ker_dualMap_eq_dualCoannihilator_range (f : M →ₗ[R] M') : + LinearMap.ker f.dualMap = (Dual.eval R M' ∘ₗ f).range.dualCoannihilator := by + ext x; simp [ext_iff (f := dualMap f x)] + +@[simp] +lemma dualCoannihilator_range_eq_ker_flip (B : M →ₗ[R] M' →ₗ[R] R) : + (range B).dualCoannihilator = LinearMap.ker B.flip := by + ext x; simp [ext_iff (f := B.flip x)] + end LinearMap end CommRing @@ -1595,6 +1605,12 @@ theorem dualMap_bijective_iff {f : V₁ →ₗ[K] V₂} : variable {B : V₁ →ₗ[K] V₂ →ₗ[K] K} +@[simp] +lemma dualAnnihilator_ker_eq_range_flip [IsReflexive K V₂] : + (ker B).dualAnnihilator = range B.flip := by + change _ = range (B.dualMap.comp (Module.evalEquiv K V₂).toLinearMap) + rw [← range_dualMap_eq_dualAnnihilator_ker, range_comp_of_range_eq_top _ (LinearEquiv.range _)] + open Function theorem flip_injective_iff₁ [FiniteDimensional K V₁] : Injective B.flip ↔ Surjective B := by diff --git a/Mathlib/Logic/Equiv/PartialEquiv.lean b/Mathlib/Logic/Equiv/PartialEquiv.lean index 39ed99c0b3f3a..c3a0d71e6b55d 100644 --- a/Mathlib/Logic/Equiv/PartialEquiv.lean +++ b/Mathlib/Logic/Equiv/PartialEquiv.lean @@ -148,6 +148,7 @@ instance [Inhabited α] [Inhabited β] : Inhabited (PartialEquiv α β) := eqOn_empty _ _⟩⟩ /-- The inverse of a partial equivalence -/ +@[symm] protected def symm : PartialEquiv β α where toFun := e.invFun invFun := e.toFun @@ -689,6 +690,7 @@ protected def trans' (e' : PartialEquiv β γ) (h : e.target = e'.source) : Part /-- Composing two partial equivs, by restricting to the maximal domain where their composition is well defined. -/ +@[trans] protected def trans : PartialEquiv α γ := PartialEquiv.trans' (e.symm.restr e'.source).symm (e'.restr e.target) (inter_comm _ _) #align local_equiv.trans PartialEquiv.trans @@ -896,18 +898,18 @@ theorem EqOnSource.source_inter_preimage_eq {e e' : PartialEquiv α β} (he : e /-- Composition of a partial equivlance and its inverse is equivalent to the restriction of the identity to the source. -/ -theorem trans_self_symm : e.trans e.symm ≈ ofSet e.source := by +theorem self_trans_symm : e.trans e.symm ≈ ofSet e.source := by have A : (e.trans e.symm).source = e.source := by mfld_set_tac refine' ⟨by rw [A, ofSet_source], fun x hx => _⟩ rw [A] at hx simp only [hx, mfld_simps] -#align local_equiv.trans_self_symm PartialEquiv.trans_self_symm +#align local_equiv.self_trans_symm PartialEquiv.self_trans_symm /-- Composition of the inverse of a partial equivalence and this partial equivalence is equivalent to the restriction of the identity to the target. -/ -theorem trans_symm_self : e.symm.trans e ≈ PartialEquiv.ofSet e.target := - trans_self_symm e.symm -#align local_equiv.trans_symm_self PartialEquiv.trans_symm_self +theorem symm_trans_self : e.symm.trans e ≈ PartialEquiv.ofSet e.target := + self_trans_symm e.symm +#align local_equiv.symm_trans_self PartialEquiv.symm_trans_self /-- Two equivalent partial equivs are equal when the source and target are `univ`. -/ theorem eq_of_eqOnSource_univ (e e' : PartialEquiv α β) (h : e ≈ e') (s : e.source = univ) diff --git a/Mathlib/Probability/Distributions/Exponential.lean b/Mathlib/Probability/Distributions/Exponential.lean index 7f1d7e38afc03..034cb4c4b1d1d 100644 --- a/Mathlib/Probability/Distributions/Exponential.lean +++ b/Mathlib/Probability/Distributions/Exponential.lean @@ -7,6 +7,7 @@ Authors: Claus Clausen, Patrick Massot import Mathlib.Analysis.SpecialFunctions.Gaussian import Mathlib.Probability.Notation import Mathlib.Probability.Cdf +import Mathlib.Probability.Distributions.Gamma /-! # Exponential distributions over ℝ @@ -30,26 +31,9 @@ open scoped ENNReal NNReal Real open MeasureTheory Real Set Filter Topology - /-- A Lebesgue Integral from -∞ to y can be expressed as the sum of one from -∞ to 0 and 0 to x -/ -lemma lintegral_Iic_eq_lintegral_Iio_add_Icc {y z : ℝ} (f : ℝ → ℝ≥0∞) (hzy : z ≤ y) : - ∫⁻ x in Iic y, f x = (∫⁻ x in Iio z, f x) + ∫⁻ x in Icc z y, f x := by - rw [← Iio_union_Icc_eq_Iic hzy, lintegral_union measurableSet_Icc] - rw [Set.disjoint_iff] - rintro x ⟨h1 : x < _, h2, _⟩ - linarith - lemma lintegral_eq_lintegral_Ici_add_Iio (f : ℝ → ℝ≥0∞) (c : ℝ) : ∫⁻ x, f x = (∫⁻ x in Ici c, f x) + ∫⁻ x in Iio c, f x := by - have union : univ = {x : ℝ | x ≥ c} ∪ {x : ℝ | x < c} := by - ext x; simp [le_or_lt] - calc - ∫⁻ x, f x = ∫⁻ x in univ, f x ∂volume := (set_lintegral_univ f).symm - _ = ∫⁻ x in {x | x ≥ c} ∪ {x | x < c} , f x ∂volume := by rw [← union] - _ = _ := by - apply lintegral_union (isOpen_gt' c).measurableSet - rw [Set.disjoint_iff] - rintro x ⟨hxge : x ≥ _, hxlt : x < _⟩ - linarith + rw [← lintegral_add_compl f (measurableSet_Ici (a := c)), compl_Ici] namespace ProbabilityTheory diff --git a/Mathlib/Probability/Distributions/Gamma.lean b/Mathlib/Probability/Distributions/Gamma.lean new file mode 100644 index 0000000000000..8ab6181d25d5b --- /dev/null +++ b/Mathlib/Probability/Distributions/Gamma.lean @@ -0,0 +1,147 @@ +/- +Copyright (c) 2024 Josha Dekker. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Josha Dekker +-/ + +import Mathlib.Analysis.SpecialFunctions.Gaussian +import Mathlib.Probability.Notation +import Mathlib.Probability.Cdf +import Mathlib.Analysis.SpecialFunctions.Gamma.Basic + +/-! # Gamma distributions over ℝ + +Define the Gamma Measure over the Reals + +## Main definitions +* `gammaPdfReal`: the function `a r x ↦ r ^ a / (Gamma a) * x ^ (a-1) * exp (-(r * x))` + for `0 ≤ x` or `0` else, which is the probability density function of a Gamma distribution with + shape `a` and rate `r` (when `ha : 0 < a ` and `hr : 0 < r`). +* `gammaPdf`: `ℝ≥0∞`-valued pdf, + `gammaPdf a r = ENNReal.ofReal (gammaPdfReal a r)`. +* `gammaMeasure`: a Gamma measure on `ℝ`, parametrized by its shape `a` and rate `r`. +* `gammaCdfReal`: the CDF given by the definition of CDF in `ProbabilityTheory.Cdf` applied to the + Gamma measure. +-/ + +open scoped ENNReal NNReal + +open MeasureTheory Real Set Filter Topology + +/-- A Lebesgue Integral from -∞ to y can be expressed as the sum of one from -∞ to 0 and 0 to x -/ +lemma lintegral_Iic_eq_lintegral_Iio_add_Icc {y z : ℝ} (f : ℝ → ℝ≥0∞) (hzy : z ≤ y) : + ∫⁻ x in Iic y, f x = (∫⁻ x in Iio z, f x) + ∫⁻ x in Icc z y, f x := by + rw [← Iio_union_Icc_eq_Iic hzy, lintegral_union measurableSet_Icc] + rw [Set.disjoint_iff] + rintro x ⟨h1 : x < _, h2, _⟩ + linarith + +namespace ProbabilityTheory + +section GammaPdf + +/-- The pdf of the gamma distribution depending on its scale and rate-/ +noncomputable +def gammaPdfReal (a r x : ℝ) : ℝ := + if 0 ≤ x then r ^ a / (Gamma a) * x ^ (a-1) * exp (-(r * x)) else 0 + +/-- The pdf of the Gamma distribution, as a function valued in `ℝ≥0∞` -/ +noncomputable +def gammaPdf (a r x : ℝ) : ℝ≥0∞ := + ENNReal.ofReal (gammaPdfReal a r x) + +lemma gammaPdf_eq (a r x : ℝ) : + gammaPdf a r x = ENNReal.ofReal (if 0 ≤ x then + r ^ a / (Gamma a) * x ^ (a-1) * exp (-(r * x)) else 0) := rfl + +lemma gammaPdf_of_neg {a r x : ℝ} (hx : x < 0) : gammaPdf a r x = 0 := by + simp only [gammaPdf_eq, if_neg (not_le.mpr hx), ENNReal.ofReal_zero] + +lemma gammaPdf_of_nonneg {a r x : ℝ} (hx : 0 ≤ x) : + gammaPdf a r x = ENNReal.ofReal (r ^ a / (Gamma a) * x ^ (a-1) * exp (-(r * x))) := by + simp only [gammaPdf_eq, if_pos hx] + +/-- the Lebesgue integral of the Gamma pdf over nonpositive reals equals 0 -/ +lemma lintegral_gammaPdf_of_nonpos {x a r : ℝ} (hx : x ≤ 0) : + ∫⁻ y in Iio x, gammaPdf a r y = 0 := by + rw [set_lintegral_congr_fun (g := fun _ ↦ 0) measurableSet_Iio] + · rw [lintegral_zero, ← ENNReal.ofReal_zero] + · simp only [gammaPdf_eq, ge_iff_le, ENNReal.ofReal_eq_zero] + apply ae_of_all _ fun a (_ : a < _) ↦ by rw [if_neg (by linarith)] + +/-- The gamma pdf is measurable. -/ +lemma measurable_gammaPdfReal (a r : ℝ) : Measurable (gammaPdfReal a r) := + Measurable.ite measurableSet_Ici (((measurable_id'.pow_const _).const_mul _).mul + (measurable_id'.const_mul _).neg.exp) measurable_const + +/-- the Gamma pdf is positive for all positive reals -/ +lemma gammaPdfReal_pos {x a r : ℝ} (ha : 0 < a) (hr : 0 < r) (hx : 0 < x) : + 0 < gammaPdfReal a r x := by + simp only [gammaPdfReal, if_pos hx.le] + positivity + +/-- The Gamma pdf is nonnegative -/ +lemma gammaPdfReal_nonneg {a r : ℝ} (ha : 0 < a) (hr : 0 < r) (x : ℝ) : + 0 ≤ gammaPdfReal a r x := by + unfold gammaPdfReal + split_ifs <;> positivity + +open Measure + +/-- The pdf of the Gamma distribution integrates to 1 -/ +@[simp] +lemma lintegral_gammaPdf_eq_one {a r : ℝ} (ha : 0 < a) (hr : 0 < r) : + ∫⁻ x, gammaPdf a r x = 1 := by + have leftSide : ∫⁻ x in Iio 0, gammaPdf a r x = 0 := by + rw [set_lintegral_congr_fun measurableSet_Iio + (ae_of_all _ (fun x (hx : x < 0) ↦ gammaPdf_of_neg hx)), lintegral_zero] + have rightSide : ∫⁻ x in Ici 0, gammaPdf a r x = + ∫⁻ x in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * exp (-(r * x))) := + set_lintegral_congr_fun measurableSet_Ici (ae_of_all _ (fun _ ↦ gammaPdf_of_nonneg)) + rw [← ENNReal.toReal_eq_one_iff, ← lintegral_add_compl _ measurableSet_Ici, compl_Ici, + leftSide, rightSide, add_zero, ← integral_eq_lintegral_of_nonneg_ae] + · simp_rw [integral_Ici_eq_integral_Ioi, mul_assoc] + rw [integral_mul_left, integral_rpow_mul_exp_neg_mul_Ioi ha hr, div_mul_eq_mul_div, + ← mul_assoc, mul_div_assoc, div_self (Gamma_pos_of_pos ha).ne', mul_one, + div_rpow zero_le_one hr.le, one_rpow, mul_one_div, div_self (rpow_pos_of_pos hr _).ne'] + · rw [EventuallyLE, ae_restrict_iff' measurableSet_Ici] + exact ae_of_all _ (fun x (hx : 0 ≤ x) ↦ by positivity) + · apply (measurable_gammaPdfReal a r).aestronglyMeasurable.congr + refine (ae_restrict_iff' measurableSet_Ici).mpr <| ae_of_all _ fun x (hx : 0 ≤ x) ↦ ?_ + simp_rw [gammaPdfReal, eq_true_intro hx, ite_true] + +end GammaPdf + +open MeasureTheory + +/-- Measure defined by the Gamma distribution -/ +noncomputable +def gammaMeasure (a r : ℝ) : Measure ℝ := + volume.withDensity (gammaPdf a r) + +lemma isProbabilityMeasureGamma {a r : ℝ} (ha : 0 < a) (hr : 0 < r) : + IsProbabilityMeasure (gammaMeasure a r) where + measure_univ := by simp [gammaMeasure, lintegral_gammaPdf_eq_one ha hr] + +section GammaCdf + +/-- CDF of the Gamma distribution -/ +noncomputable +def gammaCdfReal (a r : ℝ) : StieltjesFunction := + cdf (gammaMeasure a r) + +lemma gammaCdfReal_eq_integral {a r : ℝ} (ha : 0 < a) (hr : 0 < r) (x : ℝ) : + gammaCdfReal a r x = ∫ x in Iic x, gammaPdfReal a r x := by + have : IsProbabilityMeasure (gammaMeasure a r) := isProbabilityMeasureGamma ha hr + rw [gammaCdfReal, cdf_eq_toReal, gammaMeasure, withDensity_apply _ measurableSet_Iic] + refine (integral_eq_lintegral_of_nonneg_ae ?_ ?_).symm + · exact ae_of_all _ fun b ↦ by simp only [Pi.zero_apply, gammaPdfReal_nonneg ha hr] + · exact (measurable_gammaPdfReal a r).aestronglyMeasurable.restrict + +lemma gammaCdfReal_eq_lintegral {a r : ℝ} (ha : 0 < a) (hr : 0 < r) (x : ℝ) : + gammaCdfReal a r x = ENNReal.toReal (∫⁻ x in Iic x, gammaPdf a r x) := by + have : IsProbabilityMeasure (gammaMeasure a r) := isProbabilityMeasureGamma ha hr + simp only [gammaPdf, gammaCdfReal, cdf_eq_toReal] + simp only [gammaMeasure, measurableSet_Iic, withDensity_apply, gammaPdf] + +end GammaCdf diff --git a/Mathlib/Probability/Independence/Basic.lean b/Mathlib/Probability/Independence/Basic.lean index 18a7e4b341b6c..1e461cc0a4f38 100644 --- a/Mathlib/Probability/Independence/Basic.lean +++ b/Mathlib/Probability/Independence/Basic.lean @@ -650,11 +650,12 @@ theorem indepFun_iff_map_prod_eq_prod_map_map {mβ : MeasurableSpace β} {mβ' : rw [(h₀ hs ht).1, (h₀ hs ht).2, h, Measure.prod_prod] @[symm] -nonrec theorem IndepFun.symm {_ : MeasurableSpace β} {f g : Ω → β} (hfg : IndepFun f g μ) : - IndepFun g f μ := hfg.symm +nonrec theorem IndepFun.symm {_ : MeasurableSpace β} {_ : MeasurableSpace β'} + (hfg : IndepFun f g μ) : IndepFun g f μ := hfg.symm #align probability_theory.indep_fun.symm ProbabilityTheory.IndepFun.symm -theorem IndepFun.ae_eq {mβ : MeasurableSpace β} {f g f' g' : Ω → β} (hfg : IndepFun f g μ) +theorem IndepFun.ae_eq {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} + {f' : Ω → β} {g' : Ω → β'} (hfg : IndepFun f g μ) (hf : f =ᵐ[μ] f') (hg : g =ᵐ[μ] g') : IndepFun f' g' μ := by refine kernel.IndepFun.ae_eq hfg ?_ ?_ <;> simp only [ae_dirac_eq, Filter.eventually_pure, kernel.const_apply] diff --git a/Mathlib/Probability/Independence/Kernel.lean b/Mathlib/Probability/Independence/Kernel.lean index 89457332a0f2f..222525433f5ab 100644 --- a/Mathlib/Probability/Independence/Kernel.lean +++ b/Mathlib/Probability/Independence/Kernel.lean @@ -788,10 +788,11 @@ theorem indepFun_iff_indepSet_preimage {mβ : MeasurableSpace β} {mβ' : Measur · rwa [← indepSet_iff_measure_inter_eq_mul (hf hs) (hg ht) κ μ] @[symm] -nonrec theorem IndepFun.symm {_ : MeasurableSpace β} {f g : Ω → β} (hfg : IndepFun f g κ μ) : - IndepFun g f κ μ := hfg.symm +nonrec theorem IndepFun.symm {_ : MeasurableSpace β} {_ : MeasurableSpace β'} + (hfg : IndepFun f g κ μ) : IndepFun g f κ μ := hfg.symm -theorem IndepFun.ae_eq {mβ : MeasurableSpace β} {f g f' g' : Ω → β} (hfg : IndepFun f g κ μ) +theorem IndepFun.ae_eq {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} + {f' : Ω → β} {g' : Ω → β'} (hfg : IndepFun f g κ μ) (hf : ∀ᵐ a ∂μ, f =ᵐ[κ a] f') (hg : ∀ᵐ a ∂μ, g =ᵐ[κ a] g') : IndepFun f' g' κ μ := by rintro _ _ ⟨A, hA, rfl⟩ ⟨B, hB, rfl⟩ diff --git a/Mathlib/Topology/Homeomorph.lean b/Mathlib/Topology/Homeomorph.lean index eab27e4b2cba2..62369062ba06a 100644 --- a/Mathlib/Topology/Homeomorph.lean +++ b/Mathlib/Topology/Homeomorph.lean @@ -74,6 +74,7 @@ protected def empty [IsEmpty X] [IsEmpty Y] : X ≃ₜ Y where __ := Equiv.equivOfIsEmpty X Y /-- Inverse of a homeomorphism. -/ +@[symm] protected def symm (h : X ≃ₜ Y) : Y ≃ₜ X where continuous_toFun := h.continuous_invFun continuous_invFun := h.continuous_toFun @@ -117,6 +118,7 @@ protected def refl (X : Type*) [TopologicalSpace X] : X ≃ₜ X where #align homeomorph.refl Homeomorph.refl /-- Composition of two homeomorphisms. -/ +@[trans] protected def trans (h₁ : X ≃ₜ Y) (h₂ : Y ≃ₜ Z) : X ≃ₜ Z where continuous_toFun := h₂.continuous_toFun.comp h₁.continuous_toFun continuous_invFun := h₁.continuous_invFun.comp h₂.continuous_invFun diff --git a/Mathlib/Topology/PartialHomeomorph.lean b/Mathlib/Topology/PartialHomeomorph.lean index d0c6a7b94550f..c290c93085038 100644 --- a/Mathlib/Topology/PartialHomeomorph.lean +++ b/Mathlib/Topology/PartialHomeomorph.lean @@ -76,6 +76,7 @@ instance : CoeFun (PartialHomeomorph α β) fun _ => α → β := ⟨fun e => e.toFun'⟩ /-- The inverse of a partial homeomorphism -/ +@[symm] protected def symm : PartialHomeomorph β α where toPartialEquiv := e.toPartialEquiv.symm open_source := e.open_target @@ -816,6 +817,7 @@ protected def trans' (h : e.target = e'.source) : PartialHomeomorph α γ where /-- Composing two partial homeomorphisms, by restricting to the maximal domain where their composition is well defined. -/ +@[trans] protected def trans : PartialHomeomorph α γ := PartialHomeomorph.trans' (e.symm.restrOpen e'.source e'.open_source).symm (e'.restrOpen e.target e.open_target) (by simp [inter_comm]) @@ -1024,13 +1026,13 @@ theorem Set.EqOn.restr_eqOn_source {e e' : PartialHomeomorph α β} /-- Composition of a partial homeomorphism and its inverse is equivalent to the restriction of the identity to the source -/ -theorem trans_self_symm : e.trans e.symm ≈ PartialHomeomorph.ofSet e.source e.open_source := - PartialEquiv.trans_self_symm _ -#align local_homeomorph.trans_self_symm PartialHomeomorph.trans_self_symm +theorem self_trans_symm : e.trans e.symm ≈ PartialHomeomorph.ofSet e.source e.open_source := + PartialEquiv.self_trans_symm _ +#align local_homeomorph.self_trans_symm PartialHomeomorph.self_trans_symm -theorem trans_symm_self : e.symm.trans e ≈ PartialHomeomorph.ofSet e.target e.open_target := - e.symm.trans_self_symm -#align local_homeomorph.trans_symm_self PartialHomeomorph.trans_symm_self +theorem symm_trans_self : e.symm.trans e ≈ PartialHomeomorph.ofSet e.target e.open_target := + e.symm.self_trans_symm +#align local_homeomorph.symm_trans_self PartialHomeomorph.symm_trans_self theorem eq_of_eqOnSource_univ {e e' : PartialHomeomorph α β} (h : e ≈ e') (s : e.source = univ) (t : e.target = univ) : e = e' := @@ -1445,7 +1447,7 @@ theorem subtypeRestr_symm_trans_subtypeRestr (f f' : PartialHomeomorph α β) : rw [ofSet_trans', sets_identity, ← trans_of_set' _ openness₂, trans_assoc] refine' EqOnSource.trans' (eqOnSource_refl _) _ -- f has been eliminated !!! - refine' Setoid.trans (trans_symm_self s.localHomeomorphSubtypeCoe) _ + refine' Setoid.trans (symm_trans_self s.localHomeomorphSubtypeCoe) _ simp only [mfld_simps, Setoid.refl] #align local_homeomorph.subtype_restr_symm_trans_subtype_restr PartialHomeomorph.subtypeRestr_symm_trans_subtypeRestr