multiplicativeClosure_isGenerator_eq_top

English

The multiplicative closure of generators equals the top element.

Русский

Замыкание генераторов по умножению равно верхнему элементу.

LaTeX

$$$$ \\text{generators.multiplicativeClosure} = \\top $$$$

Lean4

/-- A property is true for every morphism iff it holds for generators and is multiplicative. -/
theorem multiplicativeClosure_isGenerator_eq_top : generators.multiplicativeClosure = ⊤ :=
  by
  apply le_antisymm (by simp)
  intro x y f _
  apply CategoryTheory.Quotient.induction
  apply Paths.induction
  · exact generators.multiplicativeClosure.id_mem _
  · rintro _ _ _ _ ⟨⟩ h
    · exact generators.multiplicativeClosure.comp_mem _ _ h <| .of _ <| .δ _
    · exact generators.multiplicativeClosure.comp_mem _ _ h <| .of _ <| .σ _

Похожие утверждения