Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

Commit

Permalink
chore(*): remove after the fact attribute [irreducible] at several …
Browse files Browse the repository at this point in the history
…places (#18168)

Part of #18164
  • Loading branch information
sgouezel committed Jan 16, 2023
1 parent ec2dfca commit 565eb99
Show file tree
Hide file tree
Showing 16 changed files with 284 additions and 151 deletions.
33 changes: 17 additions & 16 deletions src/algebra/free_algebra.lean
Original file line number Diff line number Diff line change
Expand Up @@ -179,9 +179,10 @@ variables {X}
/--
The canonical function `X → free_algebra R X`.
-/
def ι : X → free_algebra R X := λ m, quot.mk _ m
@[irreducible] def ι : X → free_algebra R X := λ m, quot.mk _ m

@[simp] lemma quot_mk_eq_ι (m : X) : quot.mk (free_algebra.rel R X) m = ι R m := rfl
@[simp] lemma quot_mk_eq_ι (m : X) : quot.mk (free_algebra.rel R X) m = ι R m :=
by rw [ι]

variables {A : Type*} [semiring A] [algebra R A]

Expand Down Expand Up @@ -230,16 +231,17 @@ private def lift_aux (f : X → A) : (free_algebra R X →ₐ[R] A) :=
Given a function `f : X → A` where `A` is an `R`-algebra, `lift R f` is the unique lift
of `f` to a morphism of `R`-algebras `free_algebra R X → A`.
-/
def lift : (X → A) ≃ (free_algebra R X →ₐ[R] A) :=
@[irreducible] def lift : (X → A) ≃ (free_algebra R X →ₐ[R] A) :=
{ to_fun := lift_aux R,
inv_fun := λ F, F ∘ (ι R),
left_inv := λ f, by {ext, refl},
left_inv := λ f, by {ext, rw [ι], refl},
right_inv := λ F, by
{ ext x,
rcases x,
induction x,
case pre.of :
{ change ((F : free_algebra R X → A) ∘ (ι R)) _ = _,
rw [ι],
refl },
case pre.of_scalar :
{ change algebra_map _ _ x = F (algebra_map _ _ x),
Expand All @@ -251,36 +253,35 @@ def lift : (X → A) ≃ (free_algebra R X →ₐ[R] A) :=
{ change lift_aux R (F ∘ ι R) (quot.mk _ _ * quot.mk _ _) = F (quot.mk _ _ * quot.mk _ _),
rw [alg_hom.map_mul, alg_hom.map_mul, ha, hb], }, }, }

@[simp] lemma lift_aux_eq (f : X → A) : lift_aux R f = lift R f := rfl
@[simp] lemma lift_aux_eq (f : X → A) : lift_aux R f = lift R f :=
by { rw [lift], refl }

@[simp]
lemma lift_symm_apply (F : free_algebra R X →ₐ[R] A) : (lift R).symm F = F ∘ (ι R) := rfl
lemma lift_symm_apply (F : free_algebra R X →ₐ[R] A) : (lift R).symm F = F ∘ (ι R) :=
by { rw [lift], refl }

variables {R X}

@[simp]
theorem ι_comp_lift (f : X → A) :
(lift R f : free_algebra R X → A) ∘ (ι R) = f := by {ext, refl}
(lift R f : free_algebra R X → A) ∘ (ι R) = f :=
by { ext, rw [ι, lift], refl }

@[simp]
theorem lift_ι_apply (f : X → A) (x) :
lift R f (ι R x) = f x := rfl
lift R f (ι R x) = f x :=
by { rw [ι, lift], refl }

@[simp]
theorem lift_unique (f : X → A) (g : free_algebra R X →ₐ[R] A) :
(g : free_algebra R X → A) ∘ (ι R) = f ↔ g = lift R f :=
(lift R).symm_apply_eq
by { rw [← (lift R).symm_apply_eq, lift], refl }

/-!
At this stage we set the basic definitions as `@[irreducible]`, so from this point onwards one
Since we have set the basic definitions as `@[irreducible]`, from this point onwards one
should only use the universal properties of the free algebra, and consider the actual implementation
as a quotient of an inductive type as completely hidden.
as a quotient of an inductive type as completely hidden. -/

Of course, one still has the option to locally make these definitions `semireducible` if so desired,
and Lean is still willing in some circumstances to do unification based on the underlying
definition.
-/
attribute [irreducible] ι lift
-- Marking `free_algebra` irreducible makes `ring` instances inaccessible on quotients.
-- https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/algebra.2Esemiring_to_ring.20breaks.20semimodule.20typeclass.20lookup/near/212580241
-- For now, we avoid this by not marking it irreducible.
Expand Down
64 changes: 44 additions & 20 deletions src/algebra/ring_quot.lean
Original file line number Diff line number Diff line change
Expand Up @@ -182,7 +182,7 @@ instance [algebra S R] (r : R → R → Prop) : algebra S (ring_quot r) :=
/--
The quotient map from a ring to its quotient, as a homomorphism of rings.
-/
def mk_ring_hom (r : R → R → Prop) : R →+* ring_quot r :=
@[irreducible] def mk_ring_hom (r : R → R → Prop) : R →+* ring_quot r :=
{ to_fun := λ x, ⟨quot.mk _ x⟩,
map_one' := by simp [← one_quot],
map_mul' := by simp [mul_quot],
Expand Down Expand Up @@ -211,7 +211,7 @@ variables {T : Type u₄} [semiring T]
Any ring homomorphism `f : R →+* T` which respects a relation `r : R → R → Prop`
factors uniquely through a morphism `ring_quot r →+* T`.
-/
def lift {r : R → R → Prop} :
@[irreducible] def lift {r : R → R → Prop} :
{f : R →+* T // ∀ ⦃x y⦄, r x y → f x = f y} ≃ (ring_quot r →+* T) :=
{ to_fun := λ f', let f := (f' : R →+* T) in
{ to_fun := λ x, quot.lift f
Expand All @@ -228,13 +228,13 @@ def lift {r : R → R → Prop} :
map_one' := by simp [← one_quot, f.map_one],
map_mul' := by { rintros ⟨⟨x⟩⟩ ⟨⟨y⟩⟩, simp [mul_quot, f.map_mul x y] }, },
inv_fun := λ F, ⟨F.comp (mk_ring_hom r), λ x y h, by { dsimp, rw mk_ring_hom_rel h, }⟩,
left_inv := λ f, by { ext, simp, refl },
right_inv := λ F, by { ext, simp, refl } }
left_inv := λ f, by { ext, simp [mk_ring_hom] },
right_inv := λ F, by { ext, simp [mk_ring_hom] } }

@[simp]
lemma lift_mk_ring_hom_apply (f : R →+* T) {r : R → R → Prop} (w : ∀ ⦃x y⦄, r x y → f x = f y) (x) :
lift ⟨f, w⟩ (mk_ring_hom r x) = f x :=
rfl
by { simp_rw [lift, mk_ring_hom], refl }

-- note this is essentially `lift.symm_apply_eq.mp h`
lemma lift_unique (f : R →+* T) {r : R → R → Prop} (w : ∀ ⦃x y⦄, r x y → f x = f y)
Expand All @@ -243,7 +243,12 @@ by { ext, simp [h], }

lemma eq_lift_comp_mk_ring_hom {r : R → R → Prop} (f : ring_quot r →+* T) :
f = lift ⟨f.comp (mk_ring_hom r), λ x y h, by { dsimp, rw mk_ring_hom_rel h, }⟩ :=
(lift.apply_symm_apply f).symm
begin
conv_lhs { rw ← lift.apply_symm_apply f },
rw lift,
refl,
end


section comm_ring
/-!
Expand All @@ -261,7 +266,11 @@ lift
λ x y h, ideal.quotient.eq.2 $ submodule.mem_Inf.mpr (λ p w, w ⟨x, y, h, sub_add_cancel x y⟩)⟩

@[simp] lemma ring_quot_to_ideal_quotient_apply (r : B → B → Prop) (x : B) :
ring_quot_to_ideal_quotient r (mk_ring_hom r x) = ideal.quotient.mk _ x := rfl
ring_quot_to_ideal_quotient r (mk_ring_hom r x) = ideal.quotient.mk _ x :=
begin
simp_rw [ring_quot_to_ideal_quotient, lift, mk_ring_hom],
refl
end

/-- The universal ring homomorphism from `B ⧸ ideal.of_rel r` to `ring_quot r`. -/
def ideal_quotient_to_ring_quot (r : B → B → Prop) :
Expand All @@ -287,7 +296,20 @@ The ring equivalence between `ring_quot r` and `(ideal.of_rel r).quotient`
def ring_quot_equiv_ideal_quotient (r : B → B → Prop) :
ring_quot r ≃+* B ⧸ ideal.of_rel r :=
ring_equiv.of_hom_inv (ring_quot_to_ideal_quotient r) (ideal_quotient_to_ring_quot r)
(by { ext, refl, }) (by { ext, refl, })
(begin
ext,
simp_rw [ring_quot_to_ideal_quotient, lift, mk_ring_hom],
dsimp,
rw [mk_ring_hom],
refl
end)
(begin
ext,
simp_rw [ring_quot_to_ideal_quotient, lift, mk_ring_hom],
dsimp,
rw [mk_ring_hom],
refl
end)

end comm_ring

Expand Down Expand Up @@ -331,20 +353,20 @@ variables (S)
/--
The quotient map from an `S`-algebra to its quotient, as a homomorphism of `S`-algebras.
-/
def mk_alg_hom (s : A → A → Prop) : A →ₐ[S] ring_quot s :=
{ commutes' := λ r, rfl,
@[irreducible] def mk_alg_hom (s : A → A → Prop) : A →ₐ[S] ring_quot s :=
{ commutes' := λ r, by { simp [mk_ring_hom], refl },
..mk_ring_hom s }

@[simp]
lemma mk_alg_hom_coe (s : A → A → Prop) : (mk_alg_hom S s : A →+* ring_quot s) = mk_ring_hom s :=
rfl
by { simp_rw [mk_alg_hom, mk_ring_hom], refl }

lemma mk_alg_hom_rel {s : A → A → Prop} {x y : A} (w : s x y) :
mk_alg_hom S s x = mk_alg_hom S s y :=
by simp [mk_alg_hom, mk_ring_hom, quot.sound (rel.of w)]

lemma mk_alg_hom_surjective (s : A → A → Prop) : function.surjective (mk_alg_hom S s) :=
by { dsimp [mk_alg_hom], rintro ⟨⟨a⟩⟩, use a, refl, }
by { dsimp [mk_alg_hom, mk_ring_hom], rintro ⟨⟨a⟩⟩, use a, refl, }

variables {B : Type u₄} [semiring B] [algebra S B]

Expand All @@ -361,8 +383,8 @@ end
Any `S`-algebra homomorphism `f : A →ₐ[S] B` which respects a relation `s : A → A → Prop`
factors uniquely through a morphism `ring_quot s →ₐ[S] B`.
-/
def lift_alg_hom {s : A → A → Prop} :
{ f : A →ₐ[S] B // ∀ ⦃x y⦄, s x y → f x = f y} ≃ (ring_quot s →ₐ[S] B) :=
@[irreducible] def lift_alg_hom {s : A → A → Prop} :
{f : A →ₐ[S] B // ∀ ⦃x y⦄, s x y → f x = f y} ≃ (ring_quot s →ₐ[S] B) :=
{ to_fun := λ f', let f := (f' : A →ₐ[S] B) in
{ to_fun := λ x, quot.lift f
begin
Expand All @@ -379,14 +401,14 @@ def lift_alg_hom {s : A → A → Prop} :
map_mul' := by { rintros ⟨⟨x⟩⟩ ⟨⟨y⟩⟩, simp [mul_quot, f.map_mul x y], },
commutes' := by { rintros x, simp [← one_quot, smul_quot, algebra.algebra_map_eq_smul_one] } },
inv_fun := λ F, ⟨F.comp (mk_alg_hom S s), λ _ _ h, by { dsimp, erw mk_alg_hom_rel S h }⟩,
left_inv := λ f, by { ext, simp, refl },
right_inv := λ F, by { ext, simp, refl } }
left_inv := λ f, by { ext, simp [mk_alg_hom, mk_ring_hom] },
right_inv := λ F, by { ext, simp [mk_alg_hom, mk_ring_hom] } }

@[simp]
lemma lift_alg_hom_mk_alg_hom_apply (f : A →ₐ[S] B) {s : A → A → Prop}
(w : ∀ ⦃x y⦄, s x y → f x = f y) (x) :
(lift_alg_hom S ⟨f, w⟩) ((mk_alg_hom S s) x) = f x :=
rfl
by { simp_rw [lift_alg_hom, mk_alg_hom, mk_ring_hom], refl, }

-- note this is essentially `(lift_alg_hom S).symm_apply_eq.mp h`
lemma lift_alg_hom_unique (f : A →ₐ[S] B) {s : A → A → Prop} (w : ∀ ⦃x y⦄, s x y → f x = f y)
Expand All @@ -395,10 +417,12 @@ by { ext, simp [h], }

lemma eq_lift_alg_hom_comp_mk_alg_hom {s : A → A → Prop} (f : ring_quot s →ₐ[S] B) :
f = lift_alg_hom S ⟨f.comp (mk_alg_hom S s), λ x y h, by { dsimp, erw mk_alg_hom_rel S h, }⟩ :=
((lift_alg_hom S).apply_symm_apply f).symm
begin
conv_lhs { rw ← ((lift_alg_hom S).apply_symm_apply f) },
rw lift_alg_hom,
refl,
end

end algebra

attribute [irreducible] mk_ring_hom mk_alg_hom lift lift_alg_hom

end ring_quot
26 changes: 15 additions & 11 deletions src/data/polynomial/eval.lean
Original file line number Diff line number Diff line change
Expand Up @@ -31,10 +31,11 @@ variables (f : R →+* S) (x : S)

/-- Evaluate a polynomial `p` given a ring hom `f` from the scalar ring
to the target and a value `x` for the variable in the target -/
def eval₂ (p : R[X]) : S :=
@[irreducible] def eval₂ (p : R[X]) : S :=
p.sum (λ e a, f a * x ^ e)

lemma eval₂_eq_sum {f : R →+* S} {x : S} : p.eval₂ f x = p.sum (λ e a, f a * x ^ e) := rfl
lemma eval₂_eq_sum {f : R →+* S} {x : S} : p.eval₂ f x = p.sum (λ e a, f a * x ^ e) :=
by rw eval₂

lemma eval₂_congr {R S : Type*} [semiring R] [semiring S]
{f g : R →+* S} {s t : S} {φ ψ : R[X]} :
Expand Down Expand Up @@ -66,7 +67,7 @@ begin
end

@[simp] lemma eval₂_add : (p + q).eval₂ f x = p.eval₂ f x + q.eval₂ f x :=
by { apply sum_add_index; simp [add_mul] }
by { simp only [eval₂_eq_sum], apply sum_add_index; simp [add_mul] }

@[simp] lemma eval₂_one : (1 : R[X]).eval₂ f x = 1 :=
by rw [← C_1, eval₂_C, f.map_one]
Expand Down Expand Up @@ -256,7 +257,7 @@ variables {x : R}
def eval : R → R[X] → R := eval₂ (ring_hom.id _)

lemma eval_eq_sum : p.eval x = p.sum (λ e a, a * x ^ e) :=
rfl
by { rw [eval, eval₂_eq_sum], refl }

lemma eval_eq_sum_range {p : R[X]} (x : R) :
p.eval x = ∑ i in finset.range (p.nat_degree + 1), p.coeff i * x ^ i :=
Expand Down Expand Up @@ -382,8 +383,12 @@ lemma is_root.eq_zero (h : is_root p x) : eval x p = 0 := h

lemma coeff_zero_eq_eval_zero (p : R[X]) : coeff p 0 = p.eval 0 :=
calc coeff p 0 = coeff p 0 * 0 ^ 0 : by simp
... = p.eval 0 : eq.symm $
finset.sum_eq_single _ (λ b _ hb, by simp [zero_pow (nat.pos_of_ne_zero hb)]) (by simp)
... = p.eval 0 :
begin
symmetry,
rw [eval_eq_sum],
exact finset.sum_eq_single _ (λ b _ hb, by simp [zero_pow (nat.pos_of_ne_zero hb)]) (by simp)
end

lemma zero_is_root_of_coeff_zero_eq_zero {p : R[X]} (hp : p.coeff 0 = 0) : is_root p 0 :=
by rwa coeff_zero_eq_eval_zero at hp
Expand All @@ -401,7 +406,8 @@ section comp
/-- The composition of polynomials as a polynomial. -/
def comp (p q : R[X]) : R[X] := p.eval₂ C q

lemma comp_eq_sum_left : p.comp q = p.sum (λ e a, C a * q ^ e) := rfl
lemma comp_eq_sum_left : p.comp q = p.sum (λ e a, C a * q ^ e) :=
by rw [comp, eval₂_eq_sum]

@[simp] lemma comp_X : p.comp X = p :=
begin
Expand Down Expand Up @@ -735,12 +741,10 @@ end
end map

/-!
After having set up the basic theory of `eval₂`, `eval`, `comp`, and `map`,
we make `eval₂` irreducible.
we have made `eval₂` irreducible from the start.
Perhaps we can make the others irreducible too?
Perhaps we can make also `eval`, `comp`, and `map` irreducible too?
-/
attribute [irreducible] polynomial.eval₂

section hom_eval₂

Expand Down
7 changes: 2 additions & 5 deletions src/linear_algebra/determinant.lean
Original file line number Diff line number Diff line change
Expand Up @@ -128,7 +128,7 @@ there is no good way to generalize over universe parameters, so we can't fully s
type that it does not depend on the choice of basis. Instead you can use the `det_aux_def'` lemma,
or avoid mentioning a basis at all using `linear_map.det`.
-/
def det_aux : trunc (basis ι A M) → (M →ₗ[A] M) →* A :=
@[irreducible] def det_aux : trunc (basis ι A M) → (M →ₗ[A] M) →* A :=
trunc.lift
(λ b : basis ι A M,
(det_monoid_hom).comp (to_matrix_alg_equiv b : (M →ₗ[A] M) →* matrix ι ι A))
Expand All @@ -140,10 +140,7 @@ See also `det_aux_def'` which allows you to vary the basis.
-/
lemma det_aux_def (b : basis ι A M) (f : M →ₗ[A] M) :
linear_map.det_aux (trunc.mk b) f = matrix.det (linear_map.to_matrix b b f) :=
rfl

-- Discourage the elaborator from unfolding `det_aux` and producing a huge term.
attribute [irreducible] linear_map.det_aux
by { rw [det_aux], refl }

lemma det_aux_def' {ι' : Type*} [fintype ι'] [decidable_eq ι']
(tb : trunc $ basis ι A M) (b' : basis ι' A M) (f : M →ₗ[A] M) :
Expand Down
11 changes: 5 additions & 6 deletions src/linear_algebra/dimension.lean
Original file line number Diff line number Diff line change
Expand Up @@ -105,7 +105,7 @@ In particular this agrees with the usual notion of the dimension of a vector spa
The definition is marked as protected to avoid conflicts with `_root_.rank`,
the rank of a linear map.
-/
protected def module.rank : cardinal :=
@[irreducible] protected def module.rank : cardinal :=
⨆ ι : {s : set V // linear_independent K (coe : s → V)}, #ι.1

end
Expand Down Expand Up @@ -136,6 +136,7 @@ theorem dim_le {n : ℕ}
(H : ∀ s : finset M, linear_independent R (λ i : s, (i : M)) → s.card ≤ n) :
module.rank R M ≤ n :=
begin
rw module.rank,
apply csupr_le',
rintro ⟨s, li⟩,
exact linear_independent_bounded_of_finset_linear_independent_bounded H _ li,
Expand Down Expand Up @@ -239,7 +240,7 @@ begin
apply le_trans,
{ exact cardinal.lift_mk_le.mpr
⟨(equiv.of_injective _ hv.injective).to_embedding⟩, },
{ simp only [cardinal.lift_le],
{ simp only [cardinal.lift_le, module.rank],
apply le_trans,
swap,
exact le_csupr (cardinal.bdd_above_range.{v v} _) ⟨range v, hv.coe_range⟩,
Expand All @@ -266,6 +267,7 @@ variables (R M)
@[simp] lemma dim_punit : module.rank R punit = 0 :=
begin
apply le_bot_iff.mp,
rw module.rank,
apply csupr_le',
rintro ⟨s, li⟩,
apply le_bot_iff.mpr,
Expand Down Expand Up @@ -775,6 +777,7 @@ theorem basis.mk_eq_dim'' {ι : Type v} (v : basis ι R M) :
#ι = module.rank R M :=
begin
haveI := nontrivial_of_invariant_basis_number R,
rw module.rank,
apply le_antisymm,
{ transitivity,
swap,
Expand All @@ -786,10 +789,6 @@ begin
apply linear_independent_le_basis v _ li, },
end

-- By this stage we want to have a complete API for `module.rank`,
-- so we set it `irreducible` here, to keep ourselves honest.
attribute [irreducible] module.rank

theorem basis.mk_range_eq_dim (v : basis ι R M) :
#(range v) = module.rank R M :=
v.reindex_range.mk_eq_dim''
Expand Down
Loading

0 comments on commit 565eb99

Please sign in to comment.